# FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models

**Authors:** Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, Yandong Wen, Ge Zhang, Weiyang Liu  
**arXiv:** [2505.02735](https://arxiv.org/abs/2505.02735)  
**Date:** 2025-05-05  
**Summary page:** https://www.summarizepaper.com/en/paper/2505.02735v1/

## Key points

- Formal mathematical reasoning is a significant challenge for artificial intelligence due to limitations in existing benchmarks
- FormalMATH is a comprehensive benchmark introduced by a team of researchers led by Zhouliang Yu, Ruotian Peng, and others
- It features 5,560 formally verified problems across various mathematical domains like algebra, calculus, number theory, and discrete mathematics
- The researchers developed a human-in-the-loop autoformalization pipeline to streamline the formalization process and reduce manual effort
- State-of-the-art LLM-based theorem provers within FormalMATH's framework had limitations with only a 16.46% success rate under practical sampling budgets
- Models exhibited domain bias excelling in areas like algebra but struggling in others such as calculus
- An unexpected inverse relationship was identified between natural-language solution guidance and proof success in chain-of-thought reasoning scenarios
- FormalMATH serves as a robust benchmark for evaluating formal mathematical reasoning capabilities with its extensive problem collection and innovative autoformalization pipeline approach

## Summary

FormalMATH: A Comprehensive Benchmark for Evaluating Formal Mathematical Reasoning Capabilities

Formal mathematical reasoning poses a significant challenge for artificial intelligence due to the limitations of existing benchmarks in terms of scope and scale. In response to this challenge, a team of researchers led by Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, Yandong Wen, Ge Zhang and Weiyang Liu have introduced FormalMATH. This innovative benchmarking system is built on the Lean4 platform and features an extensive collection of 5,560 formally verified problems across various mathematical domains such as algebra, applied mathematics, calculus, number theory and discrete mathematics. To streamline the formalization process and reduce manual effort involved in verifying statements within FormalMATH's dataset,the researchers have developed a cutting-edge human-in-the-loop autoformalization pipeline. This pipeline incorporates specialized large language models (LLMs) for statement autoformalization along with multi-LLM semantic verification and negation-based disproof filtering strategies using off-the-shelf LLM-based provers. By leveraging these advanced techniques,the team has managed to significantly decrease expert annotation costs while maintaining a high level of fidelity to the original natural-language problems. In their evaluation of state-of-the-art LLM-based theorem provers within FormalMATH's framework,the researchers uncovered notable limitations.Even the most powerful models achieved only a 16.46% success rate under practical sampling budgets.Furthermore ,these models exhibited domain bias by excelling in certain areas like algebra while struggling in others such as calculus.The study also revealed an over-reliance on simplified automation tactics among these models. One intriguing finding from their research was the identification of an unexpected inverse relationship between natural-language solution guidance and proof success in chain-of-thought reasoning scenarios. This discovery suggests that human-written informal reasoning may introduce noise rather than clarity in formal reasoning settings. Overall, FormalMATH stands out as a robust benchmark for evaluating formal mathematical reasoning capabilities. With its comprehensive set of verified problems and innovative autoformalization pipeline approach, this tool promises to advance AI's ability to tackle complex mathematical challenges effectively. For further details on this project including technical specifications and additional resources visit: https://sphere-ai-lab.github.io/FormalMATH/.