3 points | by henryrobbins00 a day ago
1 comments
Some additional details about these results that didn't make it into the main post:
- The OpenATP "standard provers" were used; see docs [5] for model / harness configuration details
- Time and cost are function of effort level, which may lead to unfair comparison across provers
- FATE-X excludes task 10 since claude and grok hit session limits
- FATE-X excludes leanstral and aristotle due to temporary endpoint failures
- Deepseek's FATE-X accuracy is corrected from 2 to 3 due to verifier bug (now fixed)
- 2 FATE-X deepseek misses are sorry-free, but rely on native_decide
- Claude's FATE-X miss is due to a failed delegation to a background subagent
- All costs come from underlying CLI, except codex which uses pricing table
Some additional details about these results that didn't make it into the main post:
- The OpenATP "standard provers" were used; see docs [5] for model / harness configuration details
- Time and cost are function of effort level, which may lead to unfair comparison across provers
- FATE-X excludes task 10 since claude and grok hit session limits
- FATE-X excludes leanstral and aristotle due to temporary endpoint failures
- Deepseek's FATE-X accuracy is corrected from 2 to 3 due to verifier bug (now fixed)
- 2 FATE-X deepseek misses are sorry-free, but rely on native_decide
- Claude's FATE-X miss is due to a failed delegation to a background subagent
- All costs come from underlying CLI, except codex which uses pricing table