Proof2Hybrid: Automatic Mathematical Benchmark Synthesis for Proof-Centric Problems
cs.CL, cs.AI
Submitted: 2025-08-04
Updated: 2026-08-29
Code: https://github.com/RenBing-Sumeru/Proof2Hybrid
License: http://creativecommons.org/licenses/by/4.0/
The gist: Evaluating the mathematical capability of Large Language Models (LLMs) is a critical yet challenging frontier.
Terminology
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.
Sources
- Wisdom from Diversity: Bias Mitigation Through Hybrid Human-LLM Crowds
- Training Verifiers to Solve Math Word Problems
- DeepSeek-V3 Technical Report
- Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Models
- FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI
- DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning
- Measuring Mathematical Problem Solving With the MATH Dataset
- Winning Gold at IMO 2025 with a Model-Agnostic Verification-and-Refinement Pipeline
- Motivated proofs: What they are, why they matter and how to write them
- Humanity's Last Exam
- Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models
- PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
- Do Large Language Model Benchmarks Test Reliability?
- A Survey on Large Language Models for Mathematical Reasoning
- MMLU-Pro: A More Robust and Challenging Multi-Task Language Understanding Benchmark
- Qwen3 Technical Report
- Qwen2.5 Technical Report
Related papers
- Exploring Solution Divergence and Its Effect on Large Language Model Problem Solving
- Ishigaki-IDS-Bench: A Benchmark for Generating Information Delivery Specification from BIM Information Requirements
- Subliminal Steering: Stronger Encoding of Hidden Signals
- MedStruct-S: A Benchmark for Key Discovery, Key-Conditioned QA and Semi-Structured Extraction from OCR Clinical Reports
- The End of Transformers? On Challenging Attention and the Rise of Sub-Quadratic Architectures
- Untangling the Mechanisms of Misleading Context in Medical Question Answering