IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generation
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909816623988736 |
|---|---|
| author | Schmitt, Johannes Bérczi, Gergely Dekoninck, Jasper Feusi, Jeremy Gehrunger, Tim Appenzeller, Raphael Bryan, Jim Canova, Niklas de Wolff, Timo Gaia, Filippo van Garrel, Michel Hashemi, Baran Holmes, David Lopez, Aitor Iribar Jaeck, Victor Jørgensen, Martina Kelk, Steven Kuhlmann, Stefan Kurpisz, Adam Meroni, Chiara Metzler, Ingmar Möller, Martin Muñoz-Echániz, Samuel Nowak, Robert Oberdieck, Georg Platt, Daniel Possamaï, Dylan Ribeiro, Gabriel Galán, Raúl Sánchez Sun, Zheming Teichmann, Josef Thomas, Richard P. Vial, Charles |
| author_facet | Schmitt, Johannes Bérczi, Gergely Dekoninck, Jasper Feusi, Jeremy Gehrunger, Tim Appenzeller, Raphael Bryan, Jim Canova, Niklas de Wolff, Timo Gaia, Filippo van Garrel, Michel Hashemi, Baran Holmes, David Lopez, Aitor Iribar Jaeck, Victor Jørgensen, Martina Kelk, Steven Kuhlmann, Stefan Kurpisz, Adam Meroni, Chiara Metzler, Ingmar Möller, Martin Muñoz-Echániz, Samuel Nowak, Robert Oberdieck, Georg Platt, Daniel Possamaï, Dylan Ribeiro, Gabriel Galán, Raúl Sánchez Sun, Zheming Teichmann, Josef Thomas, Richard P. Vial, Charles |
| contents | As the mathematical capabilities of large language models (LLMs) improve, it becomes increasingly important to evaluate their performance on research-level tasks at the frontier of mathematical knowledge. However, existing benchmarks are limited, as they focus solely on final-answer questions or high-school competition problems. To address this gap, we introduce IMProofBench, a private benchmark consisting of 39 peer-reviewed problems developed by expert mathematicians. Each problem requires a detailed proof and is paired with subproblems that have final answers, supporting both an evaluation of mathematical reasoning capabilities by human experts and a large-scale quantitative analysis through automated grading. Furthermore, unlike prior benchmarks, the evaluation setup simulates a realistic research environment: models operate in an agentic framework with tools like web search for literature review and mathematical software such as SageMath. Our results show that current LLMs can succeed at the more accessible research-level questions, but still encounter significant difficulties on more challenging problems. Quantitatively, Grok-4 achieves the highest accuracy of 52% on final-answer subproblems, while GPT-5 obtains the best performance for proof generation, achieving a fully correct solution for 22% of problems. IMProofBench will continue to evolve as a dynamic benchmark in collaboration with the mathematical community, ensuring its relevance for evaluating the next generation of LLMs. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_26076 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generation Schmitt, Johannes Bérczi, Gergely Dekoninck, Jasper Feusi, Jeremy Gehrunger, Tim Appenzeller, Raphael Bryan, Jim Canova, Niklas de Wolff, Timo Gaia, Filippo van Garrel, Michel Hashemi, Baran Holmes, David Lopez, Aitor Iribar Jaeck, Victor Jørgensen, Martina Kelk, Steven Kuhlmann, Stefan Kurpisz, Adam Meroni, Chiara Metzler, Ingmar Möller, Martin Muñoz-Echániz, Samuel Nowak, Robert Oberdieck, Georg Platt, Daniel Possamaï, Dylan Ribeiro, Gabriel Galán, Raúl Sánchez Sun, Zheming Teichmann, Josef Thomas, Richard P. Vial, Charles Computation and Language As the mathematical capabilities of large language models (LLMs) improve, it becomes increasingly important to evaluate their performance on research-level tasks at the frontier of mathematical knowledge. However, existing benchmarks are limited, as they focus solely on final-answer questions or high-school competition problems. To address this gap, we introduce IMProofBench, a private benchmark consisting of 39 peer-reviewed problems developed by expert mathematicians. Each problem requires a detailed proof and is paired with subproblems that have final answers, supporting both an evaluation of mathematical reasoning capabilities by human experts and a large-scale quantitative analysis through automated grading. Furthermore, unlike prior benchmarks, the evaluation setup simulates a realistic research environment: models operate in an agentic framework with tools like web search for literature review and mathematical software such as SageMath. Our results show that current LLMs can succeed at the more accessible research-level questions, but still encounter significant difficulties on more challenging problems. Quantitatively, Grok-4 achieves the highest accuracy of 52% on final-answer subproblems, while GPT-5 obtains the best performance for proof generation, achieving a fully correct solution for 22% of problems. IMProofBench will continue to evolve as a dynamic benchmark in collaboration with the mathematical community, ensuring its relevance for evaluating the next generation of LLMs. |
| title | IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generation |
| topic | Computation and Language |
| url | https://arxiv.org/abs/2509.26076 |