In the past year, custom and unreleased math reasoning models reached gold medal performance on the International Mathematical Olympiad (IMO). Similar performance was then reported using large-scale inference on publicly available models but at prohibitive costs (e.g., 3000 USD per problem). In this work, we present an inference pipeline that attains best-in-class performance on IMO-style math problems at an average inference cost orders of magnitude below competing methods while using only general-purpose off-the-shelf models. Our method relies on insights about grader failure in solver-grader pipelines, which we call the Cognitive Well (iterative refinement converging to a wrong solution that the solver as well as the pipeline's internal grader consider to be basically correct). Our pipeline addresses these failure modes through conjecture extraction, wherein candidate lemmas are isolated from generated solutions and independently verified alongside their negations in a fresh environment (context detachment). On IMO-ProofBench Advanced (PB-Adv), our pipeline achieves 67.1 percent performance using Gemini 3.0 Pro with an average cost per question of approximately 31 USD. At the time of evaluation, this represented the state-of-the-art on PB-Adv among both public and unreleased models, and more than doubles the success rate of the next best publicly accessible pipeline, all at a fraction of the cost.
Figures & tables
Figure 1: Results for our proposed method versus competing methods and models. Both expert graded and autograded results included (where possible). Our proposed method outperforms all open-source pipelines, while being significantly cheaper than these pipelines (cf. Figure 2 ) and ranks second only to a custom and unreleased pipeline. Comparison results taken from Luong et al. (2025) where applicable, and from Shao et al. (2025) . Autograder results calculated using the resources published in Luong et al. (2025) .
Figure 2: Pareto frontier of cost vs. performance measured using the autograder in Luong et al. (2025) . “Single" denotes that the output of a single run of the pipeline. “Combined" denotes our standard algorithm for PB-Adv which uses a further model call to choose from two parallel pipeline runs - cf. Section 2.2 “Post Enhancement and Aggregation"). All costs calculated with January 2026 pricing.
Method
Acc ↑
MAE ↓
Gemini 2.5 Pro
44.3%
30.2%
Momus
28.1%
25.9%
o4-mini (high reasoning)
47.3%
25.2%
Gemini 2.5 Deep Think
52.5%
20.5%
o3
54.0%
20.2%
Momus w/ p. sols
49.8%
19.9%
Table 1: Comparison of Momus Prompts vs. Other models on GraderBench (1000 datapoints). No reference solution provided. Non-Momus models are run with the ProofAutoGrader prompt. MAE is expressed as a percentage of the maximum score of 7.
Method
FPR ↓
FNR ↓
Acc ↑
MAE ↓
Momus
17.2%
26.1%
28.1%
25.9%
ProofAutoGrader
31.7%
6.2%
59.4%
17.6%
Momus w/ p.sols
26.9%
8.8%
49.8%
19.9%
Table 2: Comparison of Momus Prompts vs. ProofAutoGrader (with reference solution) on GraderBench (1000 datapoints). MAE is expressed as a percentage of the maximum score of 7.
Figure 3: Case study of benefits of conjecture extraction/resolution on the solution pipeline. We run (a) the pipeline without any conjecture steps and (b) with conjecture steps. For both runs, we equalize token budgets. We sample solutions for five phases throughout the runs. We then grade these runs using both the pipeline’s internal grader and the external ProofAutoGrader. We see that with conjectures, the ProofAutoGrader scores monotonically increase, while those without may jump wildly or flatline. Spikes in conjecture-based solving correspond to proof/disproof of conjectures.
Appendix figures & tables12 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 4: A high level overview of our pipeline. A problem is processed by parallel solver–grader pairs (module A ). When progress stalls, the Conjecture Extractor identifies candidate lemmas Ci and their negations from current proof attempts. Each conjecture is resolved by an independent solver–grader module (also A ), with proofs (for either the conjecture or its negation) fed back to enable further progress toward the final solution.
Figure 5: Results for IMO Proof Bench (Basic) according to the IMO-Bench autograder. “Single" here denotes that the output of a single run of the pipeline was submitted (as opposed to our standard algorithm for PB-Adv which uses a further model call to choose from two parallel pipeline runs - cf. Section 2.2 “Post Enhancement and Aggregation"). All comparison results taken from Luong et al. [2025] .
Model
ProofBench
IMO-AnswerBench
Qwen3-30B-A3B-Thinking-2507
26.1
67.0
Qwen3-235B-A22B-Thinking-2507
33.7
70.5
GPT-OSS-120B
47.5
70.5
DeepSeek-Math-V2
60.6
75.8
Gemini 3 Pro
66.7
83.2
Ours (Gemini 3.0 Flash)
80.3
91.3
Appendix
Table 3: Results on ProofBench and IMO-AnswerBench. Our pipeline runs on Gemini 3.0 Flash; baselines from QED-Nano.
Backbone
Base Avg (%)
Ours Avg (%)
Claude 4.6 Opus
23.8
85.7
DeepSeek-V3.2
15.2
66.7
Appendix
Table 4: Generalization across backbones on PB-Advanced. “Base Avg” is the autograded average score (%) for a single call to the model; “Ours Avg” is the score of our pipeline using that model as the backbone. “Graded (Ours)” is the number of problems for which grading had completed at the time of writing.
ProofAutoGrader Score
Count
0/7
1
7/7
14
DNF
15
Appendix
Table 5: The counts of how many questions received each possible autograder result on Huang and Yang [2025] pipeline solutions. None of the proposed solutions earned a 1 through 6. Note that the pipeline does not finish (DNF) if it does not grade a solution correct 5 times in a row.
Response
Accepted by Huang & Yang Verifier
Full
6/20
Truncated
0/20
Appendix
Table 6: Huang & Yang Verifier run 20 times independently on the solution the pipeline emitted on PB-Adv-011 . We see that truncation gets rid of the false positives.
Figure 6: Effect of removing conjectures from successful runs of the solver pipeline, as described in Section 3.5 . The x -axis denotes progression in time and the y -axis corresponds to the grade provided by ProofAutoGrader to the pipeline’s best solution. After removal of conjectures, the solution process becomes erratic or confused. Compare to Figure 3
Metric
HY Average
Momus Average
Score @ 1
4.90
5.33
Max Score @ 4
6.50
6.67
Average-of-4
4.92
5.10
Appendix
Table 7: Comparison of one call to Momus Solver vs. Huang Yang Solver using Average Scores on Proofbench-Basic (30 problems, 4 attempts each). “Score @ 1” is the score on the first attempt (out of 7); “Max Score @ 4” is the highest score across all four attempts.
Config
Avg (%)
L=1 , K=4
52.4
L=3 , K=4
58.1
L=6 , K=4
47.6
Appendix
Table 8: Depth ( L ) sweep at fixed K=4 on Gemini 3.0 Flash, PB-Advanced.
Config
Avg (%)
L=3 , K=2
59.6
L=3 , K=4
58.1
L=3 , K=8
60.5
Appendix
Table 9: Width ( K ) sweep at fixed L=3 on Gemini 3.0 Flash, PB-Advanced.
Run
Total Cost
Gemini 2.5 Pro Run 1
$607.60
Gemini 2.5 Pro Run 2
$618.88
Gemini 2.5 Pro Combined
$1,226.48
Gemini 3.0 Pro Run 1
$428.16
Gemini 3.0 Pro Run 2
$505.48
Gemini 3.0 Pro Combined
$933.64
Appendix
Table 10: Cost Breakdown (USD) by model for all PB-Adv questions.
Figure 7: Confusion matrices of the two Momus graders against the autograder in Luong et al. [2025] .