FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models
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
2025-05-06
Summary
This paper talks about FormalMATH, a new way to test how well large language models can handle formal math problems by using a huge collection of math questions and an automatic system to turn regular math into a format computers can understand.
What's the problem?
It's really hard and time-consuming for people to write out math problems in a way that computers can use for formal proofs, and current AI models still struggle to solve these kinds of problems accurately.
What's the solution?
The researchers created a big set of formal math problems and built a tool that automatically changes normal math into computer-friendly language, making it easier to test and improve AI's math skills.
Why it matters?
This matters because it helps scientists see where AI needs to get better at real math reasoning, which is important for everything from science and engineering to making sure AI can help with complex problem-solving in the future.
Abstract
FormalMATH, a large-scale Lean4 benchmark, introduces an autoformalization pipeline to reduce manual annotation costs and identifies limitations of existing LLM-based theorem provers in formal mathematical reasoning.