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

要旨

形式的数学推論は、人工知能にとって依然として重要な課題であり、既存のベンチマークの範囲と規模の制約によって妨げられています。これを解決するため、私たちはFormalMATHを提案します。これは、高校のオリンピック問題から大学レベルの定理まで、多様な領域（代数、応用数学、微積分、数論、離散数学など）にわたる5,560個の形式的に検証された問題を含む大規模なLean4ベンチマークです。手動での形式化の非効率性を軽減するため、以下の要素を統合した新しい人間参加型自動形式化パイプラインを導入します：(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.