Proof2Hybrid: Automatic Mathematical Benchmark Synthesis for Proof-Centric Problems
This addresses the problem of scalable and accurate mathematical evaluation for AI researchers, though it is incremental as it builds on existing benchmark synthesis methods.
The authors tackled the challenge of evaluating mathematical capabilities in Large Language Models (LLMs) by proposing Proof2Hybrid, an automated framework that synthesizes proof-centric benchmarks from natural language corpora, resulting in AlgGeoTest with 456 items that revealed profound deficits in LLMs' comprehension of algebraic geometry.
Evaluating the mathematical capability of Large Language Models (LLMs) is a critical yet challenging frontier. Existing benchmarks fall short, particularly for proof-centric problems, as manual creation is unscalable and costly, leaving the true mathematical abilities of LLMs largely unassessed. To overcome these barriers, we propose Proof2Hybrid, the first fully automated framework that synthesizes high-quality, proof-centric benchmarks from natural language mathematical corpora. The key novelty of our solution is Proof2X, a roadmap of converting mathematical proofs into various kinds of questions that are easy to verify. Instructed by this roadmap, we propose a new type of hybrid-formatted questions, named ``$m$-out-of-$n$ multiple judge questions'', specifically designed to enable robust, automatic evaluation while being resilient to guessing and superficial pattern matching inherent in traditional formats. As a demonstration of our framework, we introduce AlgGeoTest, a benchmark for algebraic geometry--a frontier domain of modern mathematics--comprising 456 challenging items. Our extensive evaluations on state-of-the-art LLMs using AlgGeoTest reveal profound deficits in their comprehension of algebraic geometry, providing a more precise measure of their true mathematical capabilities. Our framework and benchmark pave the way for a new wave of in-depth research into the mathematical intelligence of AI systems.