FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models

要約

形式的な数学的推論は、人工知能にとって依然として重要な課題であるが、既存のベンチマークの範囲と規模の限界によって妨げられている。この課題に対処するために、我々はFormalMATHを発表する。FormalMATHは、高校生のオリンピックの課題から、多様な領域（代数、応用数学、微積分、整数論、離散数学など）にまたがる学部レベルの定理まで、5,560の形式的に検証された問題からなる大規模なLean4ベンチマークである。(1)文の自動形式化のための特殊な大規模言語モデル(LLM)、(2)マルチLLM意味検証、(3)市販のLLMベースの証明器を使用した否定ベースの反証フィルタリング戦略。このアプローチでは、元の自然言語問題への忠実性を確保しつつ、手作業による検証の前に72.09%の文を保持することで、専門家のアノテーションコストを削減する。最先端のLLMベースの定理証明器を評価した結果、重大な限界が明らかになった。最も強力なモデルでさえ、実用的なサンプリング予算下では16.46%の成功率しか達成できず、顕著なドメインの偏り（例えば、代数学では優れているが微積分学では失敗する）と、単純化された自動化戦術への過度の依存を示す。特筆すべきは、自然言語による解答ガイダンスと思考連鎖推論シナリオにおける証明の成功率の間に、直感に反する逆相関があることで、人間が書いた非公式な推論は、形式的な推論設定において明確さよりもノイズをもたらすことを示唆している。我々は、FormalMATHが形式的な数学的推論をベンチマークするための強固なベンチマークを提供すると信じている。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, DeepL