MathConstruct: Challenging LLM Reasoning with Constructive Proofs

TL;DR

MathConstruct tackles a gap in evaluating mathematical reasoning by focusing on constructive proofs, where models must explicitly construct objects satisfying given constraints and whose correctness can be verified automatically. The benchmark encodes problems symbolically with parameterized formulations, a verifier function, and formatting instructions, and it generates numerous variations to test robustness. Across 14 state-of-the-art LLMs, even the best models achieve around $60\%$ accuracy, with robust performance significantly lower, highlighting remaining gaps in constructive reasoning and verification. The work also provides rigorous problem review, automated quality checks, and an open-source pipeline, underscoring the benchmark’s potential to drive future improvements in AI-assisted mathematical reasoning and benchmarking practices.

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 121 challenging problems sourced from various math competitions, which targets constructive proofs, a widely encountered problem type requiring the construction of mathematical objects with specific properties. These proofs are particularly suitable for LLM evaluation, as solution correctness can be easily verified. Our automated verifiers also enable MathConstruct to generate problem variations, used to evaluate robustness. State-of-the-art LLMs solve only 60% of MathConstruct problems, highlighting its complexity and importance for LLM evaluation.

Figures (14)

• Figure 1: Accuracy of LLMs on MathConstruct, highlighting the difficulty of constructive proofs. We compute Robust Accuracy by requiring the model to consistently solve a problem across a set of problem variations.
• Figure 2: Two sample problems from MathConstruct, each consisting of a natural language statement and a verifier function that returns a 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.
• Figure 3: A problem encoding consisting of a symbolic problem statement $P$, concrete parameters $\theta$, and a verification function $V_\theta$. We also implement a variation generator, and provide formatting instructions for the construction.
• Figure 4: Cost and accuracy of models with or without code execution. Future cost of Flash is estimated (now free).
• Figure 5: Error types of models before and after parser feedback.

Theorems & Definitions (2)

• Definition 3.1: Construction Problem
• Definition 3.2: Problem Variations