論文の概要: Benchmarking Testing in Automated Theorem Proving

• arxiv url: http://arxiv.org/abs/2604.23698v1
• Date: Sun, 26 Apr 2026 13:24:20 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-28 17:12:07.504721
• Title: Benchmarking Testing in Automated Theorem Proving
• Title（参考訳）: 自動定理証明におけるベンチマークテスト
• Abstract要約: T は形式定理の意味的正しさを評価する枠組みである。 5つの実世界のLean 4リポジトリからベンチマークを構築します。 実験により、最先端のモデルでは高いコンパイル成功を達成できるが、セマンティック・メトリックでは著しく性能が低下することが示された。
• 参考スコア（独自算出の注目度）: 39.65133452374143
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent advances in large language models (LLMs) have shown promise in formal theorem proving, yet evaluating semantic correctness remains challenging. Existing evaluations rely on indirect proxies such as lexical overlap with human-annotated proof, or expensive manual inspection. Inspired by the shift from lexical comparison to test-based evaluation in code generation, we propose T , a framework that evaluates the semantic correctness of formal theorems: a generated theorem is considered correct only if all dependent successor theorems compile successfully, analogous to integration testing. We construct a benchmark from 5 real-world Lean 4 repositories, comprising 2,206 problems paired with 41 successor theorems on average, automatically extracted without human effort. Experiments demonstrate that while state-of-the-art models achieve high compilation success, they perform significantly worse under our semantic metric. The best model, Claude-Sonnet-4.5, achieves only 38.9% Testing Accuracy on the full set, given both natural language proof and successor theorems as context, revealing a critical gap in current theorem generation capabilities.
• Abstract（参考訳）: 大規模言語モデル(LLM)の最近の進歩は、形式的定理の証明において有望であることを示しているが、意味的正当性を評価することは依然として困難である。 既存の評価は、人間による注釈付き証明と語彙的重複や高価な手動検査のような間接的プロキシに依存している。 コード生成における語彙比較からテストベース評価へのシフトに着想を得て,形式定理の意味的正当性を評価するフレームワークTを提案する。 我々は5つの実世界のLean 4リポジトリからベンチマークを構築し、平均41の後継者定理と組み合わせた2,206の問題を人間の努力なしに自動的に抽出した。 実験により、最先端のモデルでは高いコンパイル成功を達成できるが、セマンティック・メトリックでは著しく性能が低下することが示された。 最良のモデルであるClaude-Sonnet-4.5は、自然言語の証明と後継定理の両方を文脈として、完全集合上でのテスト精度を38.9%しか達成していない。

関連論文リスト

• FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence [9.041607777624504]
  FaithSieveは、自然言語の数学的証明を詳細に評価するためのリーン支援フレームワークである。 証明段階を局所的推論単位に分解し、型付き証明義務を抽出し、検証する。 350-problemのOlympiadデータセットでは、GPT-5.4バックボーンを使用したFaithSieveは81.43%の正確なファーストエラー精度を実現している。
  論文  参考訳（メタデータ） (2026-08-26T18:43:30Z)
• FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models [53.68149869349268]
  大規模言語モデル(LLM)は、自動理論計算機科学(TCS)研究の可能性を増大させている。 我々は、最前線のエンドツーエンドのTCS研究でLSMを評価するための専門家検証ベンチマークである ourbenchmarkを紹介した。
  論文  参考訳（メタデータ） (2026-08-20T15:13:41Z)
• TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics [6.168228844241134]
  TheoremBenchは、コンテストの設定を超えて定理の証明者を評価するために設計されたLean4ベンチマークである。 このベンチマークは100近い古典的定理から構築され、2つの相補的な形式で解放される。 我々の実験は、明示的な前提がLean4対応の証明モデルの性能を大幅に改善していることを示している。
  論文  参考訳（メタデータ） (2026-06-08T12:57:18Z)
• LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
  研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。 新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。 このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
  論文  参考訳（メタデータ） (2026-04-02T08:22:17Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。 DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。 我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
  論文  参考訳（メタデータ） (2025-05-29T17:59:39Z)
• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。 我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。 我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
  論文  参考訳（メタデータ） (2024-11-04T05:57:40Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)

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

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