FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , , , , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866915273833971712 |
|---|---|
| author | Yu, Zhouliang Peng, Ruotian Ding, Keyi Li, Yizhe Peng, Zhongyuan Liu, Minghao Zhang, Yifan Yuan, Zheng Xin, Huajian Huang, Wenhao Wen, Yandong Zhang, Ge Liu, Weiyang |
| author_facet | Yu, Zhouliang Peng, Ruotian Ding, Keyi Li, Yizhe Peng, Zhongyuan Liu, Minghao Zhang, Yifan Yuan, Zheng Xin, Huajian Huang, Wenhao Wen, Yandong Zhang, Ge Liu, Weiyang |
| contents | Formal mathematical reasoning remains a critical challenge for artificial intelligence, hindered by limitations of existing benchmarks in scope and scale. To address this, we present FormalMATH, a large-scale Lean4 benchmark comprising 5,560 formally verified problems spanning from high-school Olympiad challenges to undergraduate-level theorems across diverse domains (e.g., algebra, applied mathematics, calculus, number theory, and discrete mathematics). To mitigate the inefficiency of manual formalization, we introduce a novel human-in-the-loop autoformalization pipeline that integrates: (1) specialized large language models (LLMs) for statement autoformalization, (2) multi-LLM semantic verification, and (3) negation-based disproof filtering strategies using off-the-shelf LLM-based provers. This approach reduces expert annotation costs by retaining 72.09% of statements before manual verification while ensuring fidelity to the original natural-language problems. Our evaluation of state-of-the-art LLM-based theorem provers reveals significant limitations: even the strongest models achieve only 16.46% success rate under practical sampling budgets, exhibiting pronounced domain bias (e.g., excelling in algebra but failing in calculus) and over-reliance on simplified automation tactics. Notably, we identify a counterintuitive inverse relationship between natural-language solution guidance and proof success in chain-of-thought reasoning scenarios, suggesting that human-written informal reasoning introduces noise rather than clarity in the formal reasoning settings. We believe that FormalMATH provides a robust benchmark for benchmarking formal mathematical reasoning. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_02735 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models Yu, Zhouliang Peng, Ruotian Ding, Keyi Li, Yizhe Peng, Zhongyuan Liu, Minghao Zhang, Yifan Yuan, Zheng Xin, Huajian Huang, Wenhao Wen, Yandong Zhang, Ge Liu, Weiyang Artificial Intelligence Machine Learning Formal mathematical reasoning remains a critical challenge for artificial intelligence, hindered by limitations of existing benchmarks in scope and scale. To address this, we present FormalMATH, a large-scale Lean4 benchmark comprising 5,560 formally verified problems spanning from high-school Olympiad challenges to undergraduate-level theorems across diverse domains (e.g., algebra, applied mathematics, calculus, number theory, and discrete mathematics). To mitigate the inefficiency of manual formalization, we introduce a novel human-in-the-loop autoformalization pipeline that integrates: (1) specialized large language models (LLMs) for statement autoformalization, (2) multi-LLM semantic verification, and (3) negation-based disproof filtering strategies using off-the-shelf LLM-based provers. This approach reduces expert annotation costs by retaining 72.09% of statements before manual verification while ensuring fidelity to the original natural-language problems. Our evaluation of state-of-the-art LLM-based theorem provers reveals significant limitations: even the strongest models achieve only 16.46% success rate under practical sampling budgets, exhibiting pronounced domain bias (e.g., excelling in algebra but failing in calculus) and over-reliance on simplified automation tactics. Notably, we identify a counterintuitive inverse relationship between natural-language solution guidance and proof success in chain-of-thought reasoning scenarios, suggesting that human-written informal reasoning introduces noise rather than clarity in the formal reasoning settings. We believe that FormalMATH provides a robust benchmark for benchmarking formal mathematical reasoning. |
| title | FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models |
| topic | Artificial Intelligence Machine Learning |
| url | https://arxiv.org/abs/2505.02735 |