paper-with-me

Papers

Proof2Hybrid: Automatic Mathematical Benchmark Synthesis for Proof-Centric Problems

2025-08-04 · Yebo Peng, Zixiang Liu, Yaoming Li, Zhizhuo Yang, Xinye Xu, Bowen Ye, Weijun Yuan, Zihan Wang, Tong Yang arxiv

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.

📄 PDF Abstract BibTeX arXiv:2508.02208

Code (0)

등록된 구현이 없습니다.

Similar Papers 제목 키워드 기반

HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement

2025-05-21 · Jilin Hu, Jianyu Zhang, Yongwang Zhao, Talia Ringer

Formal methods is pivotal for verifying the reliability of critical systems through rigorous mathematical proofs. However, its adoption is hindered by labor-intensive manual proofs and the expertise required to use theor…

Automated Theorem ProvingMathematical Proofs

Deep Network Guided Proof Search

2017-01-24 · Sarah Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk

Deep learning techniques lie at the heart of several significant AI advances in recent years including object recognition and detection, image captioning, machine translation, speech recognition and synthesis, and playin…

Deep LearningGame of GoImage CaptioningMachine Translation+4

Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification

2024-12-18 · Kyle Thompson, Nuno Saavedra, Pedro Carrott, Kevin Fisher 외

Formal verification using proof assistants, such as Coq, enables the creation of high-quality software. However, the verification process requires significant expertise and manual effort to write proofs. Recent work has …

Retrieval

Mask-Proof: An LLM-based Automated Data Curation Pipeline on Mathematical Proofs

2026-06-13 · Jierui Zhang, Siyuan Tan, Xinhang Li, Longzhuangzhi Lin 외 arxiv

Large language models (LLMs) are increasingly capable of mathematical problem solving and can even assist with research-level proofs, yet we still lack a scalable and reproducible way to measure step-level reasoning in l…

Mathematical Reasoning

Autoformalization with Large Language Models

2022-05-25 · Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe 외

Autoformalization is the process of automatically translating from natural language mathematics to formal specifications and proofs. A successful autoformalization system could advance the fields of formal verification, …

Automated Theorem ProvingProgram Synthesis