MathConstruct: Challenging LLM Reasoning with Constructive Proofs
Authors: Mislav Balunovic
Jasper Dekoninck
Nikola Jovanović
Ivo Petrov
Martin Vechev
Venue: ICML 2025 poster (2025)
Keywords: LLM
math
evaluation
benchmark
reasoning
Primary area: general_machine_learning->evaluation
TL;DR: A new benchmark of math olympiad problems for evaluating LLMs at constructive proofs

Abstract: 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 127 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 41\% of MathConstruct problems, highlighting its complexity and importance for LLM evaluation.

MATHCONSTRUCT:
Challenging LLM Reasoning with Constructive Proofs
Mislav Balunovićs 12
Jasper Dekoninck
Nikola Jovanovié
Ivo Petroy? Martin Vechev
Abstract
100%
MATH
(97.00))
While Large Language Models (LLMs) demon- strate impressive performance in mathematics, ex- isting math benchmarks come with significant limitations. Many focus on problems with fixed ground-truth answers, and are often saturated due problem simplicity or the viability of guessing or memorization. Crucially, they cap- ture only narrow subset of relevant math prob- lems. To address this research gap, we intro- duce MATHCONSTRUCT, a new benchmark of 126 challenging problems sourced from various math competitions, which targets constructive proofs, a widely encountered problem type re- quiring the construction of mathematical objects with specific properties. These proofs are par- ticularly suitable for LLM evaluation, as solu- tion correctness can be easily verified. Our au- tomated verifiers also enable MATHCONSTRUCT to generate problem variations, used to evaluate robustness. ofate-of-the-art LLMs solve only 54% of MATHCONSTRUCT problems, highlighting its complexity and importance for L.LM evaluation.
80%
AIME 2024
(86.70%)
60%
Average Accuracy
Robust Accuracy
40%
HILLT THINKING
20%
0%
Figure Accuracy of LLMs on MATHCONSTRRUT, high- lighting the difficulty of constructive proof'. We compute Robust Accuracy by requiring the model consistently solve problem across set of problem variations.
formalized proof generation, requires LLMs to generate proof's that can be verified by automated theorem provers such as Lean (de Moura & Ullrich, 2021). Unfortunately, even models explicitly fine-tuned for this task struggle to perform well (Xin et al., 2024). Furthermore, this approach does not fully leverage the strong natural language reason- ing capabilities of LLMs. This raises important question: Is there a class of proof-based problems that are both chal- lenging for LLMs and easy to verify for correctness?
1. Introduction
Evaluating the mathematical reasoning abilities of Large Language Models (LLMs) requires high-quality public benchmarks that accurately measure progress. As shown in Fig. 1, existing benchmarks, such as MATH (Hendrycks et al., 2021), are becoming increasingly saturated as state- of-the-art models improve, highlighting the need for more challenging evaluation tasks. Many complex mathematical problems involve proefs, which are a fundamental compo- nent of advanced reasoning. However. current benchmarks primarily focus on problems where LLM outputs can be directly compared ground truth answers, making them unsuitable for evaluating proofs. A promising alternative,
Constructive proofs One important class of proofs, com- monly appearing in real-world applications and advanced mathematical competitions, involves constructive proofs. These proofs establish mathematical result by explicitly constructing an object-such as a set, matrix, or graph- -tht that satisfies specific constraints.
For instance, one the most challenging problems from the 2022 International Mathematical Olympiad (IMO). shown in Fig. 2 (left), requires constructing an n matrix that maximizes a particular quantity. More generally, disproving conjecture often involves constructing a counterexample, as seen in Cantor's 's diagonal argument (Cantor, 1890). Simi- larly, proving a bound frequently requires constructing an object that achieves that bound, as the proof the Four Color Theorem (Appel Haken, 1989).
'Equal contribution 'Department of Computer Science, ETH Zurich FINSAIT, Sofia University "St. Kliment Ohridski", Corre- spondence to: Mislav Balunović <mislav balunovvbbl ehs.
Proceedings of the nd International Conference Machine Learning, Vancouver, Canada. PMLR 267, 2025. Copyright 2025 by the author(s).

---

MATHCONSTRUCT
Problem-IMO (aann--M--0005555 CB (n=6, k=7): Let Af = dd.......... The coloring "best" if colors some 3 of the diagonals of M green, and some other 3 of its diagonals red, so that no two diagonals the same color meet inside M. and "score". the number of intersection points red diagonals inside M. maximized. For n 6 the maximum score 7. Find one coloring that achieves this
Problem- IMO-2022-C8 [n=4, 25): Given 4, fill the hoard with permutation of integers between and n² such that there 25 so-called uphilf paths: the first cell the smaller than all its neighbors, (ii) each subsequent cell in the st- quence is adjacent to previous cell, and (il) in the cells in the sequence are in increasing order.
be convexc n-gon,
and
written
LLM
LLM
def verify- 1000-2822-CB(conSEEEEE
def verl 1---IM0--255550 2805-c8 af intersecl. L. const))))::: return false it red. red.grrennconstr !- (6-3, 6-31:
if din(constr) I= (4, 4): return False if (const)) !- (1, 4+4):
15
5
10
11
14
6
12
13
7
return
return False
return paths (consrr) 25 /
return intersectionsiconste
L.M construction
LLM construction
Figure 2: Two sample problems from MATHCONSTRUCT, each consisting of a natural language statement and verifier function that returns boolean value indicating the validity of a proposed construction. The ability to easily generate problem variations (values colored in blue and brown), the complexity of the required constructions, and the difficulty of the problems make MATHCONSTRUCT well-suited for evaluating LLMs' reasoning abilities.
Constructive proofs are particularly well-suited for LLM benchmarking as coming up with valid constructions is often difficult for humans, and thus likely to also challenge the models. Yet, verifying if a proposed construction satisfies the problem constraints is usually straightforward, enabling the use of automated verifiers judge model responses.
By generating variations of each problem, we evaluate the models on 475 distinct problem instances. Even with access to code execution, these models struggle with MATHCONSTRUCT. The best model achieves only 54% accuracy, as shown in Fig. 1; complete results are pre- sented in Table 2. We further provide thorough analysis of LLMss failure modes, and study the impact of different variations, problem brute-forceability, and data contami- nation on performance. Our code is available at https: //github.... com/ hotm/eth-see sri ma thconstruct.
Our benchmark: MATHCONSTRUCC Leveraging this, we introduce MATHCONSTRUUC, a new benchmark de- signed to evaluate LLMs' reasoning capabilities through constructive proofs. MATIICONSTRUCT consists of 126 unique problems sourced from olympiad-level mathemat- ics competitions. Each problem is encoded as a natural language statement and a corresponding verifier function that determines the correctness of a proposed construction (see Sec. for details). In Fig. 2, we illustrate two sample problems from MATHCONSTRUCT.
Contributions
Our key contributions are:
We propose MATHCONSTRUCT, benchmark of 126 challenging constructive problems (Sec. 3).
We conduct rigorous evaluation of 14 state-of-the-ar LLMs on MATHCONSTRUCT, demonstrating its diffi- culty and significance for LLM evaluation (Sec. 4.1).
Beyond its challenging nature and ease of verification, MATHCONSTRUCT has several features that make it par- ticularly valuable for LLM evaluation. Most importantly, all problem statements are phrased symbolically, enabling systematic generation of variations that test models' robust- ness to small changes in problem parameters. Second, the required constructions often involve complex mathemati- cal objects (c.g., matrices, colorings) rather than simple numerical answers, making guesswork and memorization less effective. Finally, our rigorous hand-curation process (detailed in Sec. 3) ensures high problem quality, robustness against brute-force solutions, and broad coverage across mathematical domains.
We provide a detailed analysis of LLM performance on MATHCONSTRUCT, including the impact of various factors on model performance (Secs. 4.2-4.5).
2. Related Work
This section reviews related work on mathematical bench- marking and constructive proofs in machine learning.
Easier math benchmarks Most math benchmarks for LLMs focus on problems where the final answer is numer- ical value or algebraic expression that can be compared with fixed ground truth. Among these, early benchmarks such as GSM8K (Cobbe et al., 2021) and MATH (Hendrycks et al., 2021) have been saturated by recent models (Jaech et al., 2024; DeepSeek-AL, 2025). More advanced problem sets, such as AIME 2024!, are more difficult, yet ota the-art models still solve s887.
Evaluation In Sec. 4, we evaluate bate-off-the-art LLMs on MATHCONSTRUCT, including GPT-4o and 03- MINI (Jaech et al., 2024), the GEMINI family (Reid et al., 2024), and the CLAUDE family (Anthropic, 2024).
See American Invitational Mathematics Examination
2

---

MATHCONSTRUCT
Olympiad-based benchmarks To introduce more com- plexity, newer benchmarks such as OlympiadBench (He et al., 2024), Omni-MATH (Gao et al., 2024), and HARP (Yue et al., 2024) incorporate olympiad-level prob- lems, including image-based and multilingual problems. However, these benchmarks still rely on fixed-answer ver- ification, often using an LLM as a judge for compari- son. In contrast, MATHCONSTRUCT focuses on construc- tive proofs rather than verifying predefined answers, pro- viding a more challenging evaluation of reasoning abili- ties. This difference in evaluation methodology is high- lighted in problem statement that appears both in Omni- Math and MATHCONSTRUCT. Specifically, in the prob- lem on the left of Fig. 2, Omni-MATH considers a lower bound, 2n(n - 1) + 1, as the correct answer, whereas MATIICNNSTRUCT requires models construct an object that achieves the lower bound, which is significantly more challenging in this case.
making them susceptible to memorization. While most prob- lems in MATHCONSTRUCT
also NP-Hard, they ensure tractability for human solvers using pen and paper, as they originate from real mathematics competitions. This makes MATHCONSTRUCT a more direct evaluation of reasoning ability in mathematical contexts.
Constructions with machine learning Machine learning has also been previously applied to mathematical object construction and pattern discovery. Wagner (2021) use re- inforcement learning to find counterexamples that disprove conjectures in graph theory. Other works leverage neural networks for combinatorial optimization (Bello et al., 2017; Gasse et al., 2019). More broadly, machine learning has been used to identify relationships between mathematical objects, as seen in Davies et al. (2021) and Davila (2024).
3. MATHCONSTRUCT
Private benchmarks Several private benchmarks, such as FrontierMath (Glazer et al., 2024) and LastExam (Phan et al., 2025), have recently been introduced. Although Fron- tierMath includes problems that require more complex ver- ification methods, the private nature of these benchmarks prevents large-scale use and makes it difficult to evaluate the progress of the field as a whole.
Constructive proofs are a powerful tool for mathematicians, but turning these into a benchmark for evaluating the rea- soning abilities of LLMs requires significant effort. In this section, we deseribe our approach for the creation of a reliable benchmark of difficult constructive proof prob- lems, detailing the key steps: problem selection (Sec. 3.1), problem encoding (Sec. 3.2), and post-hoc problem review (Sec. 3.3). Further details on the development process are given in App. A.
Benchmarks with variations None of the above bench- marks incorporate problem variations, even though their value has been acknowledged in prior work. In partic- ular, recent efforts in related domains, such as GSM- Symbolic (Mirzadeh et al., 2024), Putnam-Axiom (Gulati et al., 2024), and UTMath (Yang et al., 2024) use symbolic problem reformulation. MATHCONSTRUCT aims to extend this line of work by applying variations to problems that require the construction of complex mathematical objects.
3.1. Problem Selection
As a first step in the creation of MATHCONSTRUCT. our team consisting of students with significant experience with math competitions preselected a preliminary set of construc- tive proof problems. To ensure quality, the problems were exclusively sourced from reputable high-level mathematics competitions, including high-school olympiads, undergradu- ate contests, and national high-school competitions. In total, our team read around 3500 problems from archives of 20 different competitions, selecting 158 possible problems that met our relevance and quality criteria.
Formal math benchmarks Another category of bench- marks evaluates formal theorem proving, requiring solutions in languages such as Lean (de Moura & Ullrich, 2021). Ex- amples include miniF2F (Zheng et al., 2022), FIMO (Liu et al., 2023), and PutnamBench (Tsoukalas et al., 2024). Despite specialized training (Xin et al., 2024), LLMS strug- gle to solve more than a few problems in this environment, indicating significant room for improvement.
Problem selection criteria Our criteria were as follows:
Difficult construction: For MATHCONSTRUCT to be nnture-proof and pose a challenge to current and future models, obtaining the required construction should in- volve non-trivial reasoning, and constitute the majority of the official solution to the competition problem.
Logical reasoning benchmarks Orthogonally, a large body of work evaluates logical reasoning in LLMs on log- ical puzzles and satisfiability problems (Gui et al., 2024; Mittal et al., 2024; Ma et al., 2024), many of which are NP-Hard (Fan et al., 2024). Examples include puzzles such as the knapsack problem and Sudoku. These tasks primarily test algorithmic problem-sol solving rather than mathematical reasoning. Furthermore, the problems are often well-known,
Complex objects: To further ensure difficulty and re- duce the probability of lucky guessing the answer, the required object should be non-trivial, i.c., the space of possible constructions should be large. In particular, we generally avoid problems where the result of the construction is a single integer.
3

---

MATHCONSTRUCT
objects satisfying some constraints. Finally, Max-problems originally ask for the maximum (or minimum) value of function of object. Often, these are solved by first prov- ing lower (resp. upper) bound and then constructing an object that achieves this bound. the second part is suf- ficiently difficult, these problems are good candidates for MATIIONSTTUUT Importantly, when adapting problems to become constructive proofs. we confirm that the quality and diffieulty criteria above hold, even after the necessary problem modifications.
Symbol ic problem statement P
problem "yind an n x matrix of rank I 3 with zeros on the main diagonal and positive reals off the diagonal."
Concrete parameters 0 parameters = ("a": 10)
Verification function Vo def verify (construction):
if dim (construcction) !- (n, n):
return 0, "Wrong dimensions" if any mny(consttuctionllll1s return 0, "Non-zero diagonal" if any (ccosstructoo <- 0)
1= 0):
3.2. Math Construction Problems
We now discuss the formalization of construction problems and their encoding into format that can be used for pro- grammatic evaluation.
return 0, "Off-diagonal <= 0"
if matrix_ree (construction) > 3:
return 0, "Rank > 3"
return 2, "Correct"
Definition 3.1 (Construction Problem). construction problem is tuple (P, 0, Va) where / symbolic prob- lem statement in natural language, 0 are concrete parameters that replace symbolic variables in the problem statement, and Vo: O - (0, 1} is a verification function that takes an object and checks whether it satisfies the constraints of the problem. A valid solution or a constructive proof for this problem any object o E such that (g( = 1.
Variation generator def generate_varlee (orrtteo_vriatio)))::
return :"n": random. randint (6, }
Formatting instructions
format "Present your construction on as matrix in LaTee enclosed in [boxed(] [
Figure 3: A problem encoding consisting of a symbolic problem statement P, concrete parameters 0, and a verifica- tion function Ve. We also implement variation generator, and provide formatting instructions for the construction.
Each problem is encoded as single Python file, containing all of its components P, 0, and Vg. Additionally, the file includes a variation generator function which generates a set of variations of the problem by plugging in different values for the parameters 0, and formatting instructions that instruct the model output the solution in a specific format.
Tractable verification: On the other hand, the verifi- cation function must be straightforward to implement relative the problem difficulty, and feasible run.
An example of an encoded MATHIONNSTUUC problem is given in Fig. 3. Here, the problem statement is P = "Find an n x matrix... ", the parameters are 0 = {n: 10). and the verification function is given by
Variations: To distinguish genuine reasoning from memorization or lucky guessing, we prioritize prob- lems that allow for multiple variations by altering pa- rameters. In Sec. 4 we introduce robust accuracy, quiring models to solve multiple variations to be con- sidered successful who knows the general solution can solve each varia- tion trivially, this criterion ensures that the model has a similar level of understanding.
Vo rank 3 0 =O 0).
When solving the problem, the model is given concretized problem statement obtained by replacing the parameters in the problem statement P with concrete parameter values 0. Similar to human contestants, the model does not have access to the verification function Vog.
given problem. Since human
Adapting different problem types The most common problems MATHCONSTTUCC are Any-problems, which ask for any object satisfying the given constraints. How- ever, several other problem types can be adapted to fit our criteria. For example, Inf -fooblosssss originally ask for proof that there are infinitely many objects that satisfy the given constraints- often require coming up with an infinite solution class, whose knowledge can be demon- strated by producing & fitting constructions for > oo. Similar reasoning holds for All-problems, which ask for all
We now further discuss each of the problem components.
Symbolic problem statement While many problems are originally stated with concrete values, they can often be generalized to obtain symbolic problem statement P. We do this for every problem where it is possible, replacing concrete values with symbolic parameters 0, allowing us to plug in different values for the parameter. For example, any positive integer can replace parameter n in the problem statement in Fig. 3.

---

MATHCONSTRUCT
Verification In our implementation, the verification fune- tion Vo takes construction and returns tuple (c, f) where is boolean indicating whether the construction satisfies the constraints of the problem, and f is a detailed feedback string that when c = false explains why the construction is incorrect. For example, in the problem in Fig. 3, the verification function checks that the matrix has the correct dimensions, the diagonal is zero, the off-diagonal elements positive, and the rank is most 3. We use the feedback strings during our review process for manual quality checks (see Sec. 3.3). Following the criteria from Sec. 3.1, we see that despite the significant difficulty of the problem in Fig. 3, the verification function is simple to implement and run, and the feedback is straightforward to understand.
Table I: Summary of MATIICONSTRUCT constructive proof problems by their category and type.
Type
Any-
All-
Inf-
Max-
Σ
Category
Combinatories
19
6
18
44
Algebra
11
5
7
24
Number Theory
26
7
15
6
54
Geometry
4
0
0
0
4
Σ 61
18
17
31
126
implementation. Next, each author was asked to ensure that their problem solvable by a human using pen and paper, to ensure that we are testing reasoning, and not merely cal- culation skills. We remark that some of our problems may include more calculation than typical in human competi- tions (e.g., writing the complete X n matrix instead of simply describing it)-however, this step is trivial once the correct insight for the problem is found. Finally, in a peer review process, each problem was reviewed by at least one other team member, checking that the problem statement sound and clear, that the verification function is feasible and returns informative feedback in case of errors, and that the problem is sufficiently challenging and of high quality.
Variations Given a problem, humans can typically find a general solution that works for all parameter values. For example, to solve the problem in Fig. 3 (and the majority of our problems), one can find general procedure that works for any n. Most popular benchmarks (Hendrycks et al., 2021; Gao et al., 2024; He et al., 2024) do not have symbolic variations, meaning it is difficult to evaluate whether the model can generalize to similar problems or simply guessed the answer. Instead, we create a number of variations for each problem, allowing us to study the robustness of the model changes in the problem parameters.
Definition 3.2 (Problem Variations), Problem variations are a set of construction problems that share the same symbolic problem statement P and verification function Vo, but have different problem parameters 01, 02 O2....,0 Ok.
Automated quality checks Complementing manual re- view, we also implemented automated checks. First, we verified that all problems are solvable by an LLM when explicitly given the solution. This verifies that the format- ting instructions are unambiguous and that our parser and verifier error-free. Second, we flagged for additional review all problems where our solution is longer than 4000 characters, as LLMs should not be significantly hampered by the difficulty of outputting large amounts of text. Finally, we implemented a code agent that flags problems that are solvable using brute-force approach, as we want to ensure that each problem is only solvable via genuine reasoning.
Formatting and parsing Since the mathematical objects involved in constructive proofs have wide variety of types, we also provide formatting instructions for each problem which can be used to prompt the model to output the solution in a specific format. Furthermore, we create a specialized parser, detailed in App. B, that can parse arbitrary combi- nations of lists, matrices, and ЕТmК objects from natural language solutions. By default, models evaluated on our benchmark receive detailed feedback from our parser, al- lowing them to correct their solutions over multiple rounds, which reduces the risk of syntax errors.
Final set of problems Most issues above were resolved by revising the problem statement the set of variations. Dis- carding the 32 problems that had unresolvable issues, we ar- rived at a final set of 126 problems in M MATHCONSTRUCT- a detailed overview of our sources and the number of prob- lems per source is given in App. C.
3.3. Problem Review
We performed a review of MATHICNNSTRUCT problems, in each stage discarding problems that did not meet our quality criteria and revising those that could be improved.
In Table I summarize MATHCONSTRUCH across differ- ent problem categories (e.g., Combinatorics) and types, as introduced above (e.g., Any-problems). We see that the prob- lems are well-distributed across categories, and that around half of the problems are Any-problems, the type that most closely illustrates constructive proofs. The other half was obtained by adapting other problem types to fit our criteria.
Manual quality checks First, each problem author was tasked with implementing a generic solution function that computes valid constructions for the problem. Additionally, extensive unit tests were implemented to check each prob- lem's 's verification and solution functions, ensuring correct
5

---

MATHCONSTRUUT
4. Experimental Evaluation
Table 2: Main results of our evaluation. We measure cost in
USD, and report both average and robust accuracy in %.
We evaluate a diverse set LLMs on MATHICONSTRUCT across various settings. We present our main results on rea- soning models (Sec. 4.1), results with code agents (Sec, 4.2), analysis of common failures (Sec. 4.3), effects of con- tamination (Sec. 4.4), and robustness of the models to varia- tions (Sec. 4.5). For readability, we adopt shortened names for some models. You can find this and other details of the experimental setup in App. D.
Model
Avg
Robust
Cost
LLAMA-3.1-4055
3.17
1.59
1.99
GPT-4O-MINI
3.77
1.59
0.32
LLAMA-3.3-70B
3.77
1.59
0.67
3.5-HAIKU
3.37
1.59
1.37
GPT-40
3.57
0.79
4.62
3.5-SONNET
4.17
0.79
4.80
4.1. Main Results
QWEN2.5-728
6.35
1.59
2.24
FLASH
11.57
3.17
N/A
We evaluate 14 state-of-the-art models on our benchmark and summarize the results Table 2, which expands on Fig. 1. Each model tasked with solving the problems in MATHCONSTRUCT while adhering to specific formatting guidelines for their responses (see App. for details). To ensure correct parsing, models receive back from the parser, allowing them to refine their answers. Additional experiments on the use of feedback from the verification function are provided App. F.2.
QWQ
13.89
7.14
8.34
RI-LLAMA-70B
19.51
7.94
15.23
OI-MINI
25.46
10.32
51.49
27.05
11.11
N/A
01
41.34
23.02
434.08
rounds of feed-
03-MINI
53.77
34.92
71.14
FLASH"
We report two key metrics: average accuracy, which first computes accuracy over all variations of problem and then averages these values across all problems, and robust accuracy, which considers problem solved only if all its variations are answered correctly. The latter metric re- flects a stricter evaluation, analogous to how human who solves the general form of a problem can solve instanti- ations. Additionally, we provide the total cost running each model on the benchmark, measured in USD.
16%
3.5-SONNET
Qwax-2.5-72B
Accuracy
GPT-4o
12%
3.5-HArku
LLAMA--.8-778
8%
4%
10a
10a
Cost
Results Among all models, 03-MINI performs best, achieving 53.8% accuracy and 34.9% robust accuracy, out- performing the second-best model, 01, by a 12% margin. Among non-reasoning models, FLASH leads with 11.3% accuracy and 3.2% robust accuracy, significantly ahead of other non-reasoning models.
Figure 4: Cost and accuracy of models with or without code execution. Future cost of FLASII is estimated (now frree).
Code agents We first evaluate the performance of models with access a Python interpreter. Specifically, each model execute Python code up to four times per problem to generate solutions, verify reasoning steps, perform cal- culations. The output of each execution is fed back to the model, allowing it to iteratively refine its reasoning, Fig. 4 shows how accuracy and cost change when models are al- lowed execute code. Compared to their base performance from Table 2, both accuracy and cost increase significantly. Most models roughly double their accuracy, the expense of fivefold increase in cost. Notably. 5.5-SONNET im- proves from 5% to 15.3% accuracy. FI.ASH still achieves the highest accuracy in this setting, reaching 17.5%.
Despite ol's impressive performance, it incurs high cost, requiring USD 443.3 to complete the benchmark- three times the combined cost of all other models. In contrast, GRMINI models are currently free (at limited rate), making them more cost-effective alternative.
Notably, all models struggle with solving every variation of problem, as reflected in the robust accuracy scores, which are approximately half of the average accuracy values. This highlights the difference between human and model performance, as humans can often solve all variations problem once they have solved the problem.
Brute-force solutions Some problems in our benchmark are susceptible to brute-force methods, as identified during our review process (Sec. 3.3). To evaluate this, we tested brute-force agents and adjusted problems that allowed triv- brute-force solutions. We considered two brute-force
4.2. Alternative Evaluation Settings
We explore alternative evaluation settings on our benchmark and analyze their effects.
6

---

MATHCONSTRUCT
50%
03-MINI (before)
QwQ (before)
40%
O3-MINI (after)
QwQ (after)
30%
20%
H Unparseable
10%
0%
Correct
Incorrect
Format
Reject
No Solution
Error Type
Figure 5: Error types of models before and after parser feedback.
Table 3: Accuracy of Brute-Force on MATHCONSTRUCT.
Fig. illustrates the distribution of error types for both 03- MINI and QwQ before and after parser feedback. A key ob- servation that 03-MINI frequently produces unparseable answers, but significantly benefits from parser feedback. When reprompted, 03-MINI successfully incorporates the feedback, leading to notable accuracy improvement of +15%. This suggests that as mathematical benchmarks increase in complexity, models should be systematically provided with parser feedback to ensure their capabilities are accurately evaluated.
BRUTE
BRUTE+INFER
Model
Avg
Robust
Avg
Robust
GPT-40
6.35
0.79
10.78
3.17
3.5-SONNET
8.13
1.59
16.67
5.56
approaches: pure brute-force, where the model is explicitly instructed to generate a brute-force solution, and brute-force inference, where the model is encouraged to solve smaller instances in a brute-force manner and then generalize findings to solve the full problem. To facilitate the latter strategy, allow the model refine its solution up times, using feedback from parser adapt its strategy.
Both models frequently fail provide solution in their ini- tial attempts, either by omitting the \boxed environment getting stuck. However, in many cases, parser feedback enables the models to correct these mistakes by trying again or making an educated guess. Interestingly. QwQ exhibits a distinet failure pattern: in 10% of its errors, explicitly rejects the premise of the question, asserting that no solu- tion exists its final answer. Moreover, unlike 03-MINI, QwQ does not improve its parseability after receiving feed- back, highlighting its inability to understand and follow instructions. In App. E.3, we additionally perform case study comparing two models, 01 and FLASH- AASHHTHING TING on several problems where 01 demonstrates stronger pattern recognition capabilities, while FLASH- THINKING does not recognize patterns and resorts to exhaustive search.
Table 3 presents results for these brute-force agents the final version of our benchmark. The pure brute-force method (BRUTE) achieves less than 8% accuracy. A man- ual review indicates that most correct solutions either in- volve non-trivial reasoning steps or arise from luck. In contrast, the brute-foree inference agent (BRUTE+INFER) performs significantly better, reaching up 16.7% accu- racy-surpassing the code agent from Sec. 4.2. This agent frequently discovers patterns by generalizing from smaller instances, effectively solving problems in more structured manner. As a result, we did not remove problems that this method solved, as they demonstrate meaningful reasoning rather than brute-force execution.
4.4. Contamination Analysis
4.3. Error Analysis
We further investigate the impact of data contamination on performance, which is particularly important since olympiad problems are commonly included in training datasets. As- sessing contamination is crucial for verifying both the reli- ability of benchmark results. Given the modifications and variations we introduced to the problems, we expect mini- mal contamination. To confirm this, we follow Dekoninck et (2024) and compare model performance on the origi- nal benchmark against rephrased version, where problem statements have been rewritten by GPT-40.
By leveraging the detailed feedback given by our parser and verification methods (described in Sec. 3.2), we conducted detailed error analysis of the models. Specifically, we categorized the errors into the following types: unparseable, where the model output could not be parsed, solution, where the model does not provide solution, reject, where the model rejects the question's premise and states there no solution, format,, where the output did not correctly follow the formatting instructions, and incorrect, where the solution does not satisfy the problem constraints.

---

MATHCONSTRUCT
30%
100%
GOLD
Actual Performance
FLASH-THINKIN
75%
3.5-SONNET (BRUTE)
20%
Accuracy
Equal Performance
50%
10%
25%
0%
0%
0%
10%
20%
30%
0
1000
2000
3000
1000
Reference Performance
String Length of the Gold Solution
Figure 6: Contamination analysis models on the bench- mark and its rephrased equivalent.
Figure 7: The effect of problem variations on accuracy.
In Fig. 6, we present the results for all models except 01, which was excluded due to cost constraints, We find that model performance on the rephrased benchmark closely matches performance on the original, suggesting minimal contamination. However, -MINI exhibits a small but no- ticeable deviation. Using bootstrapping, we estimate the 20 confidence interval of this deviation be 4.7 = 3.2%, which is small, but statistically significant. This suggests that 01 -III may slightly underperform in real-world sce- narios compared to its benchmark results. Nevertheless, the effect does not alter its ranking among the evaluated models.
review process (Sec. 3.3), where variants with this behavior were generally excluded from MATHCONSTRUCT.
The FLASH-THIEE THINKING results follow a similar pattern: achieves nearly 100% on trivial variations but struggles with larger ones. As variant size increases, accuracy declines due to the need generate long responses and perform operations large numbers. both of which increase the risk of errors. As noted in Sec. 3.3, our problem review process included a step where we manually reviewed variant size and
aimed to keep it within a reasonable range (see App. C for histogram of original problem variant sizes and App. E. for the distribution of model output tokens). Within this range, FLAAH-THINKING is fairly consistent, implying well- balanced variant difficulty in MATHCONSTRUCT.
4.5. Effect of Problem Variations
Finally, to investigate the impact of problem variations on model performance, we test the robustness of FLASH- THINKING against a range of extreme variations. Specif- ically, we select 10 problems where the model performs reasonably well and evaluate its accuracy on 24 vari- ations of each. These variations purposefully include both trivially small cases and impractically large ones scenarios intentionally excluded from the default version of MATHCONSTRUCT. For reference, we also include 3.5-SONNET (BRUtE), the brute-forcing agent introduced in Sec. 4.2. As proxy for variant difficulty, we define variant size the string length of our (GOLD) solution.
5. Conclusion
In this work, we introduced MATHCONSTRUCT, novel benchmark designed to evaluate the mathematical reason- ing of LLMs through constructive proofs. Unlike existing benchmarks, MATHCONSTRUCT uniquely combines the challenge of constructing valid mathematical objects with the case of their correctness verification, creating chal- lenging set of tasks for LLM evaluation. Starting from 126 curated problems, we generated 475 instances by systemati- cally varying key parameters the original problem state- ments. Our extensive evaluation of 14 LLMs on these tasks revealed that the most advanced models struggle signif- icantly with these tasks. Overall, believe that by focusing construction problems, MATHCONSTRUCT pushes the boundaries of mathematical reasoning benchmarks, offering a valuable resource for driving future advancements.
In Fig. 7 we show the accuracy of each model on these varia- tions, grouped by their size. As expected, the GOLD solution always achieves 100% accuracy. This reflects the perfor- mance of human contestant who has solved the problem in its general form and can apply that solution to any variation. The brute-force agent is only successful on very small vari- ations, where the problem often degenerates into trivial form. For example, setting
2 in the problem in Fig. 3 requires a 2 x 2 matrix of rank < 3, which holds for any 2 x matrix. This illustrates the importance of our problem
8

---

MATHCONSTRUCT
Impact Statement
language models. CoRR, abs/2405.16225 2024. doi: 10 1044850/AAXXX.22455.668811 URL https://do org/10
MATICONSTTUUCT has the potential to significantly im- pact the field of AI and mathematics. By providing chal- lenging benchmark of constructive proofs, it can help re- searchers and practitioners evaluate the reasoning capabil- ities of LLMs and guide the development of more robust models. Furthermore. our benchmark is the first step to- wards evaluating LLMs on broader range of math prob- lems, which can lead to more comprehensive evaluations and subsequent improvements model performance.
Fan, L.,, Hua, W. Li, L.,, Ling, H., and Zhang, Nphard- eval: Dynamic benchmark on reasoning ability of large language models via complexity classes. In ACL (!), pP. 4092-4114 Association for Computational Linguisties, 2024.
Gao, B., Song, F., Yang, Z., Cai, Z., Miao, Y., Dong, Q., Li, L., Ma, C., Chen, L.., Xu, R., Tang. Z.,, Wang, B., Zan, D., Quan, S., Zhang, G., Sha, L.,, Zhang, Y., Ren, X., Liu, T., and Chang, B. Omni-moalte math: A universal olympiad level mathematic benchmark for large language models. CoRR, abs/2410.07985, 2024.
References
Fasthtml, 2025. URL www.tttttt///tttm /ewttps:/www.... fastht.m..
Anthropic, A. Claude 3.5 sonnet model card addendum. Claude-3.5 Model Card, 3:6, 2024.
Gasse, M., Chételat, D., Ferroni, N., Charlin, L., and Lodi, A. Exact combinatorial optimization with graph convo- lutional neural networks. In NeurIPS, pp. 15554-15566, 2019.
Appel, K. I. and Haken, W. Every planar map is four colorable, volume 98. American Mathematical Soc., 1989.
Bello, I., Pham, H., Le, Q. V., Norouzi, M., and Bengio, S. Neural combinatorial optimization with reinforcement learning, In ICLR (Workshop). OpenReview.net, 2017.
Glazer, E.,, Erdil, E., Besiroglu, T., Chicharro, D., Chen, E., Gunning, A., Olsson, C. F., Denain, J., Ho, A., de Oliveira Santos, E., Järviniemi, O., Barnett, M., San- dler, R., Vrzala, M., Sevilla, J., Ren, Q., Pratt, E., Levine, I.., Barkley, G., Stewart, N., Grechuk, B., Grechuk, T., Enugandla, S. V., and Wildon, M. Frontiermath: bench- mark for evaluating advanced mathematical reasoning in AL arXiv, 2024.
Cantor, G. Ueber eine elementare frage der man- nigfaltigketislehre Jahresbericht der Deutschen Mathematiker- MaaheenatkerrVeeeiiniggnn 1:72-78, 1890.
Cobbe, K., Kosaraju, V., Bavarian, M., Chen, M., Jun, H., Kaiser, I.,, Plappert, M., Tworek, J., Hilton, J., Nakano, R., Hesse, C., and Schulman, J. Training verifiers to solve math word problems. CoRR, abs/21
Gui, J., Liu, Y., Cheng, J., Gu, X., Liu, X., Wang, H., Dong, Y., Tang, J., and Huang, M. Logicgame: Benchmarking rule-based reasoning abilities of large language models. CoRR, 0as/2408.11778 2024.
2021.
Davies, A., Velickovic, P., Buesing, L., Blackwell, S.,
Zheng, D., Tomasev, N., Tanburn, R., Battaglia, P. W., Blundell, C., Juhász, A., Lackenby, M., Williamson, G., Hassabis, D., and Kohli, P. Advancing mathematics by guiding human intuition with Al. Nat., 600(7887):70-74, 2021.
Gulati, A., Miranda, B., Chen, E., Xia, E., Fronsdal, K., de Moraes Dumont, B., and Koyejo, S. Putnam- AXIOM: A functional and static benchmark for measur- ing higher level mathematical reasoning. In The 4th Work- shop Mathematical Reasoning and Al at NeurlPS 24, 2024. URL htt.t:tt//penteeeeeeeeee wwwp///epeeeeeeeeeeepee/ee..eeee net forum? Id=YXnw1Ze0yf
Davila, R. Artificial intelligence and machine learning gen- crated conjectures with txgraffiti. CoRR, Abs/2407.027331 2024.
He, C., Luo. R., Bai, Y., Hu, S., Thai, Z. L., Shen. J., Hu, J., Han, X., Huang, Y., Zhang, Y., Liu, J., Qi, L., Liu, Z., and Sun, M. Olympiadbench: A challenging benchmark for promoting AGI with olympiad-level bilingual multi- modal scientific problems. In ACL (1), pp. 3828-3850. Association for Computational Linguistics, 2024.
de Moura, and Ullrich, S. The lean 4 theorem prover and programming language. In CADE, volume 12699 of Lec- ture Notes in Computer Science, pp. 625-635. Springer, 2021.
Deepseck-rl: DeL bility in Ilms via reinforcement learning. arXiv preprint MXXv:22001.1294, 2025.
Incentivizing reasoning capa-
Hendrycks, D., Burns, C., Kadavath, S., Arora, A., Basart, S., Tang, E.,, Song, D., and Steinhardt, J. Measuring mathematical problem solving with the MATH dataset. In NeurlPS Datasets and Benchmarks, 2021.
Dekoninck, J., Müller, M. N., and Vechev, M. T. Con- stat: Performance-hasee contamination detection in large

---

MATHCONSTRUCT
Jaech, A., Kalai, A., Lerer, A., Richardson, A., Bi-Kishky, A., Low, A., Helyar, A., Madry, A., Beutel, A., Car- ney, A., et al. Openai ol system card. arXiv preprint arXiv:2412.16720, 2024.
theorem proving in Ilms through large-scale synthetic data. CoRR, Abs/2405.143333 2024.
Yang, B., Yang, Q. and Liu, R. Utmath: Math evaluation with unit test via masoning-to-coddin thoughts. CoRR, Abs/2411.0722) 2024.
Liu, C., Shen, J., Xin, H., Liu, Z., Yuan, Y., Wang, H., Ju, W., Zheng. C., Yin, Y., Li, L., Zhang, M., and Liu, Q. FIMO: A challenge formal dataset for automated theorem proving, CoRR, (2//2309.04299 2023.
Yue, A. S., Madaan, L., Moskovitz, T., Strouse, D., and Singh, A. K. HARP: A challenging noman-annnotate math reasoning benchmark. CoRR, abs/2412.08819, 2024.
Ma, K., Du, X., Wang, Y., Zhang, H., Wen, Z., Qu, X., Yang, J., Liu, J., Liu, M., Yue, X., Huang, W., and Zhang, G. Kor-bench: Benchmarking language mod- els on Knowledge-orthoognaal reasoning tasks. CoRR, abs/2410.06526, 2024.
Zheng, K., Han, J. M., and Polu, S. minif2f: a cross-system benchmark for formal olympiad-leve mathematics. In ICLR. OpenReview.net, 2022.
Mirzadeh, S., Alizadeh, K., Shahrokhi, H., Tuzel, O., Ben- gio, S., and Farajtabar, M. Gsm-symbolic: Understand- ing the limitations of mathematical reasoning in large language models. CoRR, abs/2410.05222 2024.
Mittal, C., Kartik, K., Mausam, and Singla, P. Puzzlebench: Can Ilms solve challenging first-order combinatorial rea- soning problems? CoRR, abs/2402.02611, 2024.
Phan, L.,, Gatti, A., Han, Z., Li, N., Hu, J., Zhang, H., Shi, S., Choi, M., Agrawal, A., Chopra, A., Khoja, A., Kim, R., Hausenloy, J., Zhang, O., et al. Humanity's ' last exam. arXiv, 2025.
Reid, M.. Savinov, N.. Teplyashin, D., Lepikhin, D., Lilli- crap, T. P., Alayrac, J., Soricut, R., Lazaridou, A., Firat, O., Schrittwieser, J., Antonoglou, I., Anil, R., Borgeaud, S., Dai, A. M., Millican, K. Dyer, E., Glaese, M., Sottiaux, T., Lee, B., Viola, F., Reynolds, M., Xu, Y., Molloy, J., Chen, J., Isard, M., Barham, P., Hennigan, T., Mcllroy, R., Johnson, M. Schalkwyk, J., Collins, E., Rutherford, E., Moreira, E., Ayoub, K., Goel, M., Meyer, C., Thornton, G., Yang, Z., Michalewski, H., Ab- bas, Z., Schucher, N., Anand, A., Ives, R., Keeling, J., Lene, K., Haykal, S.. Shakeri, S., Shyam, P., Chowd- hery, A., Ring, R., Spencer, S., Sezener, E., and et al. Gemini 1.5: Unlocking multimodal understanding across millions of tokens of context. CoRR, 2as/2403.05530, 2024. doi: 10.4855/ARRXVV.400..5555 //doi. org (8550///5XX.. 2403.05530.
URL https: 05530.
Tsoukalas, G., Lee, J., Jennings, J., Xin, J.. Ding, M., Jen- nings, M., Thakur, A., and Chaudhuri, S. Putnambench: Evaluating neural theorem-proved on the putnam mathe- matical competition. CoRR, abs/2407.111244 2024.
Wagner, A. Z. Constructions in combinatories via neural networks. CoRR, abs/2104.1455 145166, 2021.
Xin. H., Guo, D., Shao, Z., Ren, Z., Zhu, Q.. Liu, B., Ruan, C., Li, W. and Liang, Deepseek-prover Advancing
10

---

MATHCONSTRUCT
A. Dataset Development Workflow
Here we describe our workflow for developing the MATIICONSTRUCT benchmark, elaborating on the details presented in the main text (Sec. 3).
Problem selection The first part of our workflow described in Sec. 3.1 is the selection of suitable problems from existing competitions. We assigned particular competitions (possibly splitting by year) to different members of our team, and each member selected problems from the assigned competitions according to the criteria described in Sec. 3.1. Overall we examined around 3500 problems from 20 different competitions. However, many of these problems were immediately discarded as they do not contain a constructive component (e.g., almost all geometry problems). Overall, this phase yielded at least 1 158 problems. Note that sometimes this step involved rephrasing the problem statement to make it more suitable for our benchmark.
Problem encoding The second part of our workflow relates to formalizing the problems and encoding them into format that can be used for evaluation, as discussed in Sec. 3.2. Each problem is encoded in a single Python file, into an object of type Problem. The first part of the object is a configuration that contains metadata about the problem such as the problem statement, formatting instructions for presenting the solution, the parameters, the source of the problem, parameters the original version of the problem, and the original solution. Additionally, the configuration contains a list of tags that describe the type of the problem and its relationship to the original version (is it simplified, generalized, etc.). In Fig. 8 we show example of this configuration for the problem from the IMC 2012 competition mentioned earlier in the paper in Sec. 3.2.
config ProblemConfigl
Lame-Probblee..gtttnnnaaLL _fil__)
3
4
wwwp://sssnettttttttttaaaaaaeeea (),
parameters=(".""
source-" 2012 P2",
7
origginai_parramtteerss<"""""" 7/,
8
.pdE", pdf",, (Tgg Tag.FIND MAX MIN, Tag. (ag.II_SSIMPLFFEED
Figure 8: Problem configuration for the problem from the IMC 2012 competition
The second important component of the problem is the encoding of the verification function Vo as Python function that receives a proposed solution and checks whether satisfies the constraints of the problem. In Fig. 9, show an example of this function from the same problem. The function returns tuple of: a boolean value indicating whether the solution is correct, feedback string explaining why the solution is incorrect, and tag indicating the type of the error.
Finally, the problem contains a generation function that generates a set of variations of the problem by plugging in different values for the parameters 0. We show an implementation of this function for the same problem below in Fig. 10. For this problem, the generation function simply returns an integer sampled uniformly at random from a given interval.
Once the problem is fully encoded, we also include a variety of unit tests. These unit tests typically ensure that our official solution to the problem is correct (namely, that satisfies the verification function). Ideally, the unit tests also test that wrong solutions are rejected by the verification function, but it is generally hard to cover all possible wrong solutions.
Problem review The final step of the workflow is reviewing the problems, described in Sec. 3.3. The key part of this workflow is our application for data analysis, which is shown in Fig. 11.
The application shows for each problem and for each variation the following information: problem statement, formatting instructions, our ground truth solution, and interaction with the model. The interaction with the model shows responses from the model, feedback from our parser (checking whether solution can be extracted from the model response, see App. B), and the final result of the verification function (correct or incorrect). We developed the application using FastHTML (fas, 2025).

---

MATHCONSTRUCT
def check (self. [ist:]ist[[foat]]]
if len (x) self.n:
return False, E"The number of rows is not n ((self.al).",
PaeckerTag.INCORRE
LENGTH
if any (Len (zow) != self.n for row in x)
return False, f"ehe number of columns is not n ((sel2.n))."
CheckerTag, CheckerTag.NNoRRE.... INCOONRTTCCCCRTTEEEETTTT
if any (x[1] !- for i in range (sclf.n)):
return False, E"Some diagonal elements are not zero.", CheckerTag. ItC.RRECT_SOOLOTTTTT range (
for
for j in range (self.n) if x111131 <= 0:
return Faise,
f"Some off-diagona elements are not positive.", CheckerTag. INCORRECT_SOLUUTIN
rank -
(x)
if rank > 3:
return False, E"The rank is (rank), which is greater than 3.", CheckerTag, CheckerTsg.NNoBREE__.. SOOOUREETTTSLOUUION return True, "OK", CrackerTag.coRRE.
21
Figure 9: Implementation of the verification function for the problem from the IMC 2012 competition
def generate () -> "Problem IMC 2012_20122"1
n randon. randint (6, 20) return Problem IMC 2012 (n:
Figure 10: Implementation of the variation generator for the problem from the IMC 2012 competition
The application generally allows us to quickly review the problems and to identify problems that are not suitable for our benchmark. For example, by investigating responses from the model, we identified issues with our problem statement or formatting instructions. Additionally, an important part of the review was identifying issues with our parsing of the LLM solutions in cases where was correct, but provided format that our parser was not able to understand.
B. Parser Details
The parser is designed to parse as many outputs as possible while still enabling specific feedback to the model in case of errors. We give a high-level overview of the implementation here, and refer to the code repository for the full implementation.
The model solution always appears a boxed environment, which is the only part of the model output that is parsed. no boxed environment is found the model solution, the parser throws the following error:
No \boxed content found in solution. Final solution needs to be encased in \boxed
The input then sanitized by removing any extraneous characters, common sequences for formatting brackets (like Vleft and bright), and other common formatting characters.
The parser differentiates between five primitive types (Integers, Floats, Fractions, Strings, and LaTeX Expressions). and two composite types (Lists and Matrices), The correct primitive type is automatically extracted from the model solution. By verifying any primitive type that gets extracted from the model solution matches this primitive type, we can ensure that the model has correctly formatted its solution. For instance, one of the most common errors is the use of in a model solution. If a parser encounters this string anywhere in the solution for a primitive type that is different than Strings, it will return the following error:
Expected a primitive int int//loattppareeal LaTex expression, but got 'dots'
Note that the same error will oceur even if the dots appears anywhere matrix list.
12

---

MATHCONSTRUCT
Model: gemmii------ffiaas---iiinnngggg
[Reload Dete]
Problem: 0tt-s-shottliii221443333000000
Home
gemini-2 O- flaah--thiniing--ennee
Problem Instance (Original):
mo shotthhtt-taat 2001-06 XXO
me-ahhntiat-2001-e XXXX
L 2 be integer, Consider an n shessboard divided squares. call guration rooks
this board (esth)/aces)) every row and every column contains axactty one rook. For is - 22 and it 5, find happy configuration rocks such that there no & squara without rook of its IP unit squarres.
mo-shortisst- 2000220 XOOX)
swwrsshtttttttt 2003 XOOXS
mo--shential-3003--0 XXXX
Formatting instructions:
mo--thoniit-2005---0000 XXXX
mo shortist 2006 c5 XISXX
Curput comma-orparatet list of 1-brood rock indices Jeo T1, 1) the too left conner of the boand) innion of (hoond, for example (11 (1FU))
mo-shortiat- 2008-02 XXSS
mo-sthontst-200822222 X00X
Our Solutione
shortizz
inc-ahenfia-2011--l WXXX
L1
21
(2),
13), 10), 177,
50, [22, 10), (20, 20), [18, 161)
mo--shortit-2011--222 XXXXX
shontist 2014 c5 XXXXX
Medel Interaction:
mm--ahanfiat-201---22 XXXX
Role: assistant
mn--shonts--201--5500000 XOOX
shortist 2016 XXXX
We are find a happy con't puration of rooks on rost, happy configunation in eurs ow have 22 mosko, and each row and each column containa esucily une molk. We mead to the poottoons of theoe 22 moles such that
chessboard such there is aquare
Ina-sdhatiaa--017---5 XXXX
x suhgrid come leeat anw mokk He reprosent the pestiion number.
Ino-shontistt2017--1 XXXX
the rooks (i) for d...., .22 where is row number i
it happy
configuratio, the row indices are i.. 22) the column indices are also -..,,... 22) In some order. We can represent the configuratio on permutation e of (1, ....... 22), where the rosla are placed it positions (5, for subard
mo shortist 2018 XXXX
2.2......
find permutalion
mm--shanliaa-2000--3
mubgrid defined by the top- comee (r,cc, where
22 5 18 is e 22
The
mo-shortiiet st 2020-nt XXOX
xr 5 suboris detined by (r, c) conslats of souares (1.3) where 4 i + Land e happy configuration such such SS in r- e c,
+-4 We want find 21.2.......
18] (1,2.....
(1, (.......
aae-shhtttttttt XXXX
sema permutation, for every e 21.2...,, and
E (1, (1,2,.... 18). there wdnds some 2.. 22) such that S dandl S of5) Si Consider the
mmo-ehentlla-2097-6 XXX
That olt) 1fr 2 22 Rooks (6 Cons der the subgrid starting at (1. subgrid consitts mhre mile enieari Bevbs
mo-shortist- 20 XXXX
2,2,3, 1.5 and columne 6, 7, Novo thasooss
4t 6)
Figure 11: Screenshot of our web application for data analysis
For composite types, the parser recursively parses the contents of the boxed environment. Lists are parsed by splitting the contents of the boxed environment by commas, newlines or & characters. We recursively extract the first element of the list. To prevent splitting the wrong character, we check if the extracted first element is valid primitive, list, or matrix. If not, the first element expands to the next coMma, newline, or & character and we repeat the process.
Matrices are parsed by checking for any иАTх environment that contains an array or matrix. Results are then extracted by splitting the matrix by "W and parsing each row as a List.
Finally, we found that lot of the models add unnecessary brackets in their solutions (e.g., writing '((12.3))) represent "1,2,3") To prevent this from causing errors in the verifier, we automatically extract the expected list depth from the verifier's s solution and match this depth with the model's 's solution. If the model's solution has an unexpected depth that can not be easily converted, the parser will return the following error:
Failed to match correct depth
{depth} for (parsed_ansseer
This entire procedure was then tested using a variety of model outputs in unit tests to ensure that the parser can handle a wide range model outputs. Furthermore, in lot our model runs, we manually verified the parser's output to ensure that it was working correctly. This gives us high confidence that model performance does not depend on the parser's behavior.
C. Additional Benchmark Details
In Table 4, we provide a summary of the MATHCONSTRUCT benchmark, including the number of problems from each source. In Fig. 12, we show a histogram of the length of the problem solutions in the benchmark. We note that there is one problem with a string length over the required limit of 4000 characters, but this solution can be more succinetly expressed in 18TEX, which is supported by our parser.
13

---

MATHCONSTRUCT
Table 4: Summary of MATHICNNSTRUCT problems by source.
Source #Problems
Source Description
bmo-shortlist
Balkan Mathematical Olympiad (+Shortlists)
bulgarian bxmo
Bulgarian Competitions (National, MO, IFYM)
Benelux Mathematical Olympiad
croatian
Croatian Competitions (MO)
dutch
7
Dutch Competitions (MO)
eme
European Mathematical Cup
ime
International Mathematics Competition for University Students
imo-shortlist
International Mathematical Olympiad (+Shortlists)
ssottihortiist
10
Junior Balkan Mathematical Olympiad (+Shortlists)
konhauser
Konhauser Problemfest
misc putnam serbian
Misc (Baltic MO, Flanders MO, IMO Prep Handouts)
William Lowell Putnam Mathematical Competition
Serbian Competitions (MO, IMO Team Selection Test, Regionals)
swiss
11
Swiss Competitions (MO, IMO Team Selection Test)
tot
Tournament of Towns
usamo usamts
USA Mathematical Olympiad
USA Mathematical Talent Search
MATHCONSTRUCT
126
D. Experimental Details
In this section, we describe in further detail how we performed all our experiments and evaluation.
D.1. Experimental Setup
Model Names For readability, adopt shortened names for some models throughout this section. Specifically, refer to GEMINI-2.0-FLASSIE F-AS-----E as FLASII and 11w----.-FLLAS-TTIIEe -XX FLASI-TIINKING Similarly, CLAUDE-3.5-SONNETT and CLAUDE-3, 3.5 -AAKU are denoted as 3.5- SONNNET and 3.5 -AI-H,, respectively.
Inference Inference of the models done through API calls to the appropriate model. For the LLAMA and QWEN models used the Together API. For all other models, we used the API of the corresponding model provider. The total cost of these experiments are reported in Table 2. Each model was queried with temperature of and nucleus sampling with parameter top_p 0.9. We use maximum output length of 16000 tokens, except for the ol model family and for TLASH-TTHNKINGG where we increased this to respectively 32000 and unlimited number tokens.
Code execution To safely execute untrusted LLM code, we conducted all experiments within a lightweight Docker container. Any generated code was executed on single core of an Intel(R) Core(TM) 19-9900K CPU @ 3. 3.60GHz with 1GB of RAM. The coding agents operated in an isolated environment without network access, restricted to using only the standard Python libraries along with numpy, scipy, and sympy libraries.
Problem setup For our experiments, we selected 126 problems, each paired with an original variation, which was kept identical to the original when possible. In cases where this was not feasible, we chose a variation that was sufficiently challenging and met the criteria outlined in Sec. 3.1 and Sec. 3.3. This resulted in a total of 475 variations, all of which were used to conduct our evaluation.
Run setup For each experiment, we used the prompts outlined in App. F and provided the respective formatting instructions, with examples shown in App. D.2. We distinguish between the -fain-of-Thought (CoT) solver and multiple coding agents in our execution process.
In the CoT experiments, after receiving the model's response, we parse the expression inside the boxed environment,
14

---

MATHCONSTRUCT
20
# of Problems
15
10
10a
10s
String length model solution
Figure 12: Histogram the length the problem solutions the benchmark.
present. If our parser detects formatting issue response found, the model is reprompted up times provide valid construction with detailed feedback. Specifically, the parser provides the model with the error in the following format:
The solution parser encountered the following error: (error)
Please format your reply accurately.
(Repetition of the formatting instructions)
For the coding models, we execute any code block appearing in the model output with a time limit of minute for the general coding model and 2 minutes for the brute-force agents. If the code runs successfully, we report the output the model. If not, provide the model with error trace. Both appear to the model in the following format:
Code Output: ('uutuut ...
We do not allow the brute-force agent to correct mistakes or adapt their strategy after the output is returned. This is to prevent the model from coming up with clever, non brute-force solutions. For the coding and brute-force inference agents, we allow them to correct mistakes and adapt their strategy after the output returned. They are then reprompted continue reasoning. We provide parser feedback up to two times per solution, allowing no more than four code attempts. Finally, we ask for final response containing the boxed solution, and parse it described earlier.
D.2. Formatting Instructions
We differentiate between main types of formats that we require from a model for verification of the solutions. This includes:
A single primitive object, i.e., an integer.
A list/set of primitives, i.e., tuple sequence.
A matrix containing primitives, i.e., board table.
A symbolic template for any LTTX expression, most generally fractions.
For each of these, we present generic formatting template that we tweak for problems that do not fit the template.
Primitive template:
Output the answer as an <integer/string> inside of $ {boxxed (...) $
For example, $\boxed[123)
15

---

MATHCONSTRUCT
List template:
Output the answer as a comma separated list inside of S\boxed(.... 18. For example, S\boxed[1, 2, 3)$.
Matrix template:
Output the answer between \verb I /brgi//array
and \verb (arday))) inside of $\boxed(....1 For example, $ d'boxed( (begin (cco)1 & & 3 \ 5 \ 7 9
(anday)
Symbolic template (for fractions):
Output the answer as fraction inside of $.boxed(...)> For example (bboxe(\ffaa((/) (2))
16

---

MATHCONSTRUCT
them to E. Additional Experiments
E.1. Analysis Output Tokens
106.
100%
01-MINI
# of Output Tokens
80%
0l
109
FLASH-THINKING THINKING
Accuracy
60%
10
40%
109
20%
0%
10a
-I-MINI
o1 FLASH-THINKING
10000
20000
30000
40000
50000
Model Name
Output Tokens
Figure 13: Distribution of the number of output tokens.
Figure 14: Correctness per number output tokens.
Reasoning models typically produce large amount of output tokens arrive at the final solution. In this analysis, take the three best performing models from our experiments (01, output tokens that they produce when evaluating on our benchmark, as well as their accuracy for each amount of tokens.
and 0l MM-NN),, and compare the number of
First, Fig. 13, we show the distribution of the number of output tokens for all models. We can observe that FLASH- THINKING produces the largest amount of output tokens, even going over 100k tokens for some problems. Overall, o1 generally produces less tokens and has higher accuracy.
When looking at the correctness for each number of output tokens, as shown in Fig. 14, we can observe that for FLASH- THINKING and 0l MIIMI the accuracy steadily decreases with larger number of output tokens. However, FLASH-THIE THINKING still produces some percentage of correct solutions even for 50k tokens. Interestingly, we can observe that 01 has 40% accuracy with around 40k output tokens. Recall that models receive feedback from the parser when their solution is not formatted correctly, and they have a chance to fix it. This bump in accuracy comes from the samples where 01 was able to correct its solution after the initial round of feedback.
E.2. Verification Feedback
Writing correct verifiers is a challenging task, but might be easier for LLMs than writing correct solutions. In this case, the LLM could potentially leverage its verifier to check the correctness of its solution, making it possible to use the verifier as a feedback mechanism. While initial experimentation indicated that LLMs were not able write correct verifiers, we can still obtain an upper bound the performance of such agentic framework by using the ground-truth verifiers. Since these verifiers were written to return very detailed feedback about the specific mistakes made by the model, provide feedback to the model in addition to the parser feedback already provided.
We ran this experiment on 03-MINI, the best performing model in our evaluation. Using ground-truth verifiers, the model achieved 65.07% instead of 53. 77% by using parser feedback alone. While significant improvement, the assumption of access to ground-truth verifiers is unrealistic, especially given the difficulty writing correct verifiers.
E.3. Case Study Comparing THINKING and 01
In this case study, we qualitatively compare the outputs of FLASH-THINKING and 01 on problems from the IMO Shortlist.
17

---

MATHCONSTRUCT
IMO Shortlist 2001 CS In main results observe that FLASH-THINKING fails to solve any variation, while 0l solves this problem correctly for 3/4 variations. First, looking the FLASH- THINKING reasoning trace that it tries to exhaustively search for solutions, and makes mistakes in the casework. On the other hand, 01 immediately recognizes that the problem asks something very similar to self reff-descii numbers (those where digit i is the number of times that appears in the number). It can recall all such numbers, and solve the problem for smaller n. Interestingly, for larger n = 17 exactly the same construction works, but ol fails to find it, possibly because typical examples on the internet contain only digits.
observe
Prompt
Find 10 finite aequeaces (#o, 21..., Ra) such that Ioz evecy d, 0 S S n, equala the numbez of sequence.
times appears Format your reply as follows:
Output the aequences as separatee tuples Inside
Yeg
(1, 2), (1, 3), (1, 1,1,0
FLASH-THINKIE
01
Let (x0,4) (
finite sequence is the the sequence,
convenient way produce such *self- dascribing" sequences is via the well- known del--describing aumbers 1210, 2020, 21200, 3211000, and each digit as an entry Zor dir ...r in in the saquence,
that for every J, 0 SJ S mumber of times J appeara The length of the sequence is n The indices are 0,1....,
Interpreting
Let's consider amall values of
finda that x; precisely how many times j appears. Here
solutions
(1,0), (2,0,0),
10 explicit examples:
03,0,0,0), (4,0,0,0,00 0) Let's verity these 10 solutions.
(I, 2, 1, 81 (2, 0, 2, 8)
12,
or [3, 2, 1, 1, 0, 0, 0)
(4,
2,
(1,0). 1,2 40's 1, 41's
1. 0, 0, 0] (5,
-1 0,
C, 1,
0, 0, 0)
3. Correct.
(6, 2, 1, 0, 8, 0,
0,
C,
01
(7,
2,
(2,0.0).
#0
8, 6
0,
41's = C, #2's Correct.
0, 0, 0, 0 L, 0, 0, 01 (8,
2,
1,
0,
0, 0, 0, 6,
0, 0, VnAnTn
form
Chey can written ass\n
Check (2,0,2,0) is velid. n 3 (10,21, 22, = Number 's in 22,0,2.0)
(1, 2, 1,0), (2. (2.0,2
1,0, 0,
Correct.ar = Number is Correct. Number of 2's in 22,0,2.0) is 2. correct. 2a Number of 3 (2,0,2,0) Correct.
in (2.0,
(4. 2, 1. 9. 1,0,
0),
(6. 2. 1. 0. 1,0
0)
(7
So 22,0,2,0) 0) is solution.
(8. 2. 1. O 1,0,0,00))
Final answer wt 11 be these 10 tuples.
(9.
Uetput: (1, 0), 12, (4,00, O)...
(9,0,
Parsed Answer Correct
[[1,
2,
1,
0),
[2,
0,
2,
01
12,
1, 2, 0,
Parsed Answer Incorrect
D),
2.
1,
0)
2,
1
0
0
01
15,
2,
1
0,
0,
1
0
0,
0],
[6,
0,
0,
0
1,
0,
0
01
[7,
[11, 01, 12, 0, 01, [3, 0, D, 01,
14.
0, 3,
1,
0,
0,
0
9
0],
18,
2
0,
0, 01, [5, 0, O, 0, 0, 01. 16,
0, 0, 0,
0,
0,
0,
0
1,
3,
0].
19,
2,
1,
3,
0, 01. 12, 6, 011
0,
0,
0,
0,
011
Parsecheck Details
INCORRECT SOLUTION: Sequence [1, 0] hag occurrences of 1, should be
18

---

MATHCONSTRUCT
Interestingly, in of the other attempts, FLASH-THINKING decides to search for exactly these sequences online, but comes up with the wrong results and eventually fails solve the problem:
"Searching for "self-referential sequence" or "autelogical sequence".
"Counting sequence".
Consider the sequence starting with "How many Os, 1s, 28, 3s, are there in this sentence?"
Wikipedia:
Self-reeerential numeric sequence.
Solutions listed
n-1: None
n=2: None
n-3: (L,2,1,0), 0,,00 n=4: (2,1,2,0,,), (3,2,1,1,0), 14,0,0,0,00
n=5: (2,1,2,0,0,0), 0,,,0,
19

---

MATHCONSTRUCT
IMO Shortlist 2014 N2 Another interesting is the IMO Shortlist 2014 N2. Here FLASH-THINKING fails solve that both models typically make
any variation, while 01 solves all variations. By inspecting the solutions deeper, the same substitution d y/ and come to the point where they have to find d such that d² 4 d 3d - 1) is perfect square. Then, both models start plugging in small values of d, but given initial sequence of small solutions 6, 12, 20, 30,.., 01 recognizes that the solutions are the pronic numbers nnn + 1), and finds the solution for all variations. On the other hand,
fails to find the pattern, and is not able to find the general solution.
Prompt
Find distinct pairs (x. u) of pesitive integers such that and
875² 13xy Ty²
Format your reply as follows:
output comm-ssparrated list of pairs (x, inside example (2. (5.6)
THIS--TIINKIGG
01
Let the given equation be
A convenient way to see that there are infinitely many solutions the first 32 of them equation d= y x 0, sa
V722 13zy + Ty² ix vl +1. have |a = equation becomes
Since
the
to set
8/7z² 132y + Ty --=====++ ++ Let y-2 integers, k= integer. Then y + Substituting into the equation, get 1/7-" 13z(# + R) 7(x + =
(7x² - 13ry + = yl becones (7a" 13x(# + d) 7(x + d) d
x x< are pesitive must be pasitive
1. Rewrite the left-hand side in terms of and d. since y ==
7 13r(s+ +(=
7x 13s 13nd + 7(x" 2nd +d)
(7x" - -0--77") 7=²)+ 1-1ddd d 14zd) 7d
Rearsanging the equation equation in we have
quadratic
" + +zd +
2² (7k2 + 0.
equation then
a² + zd 7d (d dd 3d +33 3d+1.
x² (7K2_ (13 + +3k² 3k)
x² kr + (Tk 4a -3 3k - 3k -] 1] =
Rearrange to get
2² + 4d -
2² + kr (-A* 462 38 1) = 0.ke use the
3. View that
quadrstic in For to
quadratic -k-v=-
to
#!
2 + + (dd d 3d en integer, its diseriminant d 4(4d - d 3dd- 3d- muat perfect square. One fiads that A 1s perfect square precisely
4- 1662 12814 For be
2
positive integar, wa need the discriminant
4R3 1552 4
perfect
takes the values d 6, 12, 20, 30, 42,56, 56, 72.90.... which turn
square, and -k DD to positive even integer.
to be d= 4. Solving for in terns of n. Set d(n) = (n 1)(z + 2). Cne finds that the corresponding
1)(x +
have solutions for k 20.0..30 90, 1000. Tet's 11st paira v). 6: (7, 13)k 20: (71,91)k 30: (139, 169jk 90: (791,881)
positive solutior for 13 æ(n) = n² + 444" " +33 -I, and hence v(x)= = =0)) + = = +6n +...
k 1000: (31063, 32063)Look at sequence: Ratios: 20/6 3.33, 30, 90, 1000.
30/20 1.5, 90/30 3, 1000/90 11.1.
Balow are the first 32 such pairs (i.e., through n 32) In each patr, requiced. n=1: (,, 13) n=2: 129, 411 - ==3: (71, 92) n=d: (139, 169)
pairs by increasing à by a factor of 3 or 10. take
generata
peirs based k-6, 20, 30, 90, 300, 900, 1000, 3000, 9003, ... Output
Pucting them all together:
(7. (213),22,,8 (71, (139, 169)....
pairs
(7. 13), (71, 91), (139, 169), (791, 881)...
Parsed Answer Correct
[[7, 13), [29, 41 [71, 91 [139, 169), [239, 281], [377, 433], (559, 631]. [791, 6811, [1079, 11691, (1429, 15621, ...]
Parsed Answer Incorrect
[17, 131, (71, 911, (139, 1691, [791, 881], [5014, 5314], (a4755, 856351, ...l
Parsecheck Details
INCORRECT CONORRECTSSOOUTION: SOLUTION: Tube root of 27274396 integer
20

---

MATHCONSTRUCT
F. Prompts
In this section, we outline the various prompting methods used for the different evaluations we conducted, along with example solutions for each evaluation
F.. Chain-of-Thought Solver
For our main results, presented in Table 2, we use a direct approach where each model is asked to solve the problem. We further give instructions for the precise way which the answer should be formatted.
Prompt
Show that for a 8, there exists a natural number that has the number (the sequence of digita beginning,
a from beginning to its end (zny number of zeros that appear in the beginning of the number obtained example.
constitute
decreases
this way are to removad).
Pormat your zeply as follows:
Output the answer as an integer inside of For exomple
123
01
concise way to find such an integer N Istarting with the digit *g*) is to note that "noving the first digit
the end" be described by the decima-rotaation formula:
Let N have digits and begin with Hrite N = x 104-1 R, where R < 10fd-1). Moving the first digit (8) to the end yields the new integez (in base-10) An (otateLeft((N) 10ft
problem's condition says
intager must y 10
80R+8= 10'd R)/8. Clearing deneminstors gives 80R
79R 8 -0
R (8 10d 64)/779
Hence, one neads 8 10 64 to be divisible by 79, 1.c. 10 = 8(mod79). small search
13. Plugg! mg inco the formu shows the small lest solution sccure d- 12, N 10 8101265822784. produces R= 10t2 64)/79 101260822784 checked directly that moving the lesding *g" to the end of 8201265822784 gives 1012658227848, which exactlyy N/8. explicit exapple therefare 8101265822784, 1.e. 8101 265822784
Parsed Answer Correct
61C1269622781
21

---

MATHCONSTRUCT
F.2. Coding Agent
The coding agents are allowed run any code they deem necessary. We give instructions how this be done, below:
Prompt
Let 2. 2 be an integer. Consider an X chessboard divided into n² unit squares. shappy is every zow every
call con.Eiguration of rooks on exactly one roak.
Fer n = 22 and = 5, find happy configuration of rooks such that there no k x square any
without
4a unit squares.
Format your reply as tollows:
1ist of based zook indices tso (1, 1) the top left cozner of the beard) inside " for example
Output comma
FLASH
Okay, I understand the problem. We need to Lind happy conf of 22 zooka on 22x22 square empty zooks. happy configuration means there's exactll one rook in each rew and each column, This is equiva to permutation of the numbers from simple permutation like (1, 1), (2, 2), .... 122, 22) would not satisfy this condition. if place the rooks on the main dizgonal, then any 5x5 subgrid along the diagenal has no rooks in upper-right
chessboard
22, The condition that no 5x5 squaze is empty is the crucial constraint.
bottom-left 4x4 corner,
squaze is emply, se need to spread the zooks out scmewhat evenly. à good starting point might offset
rook by cestain amount. Ior constant Les's tzy with 2=1. The rocks are at (i, i). This deesn't work. Letts try a=2. (i, 2+1 sed 22
place the Consider placing zooks
on main diagonel mod
(i,
let's try a=3. (i, 3+1 nod 22 11.
Let's try
the indices are 1- 1-based. This is guazanteed to have one zook pez row. le need to check if there is map permutation
contiquration
i-th
position (i, 3ipmo222
one rook per column.
map Hooipmod22,, Dence this is valid rook configuzation.
and ceprime. 3 and than visually check whother might work.
Now we need to see if there's a 5x5 subgrid with no rooks. will generate the configuration
for 22 "ppyhhon
-
rooks
for i range
sel (a i) 18 rooks.append coll)
print trooks)
def chack Barck__x5__e__ Exp__mptyy_eemmmepeeppp (rooks, nl:
for in range (1, n 1):
for a in range(1, n empty foz row in zange ix, E 5): range (c, =
11:
if (rоw, col) in rooks: eпpty break
if not empty:
if empty: print (E"5x5 empty square ((x), (el)
return Folsa
return True
print (check 5x5 (check__xx____________ ompty (rooka, m))**
User
Code Output:
("" 4), 12, (3, 10), (4, (5, 16), 19), 221 3), (10, 91, (11,
12), (12, 15), (13, 18), (14, 21), (15, 23, (16, 5), (17, 8), (18, 11), (19, 14) (20, 171, (21, 201, (22, 1)]
5x5 empty square round a, 17)
Palse
22

---

MATHCONSTRUCT
FLASH
okay, the coda output shows that the configurstion with a 3 doesn't work, It found a 5x3. empty squara, Tet
"python
rooks []
for i rangell,
ccl = (a + 1) A8 appks.append coll!
print [rooks)
def Sheck__x5_enne (zocks, n):
for range (1, for a in range(1, n 11: empty for Iew in range iz, = 5):
zange (c, 5):
if col) rooks: empty raise break
if not empty:
if empty: print (f"5x5 empty square ((r), (cl)
return Palse
return Trus
print (caeck_5x5 expty (zooka, a))"
User
Code Outpul: (L, 8), 12, 15), (3, 22), (4, 71, (5, 14), 16, 21), 17, 6), 18, 13), 19, 20), (10, 5), (11,
12), (12, 19), (13, 41, (14, 111, (15, 18), (16, 31, (17, 10), (18, 17), (19, (20, 121 16), (22, 1)]
empty square found 11
Falde
FLASH
okay, also doean't work. lat's ""python
9
zooks - []
for i range
cel (a 1) 18 apoes. c611)
print !rooks
def check 5x5_ Exp_emptyyy_eeeeeeeeepppppp_ppp_ (zooks, n):
for range for a in ronge(1, n 11: empty for rew in zange iz, = 5): zange (c, =
1):
if (rom, col) in rooks: empty Palse break
if not empty:
if expty:
print (f"5x5 empty square ((r), (cl)
return Fa
return Trus
print scneck_sxt_emme (rooka, n))*"
23

---

MATHCONSTRUCT
User
connect ones Code output:
"1 101, 19), 12), (12, 21), (13, 81, (14, 17h, (15, 4), (16, 13), (17, 221, (18, 9), (19, 181, (20, 5), 121,
11,, 201 7), (10,
14), (22, 1)
True
FLASH
Okay, the code output shows
configuration
The rook positions are: (1, 10), (2, 19), (3, E), 14, 15), (5, 2), 16, 11), (3, 20), (8, 71, (9,
16), (10, 31, (11, 12), 112, 21), 113, 8), (14, 17), (15, 41, (16, 131, (17, 221, (18, 9), (19, 18), (20, 51, (21, 14), (22, 1).
Final Answer: The happy contiguration of rooks is Aboxed (C,, (C, 101, (2, 19), 13, 61, (4, 15), (5, 2), 111, (7,
(8, (9, 16), (10, 111, 4), (16, 13,, (17, 22), 128, 91, (19, 18), (20, 51, (21, 141, (22, 1)11.
112, 21), 113, 8), 014, 17), (15
Parsed Answer Correct
[11, 101, [2, 191, [3, 6], 14, 15), [5, 21, [6, 111, [7, 201, [3, 71, 19, 161, (10, 31, [21,
121, [12, 211, [13, 81, [14, 17), [15, 41, [16, 131, [17, 22), [18, 91, 119, 181, 120, 51, [21,
14), 122, 11]
F.3. Bruteforce Solver
For the brute-force approach, the models are asked to generate single block of code that naively creates a solution satisfies the problem's is constraints. Only one attempt to produce the code is permitted.
System
You exper: nathematician that selves problems using brute force approach. You have been given access to a Python interpreter that you can use to generate your brute-force approact.
Make sure to abide by the following rules: should the ..... saquence fol lowed by the end of your "esponse.
"pythonn ending 2. The code should be brute force solution without optimisations. The usez needs to know whether the problem
Python
starting
be solved in brute-foa force sppresch.
3. After you have written your code, you can immediately stop your output. The user will you results.
execute your
result successful, you can then
format the response accurately.
your Pyshon code, you con 'print ()* save whatever important information you will then need to format environment.
final. reply, The user will then execute your code in Python
for minutes. If the code times cut, you will receive timeout ecroz alosg with all print statements received before Liming out. Before generating code, perform reasoning ensure your solution will attempt valid brute-farce approach.
5. Your code will
your program finishes withost valid solution efore the two-minute timeout, you have not done your Jeb well.
User
27, sequence distinst real numbers P1. such (R), #2, (x2, Pab..., (#a-2, #n-1, wa), [#a-1, 2n, 2ih, and 21, forms 3-term arithmeric progression when arranged in increasing ordez.
3.5-SONNET
het me reasen about this prohlem:
27 distinet
where consecutive triplet arichmetic
sequence when sorted
triplets wrap around, meaning
3) A brute-force approzch would he to: Start with some amall initial values
24

---

MATHCONSTRUCT
Incrementally try values that satisty each consecut Ive. triplet
Keep Lrack ef used values ensure distinctness
Check if it wrapa around correctly
solution, let's:
Start with small initiel values Ixlu2081, x!u2062)
-Fer each next value, ensure can an previous two
Use reasonable bounda to imit search apace
Check for distinetnese
Let write code search for such
"pyyhonn
deč s__arithmetic__ae wtt___hheeeeeeeeeeeeea b, c):
numa corted c])
return abs (nums [1] [o]) (nums nums [1])] < 1e-10
def check_sequence (seq):
n (seg)
for 1 range
15 not sogaatttmmetcc__oeee_orrrdddd recurn
seg (i+1) Wa], seg/ Man11
Check inctness
return len (set (seeg))))
leniseg)
daf
(n=27):
def extend sequeece (ourrent_seq)s
if len (onurrentt_eeg == m:
check sequence (current_seg!
print (", join (mapistz, curcent_seq)) return True
False
prevl, prev2 current_eeq[
Try values that could petentially form arithmetic sequence used (current_seg)
different passibilitias for value for multiplier in r-10, 11); candidates
Iry extending based
patterns
prev2 previ multiplier, Continue in one direction 2 previ prev2 multiplies, Continue in other direction (previ /22v2) multiplier + Kiddle value
[or next_val in candidates:
next_val
if bttschhntti__hhe_cortteeee next_vei prev2, next_val) setuen__eeueence (current_seg [next_val]):
return False
Try different starting values range (-5, 6):
for sacond in r-S, 61:
is start !- secend:
extend_sequanee ([start,, (staat,, second] return find_sequence
User
Code Output:
",--,,-4,6, -,,,,4,,-66,2111,,-2-4-11-111 22,, -11,-7,-30 -3 This code.
-15,
time your executed, on, you
3.5-SONNET
Based on the autput, I can now provide the solution.
5, 4, 66, 6, 88, 10, - 12, - 14, 16, 18, 20, 22, 24, 26, 28,
-30
32,
34.
33,
35,
31,
27.
23
19,
15
-11,-7-3
This sequence satiofies all the raquired conditions:
1. containa distinct numbera
25

---

MATHCONSTRUCT
2, Bach consecut.ive triplet torms an aritametic sequence when arranged increasing order
3, The wrap eround condition also satisfied Ithe Last two numbers with the first, and the last number with the first two)
Parsed Answer Correct
(-5, -4 6, -8, -10, -12, -14, -16, -18, -20, -2, 244, -26, -28 -30, -32, -34, -33, -35, -31,
27, 23, 19, -1, -12, -7, -31
F.4. Brute+Infer Solver
Unlike the pure brute-force solver, the brute-force inference agent allowed explore solutions with smaller parameters generalize the pattern. allowed up to two feedback rounds explore settings and test different strategies. The interaction below demonstrates how model, in this case GPT-4o, can adapt its naive brute-force approach into more effective algorithm by combining logical reasoning with programmatic solution.
System
expert nathematician inferance. You approach mathemarical problams by first solving them in brute-force menner for smaller cases necessary and then generalizing your rindings to solve the problem itself, In in series of In each step, you
problems using brute-force approach logical
order to solve the problem, you need execute a Python code block to test your current idea.
Make sure to abide by the folloking rules:
1. You should write the code in Python onda block starting with ''""ython" and ending with the 1... sequence followed by the end of your respoase.
2. to solve the problem itself if possible) and then generslize your findings to solve the problem itself. rry to properties that
brute- force
for smaller
(or for the
find patzerns, rellationhiip,,
you solve the problem. output. The user will execute your was aucceasful, you con then
3. After you have written your code, can stop code and giva you results. response accurately.
the
4. In your Python code, you can use 'pzint ()* to save whatever important information you will then need to format your final reply. The will then environmen..
code in Pythen
User
posilive integez said
it v00 2yndni
positive integer with exact ly 60 close divisors.
Permat your zeply follows: Output answer as integer inside ... example
YYour answer
mathematical operations using valid LaTeX notation.
GPT-40
To solve this problen, we need to find posicive integer n such that the number of its sstistying yn < 2/n exactly Wiet's down problem:
cenaider 2. +ACeunting Jivisorsa:: will have ensure that there exactly 60 diviscrs in this sange
viRange Divisorsus
range vn < 2/n.
**Choos'me ng
select
this condition satistied. terdiitemize)
find an n, can explore integers small condition. Lot's sttempt to brute-farce this for a smaller test case first, by examining posatble candidates for n.
they satisfy
Import Function calculate number close d'visora
def count_close divisors (n)
aqrt_n math. (n)
close_divisors [d for range 11, a 1) W8 and aqrt_n sert_n]
26

---

MATHCONSTRUCT
return Len (elose__divee
divisors) Brute-toree search for the Integer
60
for n in zange(1, 10++6): count_close_diiieert print(n) break)i
azzet__looe_diiveee
This cede attempts to find the smallest with exectly 60 close divisors by iserating pessible n values, counting their close divisors, and stopping when the target number of close divisors reached. You can run the code to see the result.
User
Code put : \V- Brror exceeded 120,0 seconda timeout."" "*"\\
GPT-40
To address the timeout issue, we should focus on optimizing our approsch instead of brute- forcing through all integars. let 's the propertias of civisors down search,
#+ Understanding the Divisors
Por number the total aumber of divisors determined its prime factorization. If Pi P2 .. ther the number of divisers d(n) is given by: d(n) [a_1 to_2
(a_k
**# sange for close Divisors
Ne want to find numbers whose divisors satisfy v < d 2yn. If n has d(n) total divisurs, the divisors around middle diviser list. IE exactly divisors, it is reasonable to conaider numbers with larger total divisers count and check their properties.
### Revised Approach
We will:
Consider numbers high total
2, Use combinations of amall primes to achieve high number of total diviaors.
3. Calculate close divisors for these numbers efficiently.
tet's try an approach using more atructured exploration of numbera with signi oannt. numbera divisors: "python
import math
from sympy import primefactors
Function caleulate all divisora def (n)
diva []
for i in zangeti, (math. 1):
(ivs.appendd
i n // diva.appand
return sorted
optimized search for 200____lo__ddviiiorre... (1
def inine_inteegrr___e with_wtthhhhh
primes [2, 3, 5, 7, 11, 13]
max max_divisors
best_n
Iterate over sone product of primes raised to gowers range
for x2 in s1, 5):
a3 range 5)
for a4 in sange:l, 5):
for a5 in range 51:
range
a [primes[0] vAlxa))
(prines [1] (x22) (1]2)
(primes [2] xxa3)
(primes [3]
(primes *.a5) (primes(S] **aE)
divs = divisera (n)
aqrt_n math.aqrt (n)
27

---

MATHCONSTRUCT
poose_divs for dive sqetun sqrt_n]
if leniclose_dive) 60: return
result wtt.eper.wiiiitlooooooeeeeeee divissrei) print (result)
tais approach, we use combinal combinations of the first Iew small primes raised to snall powers efficiently search for Each configuration in exactly 60 close divisors. You can run this code to find n.
is evaluated if it results
User
Code :utput: 8985139471250
GPT-40
code successfully found positive inceger exactly divisors. Therefere, the positive integer we are looking for is 6985199471250
28


Reviews:
[{"review_id": "VcWYG5GVwO", "reviewer": "Reviewer_Aczy", "summary": "This paper proposes MathConstruct, a new benchmark for mathematical reasoning based on constructive problems from math competitions. These problems are highly interesting, yet benchmarks generally avoid them due to the non unique answers. This paper contributes a suite of problems taken from past along with answer verifiers. The problems are shown to be generally very hard for most LLMs, and OpenAI o1 does substantially better, although also at much higher cost. The authors also propose systematic problem variations to probe for robustness, and evaluate agents with access to a Python interpreter. Most of the problems are hard to brute-force via code alone, although access to the interpreter generally enables models to do better (again with higher cost).", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for the constructive comments, and are happy to read that they find our work novel and relevant to the community, and our framework easy to work with. We address any remaining concerns below.\n\n**Q.1. Can any parts of the pipeline be automated? What challenges did the authors encounter when trying to automate them?**  \nAlthough certain elements of our pipeline can be readily automated, most aspects currently remain beyond the capabilities of state-of-the-art agents and models. We detail the three main components of the benchmark curation process below:\n- **Problem Curation**: One aspect of the pipeline where automation was partially successful involves the curation and filtering of constructive problems. Constructive problems can be identified according to the selection criteria specified in our paper. A small portion of our benchmark questions were automatically selected by GPT-4o-mini from a larger internal dataset, and subsequently processed manually by the authors. While there were still plenty of false positives among the selected problems, this did make the selection procedure easier for these questions.\n- **Verifier Function**: The most challenging part to automate is the creation of verification functions. Although we experimented briefly with automating this task, current models were unable to generate rigorous enough verification functions. Developing a robust verification function requires the identification of potential failure modes in model outputs, careful creation of efficient checkers, and creation of thorough test cases that cover all relevant edge cases. While future LLMs might be able to automate this, this currently remains out of reach for complex questions of MathConstruct.\n- **Problem Validation**: Another critical aspect is ensuring problem quality, which falls between problem curation and verifier function generation in terms of automation feasibility. We automated several aspects of this step. For example, confirming problems could not be solved through brute-force methods using LLMs, as detailed in the paper. However, each problem underwent additional validation through an internal peer-review process among the authors. Manual peer review is essential for catching small issues and ensuring nothing is missed. While automation can help, it currently cannot fully replace this process as one needs to be certain that problems are correct once processed through this review. Therefore, even in a fully automated pipeline, some form of human validation would remain necessary.\n\nIn conclusion, while investigating further automation opportunities is valuable future work, we emphasize the importance of prioritizing a smaller yet more rigorously curated benchmark to accurately measure model performance.", "claims_and_evidence": "Yes, they are clear", "methods_and_evaluation_criteria": "Yes", "theoretical_claims": "N/A", "experimental_designs_or_analyses": "Yes. The benchmark construction seems sounds (it involved a significant amount of manual analysis from students with experience in math competitions, so that part is hard to check, yet I think it is inevitable for constructing a high-quality dataset for this domain). The experimental analysis of frontier LLMs also seems sound: I checked the examples in the appendix, and the authors spent a decent amount of effort into getting parsing right, which is often a pain in these evaluations. I believe that the results reflect the model's capabilities, not any unsoundness in the pipeline (e.g. failure to parse answers, etc).", "relation_to_broader_scientific_literature": "This paper augments the literature in the evaluation of mathematical reasoning in LLMs by providing a class of problems that has been mostly ignored so far, due to the complexity of verifying answers. Although there are many benchmarks in general for \"mathematical reasoning\", none of them (as far as I know) contains constructive problems.", "essential_references_not_discussed": "N/A", "other_strengths_and_weaknesses": "### Other strengths\n\nThe paper finds that performance on standard benchmarks, which would make it seem like competition problems have almost been saturated already (e.g. MATH; and more recent results on AIME by various frontier labs), is not telling the full picture. Even neglected problems from the same difficulty region are still very challenging. The difference in performance between GPT-4o and Sonnet on AIME vs on MathConstruct is quite stark. The paper is clear, the results are significant for the community at large, especially now that mathematical reasoning became one of the main evaluations of frontier LLMs, as advertised extensively by model creators whenever they release models. \n\n### Weakness\n\nThe only issue might be that the dataset construction pipeline seems quite effortful for further work to expand. Human-curated datasets are very rarely expanded later (e.g., GSM8k -> GSM1k being a rare example). This doesn't diminish the value of the current benchmark or the results, but I think the work would be more \"future proof\" if some of the more labor intensive parts could have been automated (e.g., I could imagine an LLM-based pipeline doing a first pass on (a) filtering relevant problems from recent competitions, (b) writing a verifier and ensuring that the example solution verifies, etc, perhaps with manual review by humans only at the end).", "other_comments_or_suggestions": "N/A", "questions_for_authors": "Did the authors consider automating some parts of the pipeline, as suggested above (besides the quality checks, but I mean more for the construction of the problems per se)? If so, were there significant challenges that prevented this from making into the paper? This would be good for future work to be aware of.", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "2PhlVZSnxF", "reviewer": "Reviewer_S8Ey", "summary": "The paper presents MathConstruct, a new benchmark to test LLMs on constructive mathematical proofs with a symbolic verifier for correctness of each problem. Unlike traditional math benchmarks that focus on fixed numerical answer problems,  MathConstruct introduces 127 modified olympiad-level math problems, where tasks require constructing mathematical objects with some specific properties. The also evaluates 13 SOTA LLMs on the dataset, and the best LLM only achieved 41% accuracy, which highlights its difficulty.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank reviewer S8Ey for their review. We appreciate that they found MathConstruct to be an interesting benchmark, and our experimental design detailed. Below, we address their other questions:\n\n**Q.1. Does robust accuracy suitably measure the correctness of problem solving for a given question?**  \nYes, because all included variations require the same underlying solution strategy. Furthermore, we explicitly exclude brute-forceable variations, thereby preventing models from using shortcuts specific to any single problem instantiation. Therefore, if a model correctly applies the solution strategy across all four provided problem variations, it is very likely capable of generalizing this approach to other instantiations.\n\nMore fundamentally, the main goal of our benchmark does not depend on these specific metrics. Specifically, our benchmark aims to provide effective means of evaluating models on a new reasoning task, where relative accuracy between models is the primary metric of interest.\n\n**Q.2 Is the small dataset size a limitation?**  \nNo, this is not a limitation. Although our benchmark is smaller than datasets like MATH [1], it is significantly more challenging, is better verified, and incorporates variations designed to test model generalization. It is worth noting that many widely used benchmarks contain relatively small problem sets. For instance, the 2024/2025 AIME competitions, which are frequently used to evaluate reasoning capabilities, consist of only 30 problems each. Lastly, rigorous benchmarking requires carefully curated problems that are neither erroneous nor overly simplistic. Thus, the importance of high-quality examples outweighs dataset size.\n\n**Q.3. Are there ways to reduce the amount of manual labour involved in the construction of the benchmark?**  \nWe refer the reviewer to our response to **Q.1** of reviewer Aczy. \n\n**Q.4. What value do the variations add to the benchmark?**  \nThe variations we define have three main purposes:\n- **Reducing Variance**: Including variations effectively increases the benchmark size, thus reducing measurement variance.\n- **Problem Analysis**: We can perform several additional experiments, such as the one presented in Section 4.5, that analyze the effect of model variations on the model solutions.\n- **Reducing Contamination**: Variations guard against memorization, as a model encountering a known problem from its training data must successfully solve all variations.\n \n**Q.5. Is there a way to improve the performance of LLMs?**  \nYes, we already included several improvements designed to enhance model accuracy. Specifically, we implement parser feedback to ensure accurate interpretation of answers and evaluate agent-based approaches. Furthermore, prompted by the reviewer, we ran additional experiments evaluating an agent-based approach that obtains detailed feedback from the ground-truth verification function. These functions log each failure with a specific reason, and therefore allow the model to correct its answer based on this feedback. Using this approach, o3-mini (the best model) improves by an additional 12% (53%->65%). We stress that this experiment should not be considered valid for real-world applications due to lack of access to the verification function at inference time, but it does give an upper bound on what is possible. We will add a discussion about this result in the appendix of our paper.\n\nWe did consider an advanced agent-based approach where the model would first implement this verifier function itself and subsequently use it to validate its solution. However, preliminary experiments checking the automation feasibility of our benchmark showed that current models struggle significantly with this task. Thus, we currently consider this out of scope for this benchmark paper. \n\n**Q.6. Did the authors apply mitigations against contamination?**  \nFirst, we emphasize that our benchmark's problems rarely appear verbatim in existing training datasets. Notably, problems beyond the “Find Any”-category underwent substantial revision to become suitable constructive problems, and some were translated from other languages.\n\nSecond, we implemented a contamination detection strategy described in Section 4.4. Previous work shows that rewording mathematical problems can influence model performance in the presence of contamination [2]. By doing so, we observed minimal contamination of our benchmark.\n\n**Q.7. Can you include references to these additional works?**  \nWe appreciate the reviewer’s suggestion and will incorporate the additional references.\n\n[1] https://arxiv.org/abs/2103.03874  \n[2] https://arxiv.org/abs/2405.16281", "claims_and_evidence": "The paper claims that MathConstruct is a challenging benchmark for evaluating LLMs in mathematical reasoning. \nThe evidence is demonstrated by extensive experimental results on various models like GPT4o o1, and compared with brute-force approaches and analysed errors.", "methods_and_evaluation_criteria": "(i) The methods for problem selection, symbolic encoding, and evaluation are well-defined. The benchmark is designed with strict verification criteria, ensuring that models must generate correct constructions rather than relying on memorization. \n\n(ii) Evaluation metrics like average accuracy and robust accuracy in this paper are the correctness of constructed instances on selected variations of problems. However, many problems in this benchmark (e.g. IMO Shortlist 2014 C3 in Appendix B on Page 13) have infinitely many variants (here, variants include \\{(n,k) | n, k \\in \\mathbb{N}^+, n\\geq 2, k\\geq 1, k \\leq \\lfloor \\sqrt{n-1}\\rfloor \\}, but evaluations are done on small subsets of the infinite variants, which are insufficient to solve the problem. Overall, the metrics are not suitable enough for evaluating the correctness of problem-solving.", "theoretical_claims": "The paper does not make any new theoretical claim.", "experimental_designs_or_analyses": "The experimental design seems comprehensive, covering different LLMs and evaluation settings. The error analysis is detailed, revealing common failure modes in LLM.", "relation_to_broader_scientific_literature": "The paper is closely related to mathematical reasoning and somehow contributes to formal theorem proving.", "essential_references_not_discussed": "This paper cites all essential references in this research area, but could add the following:\n(i). Program-assisted LLM (PAL) paper in solution enumeration: [1] Gao, Luyu, et al. \"Pal: Program-aided language models.\" International Conference on Machine Learning. PMLR, 2023.\n(ii). Datasets: [2] Li, Jia, et al. \"Numinamath: The largest public dataset in ai4maths with 860k pairs of competition math problems and solutions.\" Hugging Face repository 13 (2024).", "other_strengths_and_weaknesses": "Strengths:\nThe paper introduces an interesting and challenging benchmark for evaluating LLM reasoning by constructive math problems.\n\nWeaknesses:\n1. The benchmark dataset is very small in size, containing only 127 problems in total. This amount of problems is insufficient to fine-tune an LLM on this task or conduct thorough/in-depth evaluation of constructive math problems. \n2. In addition, the dataset curation relies too much on manual laboring (including problem selection, verifier construction, and quality checks) , making it intractable to scale up. More data synthetic methods can be applied to create large-scale high-quality dataset.\n3. The “problem variations” in this paper are still limited to specific cases of problems. For example, on Page 4 Figure 3, the “variation” is different cases of $n$ in a problem, instead of a completely new problem adapted from original problem. \n4. Regarding the limitations in evaluation metrics, check the Methods and Evaluation Criteria section. \n5. The paper mentions that constructive proofs are challenging but does not propose any method to enhance or improve LLM’s capabilities in such tasks. It would be very interesting and contributive if the authors could implement any method and outperform the LLM baselines", "other_comments_or_suggestions": "N/A", "questions_for_authors": "How do you mitigate potential dataset contamination, especially since olympiad problems are commonly included in pre-training data? Have you provided another set of problems with timestamps after knowledge cutoffs of popular LLMs?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "XaRzDYWwl7", "reviewer": "Reviewer_6y3x", "summary": "This paper introduces MathConstruct, a novel mathematical benchmark designed to evaluate LLMs' reasoning in constructive proofs from high-school competition problems. The authors curated a dataset of 127 challenging problems from various sources and converted them into a unified format with symbolic parameters, enabling parameter variations and generating a total of 480 problem variants.\n\nTo rigorously assess LLMs on these tasks, MathConstruct provides Python-based verification code for each problem and incorporates a parser that prompts LLMs and delivers feedback to refine their responses toward the correct output.\n\nExperimental results reveal that current state-of-the-art LLMs (e.g., OpenAI o1) achieve only 41.08% average accuracy on the full set of 480 problems and 22.83% robust accuracy across all variants of the original 127 problems. Additionally, the authors conduct a comprehensive evaluation, employing code agents, brute-force methods, error analysis, and potential data contamination assessments.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank reviewer 6y3x for their review. We are delighted that they recognize MathConstruct as a valuable and novel contribution. We also appreciate their feedback on the clarity of our paper and will incorporate the suggested clarifications. Below, we address their additional questions:\n\n**Q.1. Could the authors evaluate more recent models on MathConstruct?**  \nWe have evaluated newly released frontier models, including o3-mini and DeepSeek R1, and provide an updated results table below:\n\n| Model | Avg | Robust | Cost |\n|----------------------|--------|--------|-------- |\n| Llama-3.1-405B | 3.17 | 1.59 | 1.99 |\n| GPT-4o-mini | 3.77 | 1.59 | 0.32 |\n| Llama-3.3-70B | 3.77 | 1.59 | 0.67 |\n| 3.5-Haiku | 3.37 | 1.59 | 1.37 |\n| GPT-4o | 3.57 | 0.79 | 4.62 |\n| 3.5-Sonnet | 4.17 | 0.79 | 4.80 |\n| Qwen2.5-72B | 6.35 | 1.59 | 2.24 |\n| Flash | 11.57 | 3.17 | N/A |\n| QwQ-Preview | 13.89 | 7.14 | 8.34 |\n| o1-mini | 25.46 | 10.32 | 51.49 |\n| Flash-Thinking | 27.05 | 11.11 | N/A |\n| R1 | 32.28 | 15.08 | 48.39 |\n| o1 | 41.34 | 23.02 | 434.08 |\n| o3-mini | **53.77** | **34.92** | 71.14 |\n\nWe observe that o3-mini significantly outperforms even o1, demonstrating stronger generalization and mathematical reasoning while being considerably more cost-efficient. R1, on the other hand, achieved an accuracy of only 32.3%.\n\n**Q.2. How many variants can be generated, and how were the 480 presented variants selected?**  \nMany of our problems, particularly those in the “Find Inf”-category, permit infinitely many variations. However, generating interesting variations is more challenging for other types of problems, as their constructions fail for most values. Additionally, for each problem, we manually defined a range of parameters to ensure two important conditions: (1) the problem is resistant to brute-force solutions, and (2) the resulting output remains within a 4,000-character limit. Most problems allow for at least four variations under these constraints, although a small number permit only two or three. Therefore, we generated up to four variations per problem or fewer if four were not feasible. In practice, many problems could include significantly more variations. This point is illustrated clearly in Figure 7, in which we use 24 variations for each of the ten “Find Inf”-problems discussed in this subsection.", "claims_and_evidence": "From my perspective, all claims made in the submission are supported by clear evidence.", "methods_and_evaluation_criteria": "I think the proposed benchmark and evaluation setting are well-motivated and make sense.", "theoretical_claims": "N/A", "experimental_designs_or_analyses": "I think the experiments are comprehensive and sound.", "relation_to_broader_scientific_literature": "I think the proposed benchmark serves as a valuable complement to existing mathematical reasoning benchmarks.", "essential_references_not_discussed": "I find the related work section to be thorough and well-researched.", "other_strengths_and_weaknesses": "I find the paper is well-motivated, novel, and overall well-written. It primarily evaluates LLMs on informal constructive proofs, while leveraging Python-based verification methods instead of formal theorem provers, making the approach more lightweight and accessible. The experiments and analysis are also quite comprehensive.\n\nI do not see any major weaknesses in the paper. However, one potential limitation is that constructive proofs in Olympiad mathematics may be relatively rare compared to other types of proof-based or computational problems.", "other_comments_or_suggestions": "I would say the paper is overall very strong, but there are some minor aspects that could be improved. If I understand correctly, the phrase \"symbolic problem statement in natural language\" in lines 182 and 211 could be more clearly written as \"problem statement in natural language with symbolic parameters.\" Additionally, the authors could consider evaluating DeepSeek R1 on their proposed benchmark to further enhance the comprehensiveness of the evaluation.", "questions_for_authors": "In principle, given the original 127 problems in MathConstruct, is it possible to generate an arbitrary number of variants for each problem? What design choices guided the selection of the 480 problem variants used in the benchmark?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: This research presents a challenging benchmark for assessing the reasoning capabilities of Large Language Models, utilizing constructive math problems and lightweight verifier. The reviewers unanimously provided positive evaluations, commending the novelty of the work, the clarity of its presentation, and the significance of the evaluation outcomes. However, several concerns were raised. These include the limited size of the dataset, the difficulty in automating the pipeline, the inadequacy of the metrics in accurately gauging the correctness of problem-solving approaches, and the relative scarcity of constructive proofs in mathematics. Despite these concerns, AC concurs that this benchmark is a valuable and timely contribution for evaluating reasoning models, and thus recommends acceptance.
Decision: Accept (poster)