Proof2Hybrid: Automatic Mathematical Benchmark Synthesis for Proof-Centric Problems

TL;DR

Proof2Hybrid is an automated framework that synthesizes proof-centric mathematical benchmarks from natural language corpora, enabling more accurate evaluation of LLMs' mathematical reasoning abilities, demonstrated through the AlgGeoTest benchmark.

Contribution

The paper introduces Proof2X, a novel method for converting proofs into verifiable questions, and creates AlgGeoTest, a new algebraic geometry benchmark for assessing LLMs.

Findings

LLMs show significant gaps in understanding algebraic geometry

The hybrid question format improves robustness of evaluation

Automated benchmark synthesis scales evaluation of mathematical reasoning

Abstract

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.