PaperlayerView exact revision on arXiv

Source-linked AI summary

MathConstruct: Challenging LLM Reasoning with Constructive Proofs

Mislav Balunović, Jasper Dekoninck, Nikola Jovanović, Ivo Petrov, Martin Vechev

arXiv:2502.10197v2cs.AI

TL;DR

Existing math benchmarks often rely on fixed answers, leaving proof evaluation limited, while constructive proofs offer challenging tasks with verifiable solutions. MathConstruct provides a competition-sourced benchmark of such problems with generated variations; the best model achieves 60.5% accuracy and 42.2% robust accuracy.

  • Problem

    Many math benchmarks use fixed ground-truth answers and are unsuitable for evaluating proofs, while formal proof generation remains difficult for LLMs.

    Source: §1 · p. 1

  • Method

    MathConstruct benchmarks constructive proofs with 121 competition-sourced problems, natural-language statements, automated verifiers, and parameter variations.

    Source: §1 · p. 2

  • Results

    O3-MINI achieves 60.5% accuracy and 42.2% robust accuracy, outperforming the second-best model, O1, by a 15% margin.

    Source: §4.1 · p. 6

  • Takeaways & Limitations

    MathConstruct offers a challenging benchmark for evaluating LLM mathematical reasoning through construction problems with readily verifiable correctness.

    Source: §1 · p. 2, §5 · p. 8

Abstract

from arXiv · show

While Large Language Models (LLMs) demonstrate impressive performance in mathematics, existing math benchmarks come with significant limitations. Many focus on problems with fixed ground-truth answers, and are often saturated due to problem simplicity or the viability of guessing or memorization. Crucially, they capture only a narrow subset of relevant math problems. To address this research gap, we introduce MathConstruct, a new benchmark of 121 challenging problems sourced from various math competitions, which targets constructive proofs, a widely encountered problem type requiring the construction of mathematical objects with specific properties. These proofs are particularly suitable for LLM evaluation, as solution correctness can be easily verified. Our automated verifiers also enable MathConstruct to generate problem variations, used to evaluate robustness. State-of-the-art LLMs solve only 60% of MathConstruct problems, highlighting its complexity and importance for LLM evaluation.

1. Introduction

The introduction motivates constructive proofs as challenging tasks whose correctness is straightforward to verify, then presents MATHCONSTRUCT as a benchmark for evaluating LLM reasoning. Its evaluation finds that the best model achieves only 60% accuracy.

Motivation

  • Existing benchmarks often use fixed ground-truth answers, limiting their suitability for proof evaluation, while formal proof generation can be difficult for LLMs.The introduction asks whether proof-based problems can be both challenging and easy to verify.Source: §1 · p. 1

Constructive proofs

  • Constructive proofs require explicitly building an object that satisfies constraints, and proposed constructions are usually straightforward to verify automatically.Examples of such objects include sets, matrices, and graphs.Source: §1 · pp. 1–2

Our benchmark: MATHCONSTRUCT

  • MATHCONSTRUCT contains 121 competition-sourced problems encoded as natural-language statements with verifiers that check proposed constructions.The benchmark is designed to evaluate LLM reasoning through constructive proofs.Source: §1 · p. 2
  • Symbolic problem statements enable parameter variations, while complex constructions and hand curation target robustness, difficulty, and broad mathematical coverage.The authors say complex objects make guessing and memorization less effective.Source: §1 · p. 2

Evaluation

  • The best model achieves only 60% accuracy on MATHCONSTRUCT, despite the evaluation including state-of-the-art LLMs.The introduction also describes analysis of failure modes, problem variations, brute-forceability, and data contamination.Source: §1 · p. 2

2. Related Work

Related work covers fixed-answer math benchmarks, olympiad and private problem sets, symbolic variations, formal theorem proving, logical reasoning, and machine-learning approaches to mathematical construction. MATHCONSTRUCT differs by evaluating construction of mathematical objects rather than relying on predefined answers.

Easier math benchmarks

  • Many math benchmarks use fixed numerical or algebraic answers; GSM8K and MATH are described as saturated, while state-of-the-art models solve approximately 87% of AIME 2024.The passage contrasts early benchmarks with more advanced problem sets.Source: §2 · p. 2

Olympiad-based benchmarks

  • OlympiadBench, Omni-MATH, and HARP include olympiad-level problems but retain fixed-answer verification, unlike MATHCONSTRUCT’s required object construction.For the shared example, Omni-MATH accepts a lower bound as the answer, whereas MATHCONSTRUCT requires an object attaining it.Source: §2 · p. 3

Private benchmarks

  • FrontierMath and LastExam are private benchmarks, which the authors say limits large-scale use and assessment of field-wide progress.Source: §2 · p. 3

Benchmarks with variations

  • Prior work uses symbolic reformulations in other domains, while MATHCONSTRUCT applies variations to problems requiring complex mathematical constructions.The cited examples include GSM-Symbolic (Mirzadeh et al., 2024), Putnam-Axiom, and UTMath (Yang et al., 2024).Source: §2 · p. 3

Formal math benchmarks; Logical reasoning benchmarks

  • Formal theorem-proving benchmarks require languages such as Lean, while logical-reasoning benchmarks primarily test algorithmic problem-solving rather than mathematical reasoning.The passage also notes that LLMs struggle to solve more than a few formal benchmark problems even with specialized training.Source: §2 · p. 3

Constructions with machine learning

  • Machine learning has been applied to counterexample search, combinatorial optimization, and discovery of relationships between mathematical objects.Examples include reinforcement learning for graph-theory counterexamples and neural networks for combinatorial optimization.Source: §2 · p. 3

3. MATHCONSTRUCT

MathConstruct turns difficult competition problems into constructive tasks with explicit verifiers and parameterized variations. This section describes how problems are selected, encoded, reviewed, and finalized as a 121-problem benchmark.

3.1. Problem Selection

  • From around 3,500 problems across 20 competitions, the team selected tasks requiring nontrivial reasoning, complex outputs, tractable verification, and parameter variations.The initial selection contained 158 possible problems.Source: §3.1 · pp. 3–4
  • Some Inf-, All-, and Max-problems are adapted into constructive tasks when their construction remains sufficiently difficult and meets the quality criteria.Examples include producing k constructions for an Inf-problem or constructing an object that achieves a bound for a Max-problem.Source: §3.1 · p. 4

3.2. Math Construction Problems

  • Each problem encodes symbolic P, concrete parameters θ, and verifier Vθ; variations change θ while retaining P and Vθ, and formatting instructions and a parser support model outputs.The variations permit robustness evaluation under parameter changes.Source: §3.2 · pp. 4–5

3.3. Problem Review

  • Problem review combined author-written solution functions and unit tests with human solvability checks, peer review, and automated checks for ambiguity, excessive output, and brute-force solutions.Automated checks also verified that each problem could be solved when the solution was supplied.Source: §3.3 · p. 5
  • The finalized benchmark contains 121 problems, well-distributed across categories, with around half Any-problems and the rest adapted types.Thirty-seven problems with unresolvable issues were discarded.Source: §3.3 · p. 5, Table 1 · p. 5

4. Experimental Evaluation

The evaluation tests 14 LLMs across main, code-agent, brute-force, parser-feedback, contamination, and variation settings. O3-MINI leads the main results, while accuracy also varies with feedback, contamination checks, and problem-variation size.

4.1. Main Results

  • 60.5% accuracy and 42.2% robust accuracy put O3-MINI first; it outperforms second-best O1 by a 15% margin.Table 2 reports average and robust accuracy alongside cost in USD.Source: §4.1 · p. 6, Table 2 · p. 6
  • 82.0% average accuracy is reported for GPT-5 with high reasoning in the 2025 update.O1 costs USD 415.3, three times the combined cost of all other models; robust accuracy is approximately half average accuracy across models.Source: §4.1 · p. 6

4.2. Alternative Evaluation Settings

  • Most models roughly double accuracy with code execution at fivefold cost; FLASH reaches the setting’s highest accuracy, 20%.3.5-SONNET rises from 5% to 18% accuracy.Source: §4.2 · p. 6, Figure 4 · p. 6
  • Pure BRUTE achieves less than 10% accuracy, while BRUTE+INFER reaches up to 19.2% by generalizing from smaller instances.Manual review found most correct pure-brute-force solutions involved non-trivial reasoning or luck, while BRUTE+INFER often discovered patterns.Source: §4.2 · p. 7, Table 3 · p. 7

4.3. Error Analysis

  • O3-MINI often gives unparseable answers but gains +15% accuracy after parser feedback; QWQ does not improve its parseability.The error categories are unparseable, no solution, reject, format, and incorrect.Source: §4.3 · p. 7, Figure 5 · p. 7

4.4. Contamination Analysis

  • Rephrased-benchmark performance closely matches the original, suggesting minimal contamination; O1-MINI’s deviation is 3.8±3.5% and does not change model rankings.The comparison uses GPT-4O-rephrased problem statements; the deviation is reported as a bootstrapped 2σ confidence interval.Source: §4.4 · p. 8, Figure 6 · p. 8

4.5. Effect of Problem Variations

  • 9 selected problems each receive 24 extreme variants, grouped by GOLD-solution string length; FLASH-THINKING nears 100% on trivial cases but declines as size grows.BRUTE succeeds only on very small variants, often because they degenerate into trivial cases; such variants were generally excluded during problem review.Source: §4.5 · p. 8, Figure 7 · p. 8

5. Conclusion

The paper introduces MATHCONSTRUCT to evaluate mathematical reasoning through constructive proofs. It comprises 121 curated problems and 456 varied instances, on which even advanced models struggle.

5. Conclusion

  • MATHCONSTRUCT evaluates LLM mathematical reasoning through constructive proofs, combining challenging construction tasks with straightforward correctness verification.The benchmark starts from 121 curated problems and generates 456 instances by varying key parameters.Source: §5 · p. 8
  • The evaluation of 14 LLMs finds that even the most advanced models struggle significantly on these tasks.The benchmark focuses on constructing valid mathematical objects.Source: §5 · p. 8
  • The authors present MATHCONSTRUCT as a resource for advancing mathematical-reasoning benchmarks.They argue that construction problems push the boundaries of current benchmarks.Source: §5 · p. 8

Impact Statement

MATHCONSTRUCT is presented as a challenging benchmark for evaluating LLM reasoning. The authors frame it as an initial step toward broader mathematics evaluation and future model improvements.

Impact Statement

  • MATHCONSTRUCT provides a challenging benchmark of constructive proofs for evaluating LLM reasoning capabilities.The authors describe it as a first step toward evaluating a broader range of mathematics problems.Source: Impact Statement · p. 9
  • The authors state that broader mathematics evaluations may lead to more comprehensive assessments and subsequent improvements in model performance.Source: Impact Statement · p. 9

A. Dataset Development Workflow

The workflow selects competition problems, encodes each with a verifier and variation generator, and reviews them; the parser handles varied solution formats, with testing and manual checks supporting confidence in its behavior.

A. Dataset Development Workflow

  • Problems are selected from competition archives, encoded in Python with metadata and verification functions, and reviewed for suitability and parser issues.The encoded problem includes configuration metadata, a verifier returning correctness and error information, and a function for generating parameter variations.Source: A. Dataset Development Workflow · p. 11
  • Unit tests check that official solutions pass verification and, when feasible, that incorrect solutions are rejected.The authors note that testing all possible incorrect solutions is generally difficult.Source: A. Dataset Development Workflow · p. 11
  • The review application displays each problem and variation alongside its instructions, ground-truth solution, model interaction, parser feedback, and verification result.Review also helped identify unclear statements or formatting instructions and cases where correct solutions could not be parsed.Source: A. Dataset Development Workflow · pp. 11–12

B. Parser Details

  • The parser extracts boxed solutions, distinguishes primitive from composite types, and recursively parses lists and matrices.It also uses the verifier’s expected list depth to accommodate unnecessary brackets in model outputs.Source: B. Parser Details · pp. 12–13
  • The parser was tested on varied model outputs and manually checked in many runs, giving the authors high confidence that performance does not depend on parser behavior.The parser is designed to handle varied outputs while providing specific error feedback.Source: B. Parser Details · pp. 12–13

C. Additional Benchmark Details

The additional benchmark details summarize problems by source and report the distribution of solution lengths, including one unusually long solution.

C. Additional Benchmark Details

D. Experimental Details

This section introduces further detail on the paper’s experiments and evaluation.

D. Experimental Details

  • The section provides additional details about the experiments and evaluation.The passage does not specify the procedures or results.Source: D. Experimental Details · p. 14

D.1. Experimental Setup

The experimental setup evaluates 121 problems across 456 variations using model-solving and coding-agent procedures; formatting instructions standardize outputs for verification.

D.1. Experimental Setup

  • Models are queried through provider APIs at temperature 1 and top_p 0.9, with maximum output lengths of 16,000 tokens except for specified model families.The O1 family receives 32,000 tokens and FLASH-THINKING has an unlimited output length.Source: §D.1 · p. 14
  • The evaluation uses 121 problems and 456 variations, pairing each problem with an original or suitably challenging variation.When possible, the original variation was kept identical to the competition version.Source: §D.1 · p. 14
  • For chain-of-thought runs, models may be reprompted up to two times after parser errors; coding runs execute submitted code with one- or two-minute limits.General coding models receive one minute, while brute-force agents receive two minutes.Source: §D.1 · pp. 14–15
  • Brute-force agents cannot correct mistakes or adapt after output, while coding and brute-force inference agents may revise responses with parser feedback.Feedback is provided up to twice per solution, with at most four code attempts.Source: §D.1 · p. 15

D.2. Formatting Instructions

  • Formatting instructions cover primitive answers, lists or sets, matrices, and symbolic LaTeX expressions, with generic templates adapted when needed.The templates place answers inside a boxed environment.Source: §D.2 · p. 15

E.1. Analysis of Output Tokens

The analysis compares output-token use with correctness and tests whether detailed feedback from ground-truth verifiers improves performance beyond parser feedback. O1 generally uses fewer tokens and has higher accuracy, while accuracy declines with longer outputs for FLASH-THINKING and O1-MINI.

E.1. Analysis of Output Tokens

  • O1 generally produces fewer output tokens and has higher accuracy than FLASH-THINKING and O1-MINI.FLASH-THINKING exceeds 100k tokens on some problems.Source: §E.1 · p. 17, Figure 13 · p. 17
  • Accuracy steadily decreases with larger output-token counts for FLASH-THINKING and O1-MINI.FLASH-THINKING still has some correct solutions at 50k tokens; O1 reaches 35% accuracy around 40k tokens, where parser feedback enabled some corrections.Source: §E.1 · p. 17, Figure 14 · p. 17

E.2. Verification Feedback

  • The verification-feedback experiment uses detailed ground-truth verifier feedback in addition to parser feedback to estimate an upper bound for an agentic framework.The authors note that writing correct verifiers is challenging, though it might be easier than writing correct solutions.Source: §E.2 · p. 17
  • 66.94% with ground-truth verifier feedback versus 60.54% with parser feedback alone for O3-MINI.The improvement assumes access to ground-truth verifiers, which the authors describe as unrealistic given the difficulty of writing correct verifiers.Source: §E.2 · p. 17

E.3. Case Study Comparing FLASH-THINKING and O1

This section compares FLASH-THINKING and O1 on two IMO Shortlist case studies, with prompt descriptions covering direct, coding-agent, and brute-force setups. The cases involve a 27-number sequence satisfying cyclic sorted arithmetic-progression constraints and a structured search for an integer with exactly 60 close divisors; O1 solves more variations than FLASH-THINKING.

E.3. Case Study Comparing FLASH-THINKING and O1

  • On IMO 2001 C5, FLASH-THINKING solved no variations while O1 solved 3/4; on IMO 2014 N2, FLASH-THINKING solved none while O1 solved all variations.Source: §E.3 · pp. 18, 20
  • O1 recognized self-describing numbers for C5 and pronic numbers for N2, while FLASH-THINKING made casework errors, missed the N2 pattern, and once found incorrect online results.Source: §E.3 · pp. 18–20

F.1. Chain-of-Thought Solver

  • For main results, the Chain-of-Thought prompt directly asks each model to solve the problem and specifies the answer format.Source: §F.1 · p. 21

F.2. Coding Agent

  • Coding-agent evaluation allows arbitrary code and illustrates it with a 22×22 rook configuration avoiding empty 5×5 squares.Source: §F.2 · p. 22

F.3. Bruteforce Solver

  • The brute-force solver prompt requires one code block that naively constructs a solution and permits only one attempt.Source: §F.3 · p. 24
  • The pure brute-force solver is instructed to generate unoptimized Python code for the n=27 cyclic triplet progression problem.The problem requires distinct real numbers whose consecutive triples, including wrap-around triples, form arithmetic progressions when sorted.Source: §F.3 · p. 24

3.5-SONNET

  • The 3.5-Sonnet search produced a 27-number sequence reported to contain distinct entries and satisfy each consecutive and wrap-around 3-term arithmetic-progression condition.The output lists the sequence, and the accompanying text confirms its distinctness and the progression conditions.Source: 3.5-SONNET · pp. 25–26

F.4. Brute+Infer Solver

  • 6985199471250 is reported as a positive integer with exactly 60 close divisors.An initial integer-by-integer search timed out; the follow-up evaluated combinations of the first few small primes raised to small powers.Source: §F.4 · pp. 27–28
Loading 2502.10197v2…