Construction-Verification: A Benchmark for Applied Mathematics in Lean 4
Bowen Yang, Yi Yuan, Chenyi Li, Ziyu Wang, Liangqi Li, Bo Zhang, Zhe Li, Zaiwen Wen
TL;DR
AMBER introduces a construction-verification benchmark in Lean 4 to evaluate applied mathematics reasoning, requiring explicit solution construction before verification across evaluation, algorithm design, representation transformation, and theorem proving. The benchmark spans convex analysis, optimization, numerical algebra, and high-dimensional probability, and includes expert-driven difficulty assessment and a dependency-density analysis to quantify formal complexity. Experiments show general-purpose models outperform specialized provers on constructive tasks, highlighting a tactical overfitting gap and the need for end-to-end neuro-symbolic approaches that integrate algorithmic synthesis with formal verification. The work demonstrates the practical significance of enforcing constructive reasoning for reliable formalization of applied mathematics and sets a benchmark for future research in this space.
Abstract
Recent advances in large language models have demonstrated impressive capabilities in mathematical formalization. However, existing benchmarks focus on logical verification of declarative propositions, often neglecting the task of explicitly synthesizing solutions. This limitation is particularly acute in applied mathematics domains, where the goal is frequently to derive concrete values or executable algorithms rather than solely proving theorems. To address this, we introduce a Lean 4 framework that enforces a construction-verification workflow, compelling the agent to define explicit solutions before proving their correctness. We curate a comprehensive benchmark AMBER (Applied Mathematics BEnchmark for Reasoning) spanning core domains of applied mathematics, including convex analysis, optimization, numerical algebra, and high-dimensional probability. Aside from theorem proving, our benchmark features complex tasks such as evaluation, algorithm design, and representation transformation. Experiments reveal that current models face significant difficulties with these constructive tasks. Notably, we observe that general-purpose reasoning models consistently outperform specialized theorem provers. We attribute this to a degradation of instruction following capabilities in specialized models. Fine-tuning on proof corpora appears to induce ``tactical overfitting", compromising the ability to adhere to complex constructive requirements, whereas general models retain the versatility needed for multi-task formal reasoning.