論文の概要: FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models

• arxiv url: http://arxiv.org/abs/2505.02735v1
• Date: Mon, 05 May 2025 15:37:00 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-06 18:49:35.729041
• Title: FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models
• Title（参考訳）: FormalMATH:大規模言語モデルの形式的推論のベンチマーク
• 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,
• Abstract要約: 本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。 本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。 現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
• 参考スコア（独自算出の注目度）: 17.919212265668783
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.
• Abstract（参考訳）: 形式的な数学的推論は、既存のベンチマークのスコープとスケールの制限によって妨げられている、人工知能にとって重要な課題である。 そこで本研究では,高校のオリンピアード問題から,様々な領域(代数,応用数学,計算学,数論,離散数学など)にまたがる学部レベルの定理まで,5,560の証明済み問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。 手動の形式化の効率を損なうために,(1)文の自動形式化のための特殊な大規模言語モデル(LLM),(2)マルチLLMセマンティックな検証,(3)オフザシェルのLCMベースのプローバーを用いた否定に基づく防音フィルタ戦略を導入する。 このアプローチは、手作業による検証の前に72.09%のステートメントを保持しながら、元の自然言語問題に対する忠実性を確保することによって、専門家のアノテーションコストを削減する。 最強モデルでさえ、実用的なサンプリング予算の下では16.46%の成功率しか達成できず、明らかにドメインバイアス(例えば、代数に優れ、計算に失敗する)を示し、自動化戦術の単純化に過度に依存している。 特に,自然言語による解法指導とチェーン・オブ・シークレット推論における証明成功の反直感的逆関係を同定し,人間の手書きの非公式推論は,形式的推論設定における明瞭さよりもノイズを導入することを示唆している。 我々は、フォーマルな数学的推論をベンチマークするための堅牢なベンチマークをFormalMATHが提供していると信じている。

関連論文リスト

• Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models [86.45058529521258]
  OlymMATHは、LLMの複雑な推論能力を厳格にテストするために設計された、Olympiadレベルの新しい数学ベンチマークである。 OlymMATHは200の厳密にキュレートされた問題があり、それぞれが手動で検証され、英語と中国語の並行バージョンで利用可能である。
  論文  参考訳（メタデータ） (2025-03-27T11:20:17Z)
• Large Language Models and Mathematical Reasoning Failures [1.6114012813668932]
  本稿では,50の高校レベルの単語問題を用いた大規模言語モデル(LLM)の数学的推論能力について検討する。 最終回答と解決手順の両方を厳格に分析して、推論の失敗を特定します。 より新しいモデル(例えば、o3-mini、deepseek-r1)はより精度が高いが、全てのモデルは空間的推論、戦略的計画、算術における誤りを示す。
  論文  参考訳（メタデータ） (2025-02-17T09:07:32Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4 [0.0]
  本稿では,Large Language Models (LLMs) を用いて,形式的証明ステップと完全形式的証明を生成する。 目標は、AIをどのように活用して数学的形式化プロセスを支援し、パフォーマンスを向上させるかを決定することである。
  論文  参考訳（メタデータ） (2024-09-09T18:21:28Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。