Search papers, labs, and topics across Lattice.
This paper introduces MathAdv, a comprehensive diagnostic benchmark designed to assess the capabilities of theorem provers across 13 mathematical domains, addressing limitations in existing benchmarks that focus solely on aggregate proof accuracy. The evaluation reveals critical insights, including that formalization is a significant bottleneck, performance varies widely by domain, and that natural-language guidance can both aid general-purpose LLMs and hinder specialized proof models. Importantly, the study highlights how evaluating models through component-wise tasks can uncover nuanced capabilities and failure modes that traditional accuracy metrics overlook.
Formalization is a major bottleneck in theorem proving, with performance varying dramatically across mathematical domains and problem presentations.
Formal theorem proving enables machine-verifiable evaluation of mathematical reasoning, yet existing benchmarks often emphasize aggregate proof accuracy, concentrate on a narrow range of mathematics, and provide limited evidence of robustness to equivalent reformulations. We introduce MathAdv, a diagnostic benchmark spanning 13 domains across undergraduate- and graduate-level mathematics. Alongside Lean 4 theorem proving, MathAdv provides up to three auxiliary tasks: multiple-choice questions that probe mathematical knowledge, fill-in-the-blank problems that isolate informal reasoning, and expert-crafted transformations that test robustness to problem presentation. Our evaluation of contemporary theorem provers yields four findings: formalization remains a major bottleneck; performance varies substantially across mathematical domains; natural-language guidance helps general-purpose LLMs but can hinder proof-specialized models; and mathematically equivalent reformulations expose substantial robustness limitations. Together, these results show how component-wise evaluation can reveal model capabilities and failure modes that aggregate theorem-proving accuracy obscures. The dataset and evaluation scripts are available at https://github.com/margotyjx/MathAdv.git.
