Research map / Large language models / Agents, code and math
MathConstruct: Challenging LLM Reasoning with Constructive Proofs
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Introduces MathConstruct, a 121-problem olympiad benchmark of constructive proofs with programmatic verifiers and parametric variations (456 instances), finding the best LLM (o3-mini) reaches about 60% average accuracy.
Problem
Existing math benchmarks rely on fixed final answers that are saturated, guessable, or memorizable, and they cover only a narrow subset of proof-type problems; constructive proofs are hard for LLMs yet easy to verify.
Approach
Curate olympiad constructive-proof problems, encode each as a symbolic statement with a Python verifier and a variation generator, and score models with robust accuracy that requires solving all variations of a problem.
Key results
- o3-mini achieves 60.5% average accuracy and 42.1% robust accuracy on MathConstruct, the best among 14 evaluated models.
- o1 is 15 points behind o3-mini and costs USD 415.3 to run the benchmark, about three times the combined cost of the other models.
- Code agents roughly double accuracy for most models at about a fivefold cost increase; Gemini-2.0-Flash-Thinking reaches 20% with code execution.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| allow up to four Python executions per problem | LLMs evaluated on MathConstruct · MathConstruct with code execution | average accuracy | Helped |
| allow Python code execution | 3.5-Sonnet · MathConstruct with code execution | average accuracy: 5% -> 18% | Helped |
| provide parser feedback and allow reprompting | o3-mini · MathConstruct | accuracy: +15% | Helped |
| add detailed ground-truth verifier feedback alongside parser feedback | o3-mini · MathConstruct | average accuracy: 60.54% -> 66.94% | Helped |
| use brute-force inference to generalize from smaller instances | 3.5-Sonnet · MathConstruct | average accuracy: 9.9174 -> 19.2149 | Helped |
| rephrase problem statements | evaluated models · MathConstruct rephrased benchmark | performance | No clear effect |
| increase variation size, measured by Gold solution string length | Flash-Thinking · extreme MathConstruct variations | accuracy | Hurt |
| evaluate every variation as a requirement for solving a problem | models evaluated on MathConstruct · MathConstruct variations | accuracy | Hurt |
Surprising findings
- Brute-force inference agents (Brute+Infer) reach up to 19.2% accuracy, surpassing the general code agent, because they generalize patterns from small instances.
- Using parser feedback raises o3-mini accuracy by about 15 points because it often produces unparseable outputs initially.
Limitations
- Small benchmark of 121 base problems (456 variations) with limited statistical power.
- Some problems are susceptible to brute-force solutions and some variations degenerate into trivial cases.
- Possible residual data contamination; o1-mini shows a small but significant gap on rephrased problems.
Experimental setup
Datasets: MathConstruct
Benchmarks: MathConstruct
Metrics: average accuracy robust accuracy cost in USD
Baselines: GPT-4o o1 o1-mini o3-mini QwQ DeepSeek-R1-Distill-Llama-70B Gemini-2.0-Flash Gemini-2.0-Flash-Thinking Claude-3.5-Sonnet Claude-3.5-Haiku Llama-3.3-70B Llama-3.1-405B
Builds on: Omni-MATH OlympiadBench GSM-Symbolic Putnam-Axiom
Closest papers by meaning
- Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness (NeurIPS 2026 · similarity 0.91)
- MathArena: Evaluating LLMs on Uncontaminated Math Competitions (NeurIPS 2025 · similarity 0.91)
- Putnam-AXIOM: A Functional & Static Benchmark for Measuring Higher Level Mathematical Reasoning in LLMs (ICML 2025 · similarity 0.89)
- RealMath: A Continuous Benchmark for Evaluating Language Models on Research-Level Mathematics (NeurIPS 2025 · similarity 0.89)
- Llemma: An Open Language Model for Mathematics (ICLR 2024 · similarity 0.89)
- One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs (ICML 2025 · similarity 0.89)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.