FormalMATH: 대규모 언어 모델의 형식적 수학적 추론 능력 벤치마킹

FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models

May 5, 2025

저자: 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

cs.AI

초록

형식적 수학적 추론은 여전히 인공지능의 주요 과제로 남아 있으며, 기존 벤치마크의 범위와 규모의 한계로 인해 더욱 어려움을 겪고 있다. 이를 해결하기 위해 우리는 고등학교 올림피아드 문제부터 학부 수준의 정리까지 다양한 영역(예: 대수학, 응용수학, 미적분학, 정수론, 이산수학)에 걸친 5,560개의 형식적으로 검증된 문제로 구성된 대규모 Lean4 벤치마크인 FormalMATH를 제시한다. 수동 형식화의 비효율성을 완화하기 위해, 우리는 다음과 같은 요소를 통합한 새로운 인간-참여형 자동 형식화 파이프라인을 도입한다: (1) 문장 자동 형식화를 위한 특화된 대형 언어 모델(LLM), (2) 다중 LLM 의미 검증, (3) 기성 LLM 기반 증명기를 활용한 부정 기반 반증 필터링 전략. 이 접근법은 전문가 주석 비용을 줄이면서도 원본 자연어 문제에 대한 충실도를 유지하며, 수동 검증 전에 72.09%의 문장을 보존한다. 최신 LLM 기반 정리 증명기에 대한 평가 결과, 가장 강력한 모델조차도 실질적인 샘플링 예산 하에서 16.46%의 성공률을 보이며, 특정 영역에 대한 편향(예: 대수학에서는 우수하지만 미적분학에서는 실패)과 단순화된 자동화 전술에 대한 과도한 의존성을 보였다. 특히, 우리는 사고 연쇄 추론 시나리오에서 자연어 해결 지침과 증명 성공률 간의 역설적인 역관계를 발견했는데, 이는 인간이 작성한 비형식적 추론이 형식적 추론 환경에서 명확성보다는 오히려 잡음을 유발한다는 것을 시사한다. 우리는 FormalMATH가 형식적 수학적 추론을 벤치마킹하기 위한 견고한 기준을 제공한다고 믿는다.

English

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.