論文の概要: TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics

• arxiv url: http://arxiv.org/abs/2606.09450v1
• Date: Mon, 08 Jun 2026 12:57:18 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-09 14:42:07.075926
• Title: TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics
• Title（参考訳）: TheoremBench: 形式数学の定理証明におけるLLMの評価
• Authors: QuocViet Pham, Elvir Karimov, Andrey Galichin, Ivan Oseledets,
• Abstract要約: TheoremBenchは、コンテストの設定を超えて定理の証明者を評価するために設計されたLean4ベンチマークである。 このベンチマークは100近い古典的定理から構築され、2つの相補的な形式で解放される。 我々の実験は、明示的な前提がLean4対応の証明モデルの性能を大幅に改善していることを示している。
• 参考スコア（独自算出の注目度）: 6.168228844241134
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: LLMs have recently achieved strong results on formal proving benchmarks. However, existing evaluations remain heavily concentrated on competition-style problems and often fail to capture how models behave on longer, more dependency-rich mathematical developments. We introduce TheoremBench, a Lean4 benchmark designed to evaluate theorem provers beyond contest settings. The benchmark is built from nearly one hundred classical theorems and is released in two complementary forms: a plain main version containing one target theorem per instance, and a premised version that expands each theorem into a structured family of related proving tasks consisting of the main theorem together with automatically extracted supporting subtheorems. This design enables evaluation of not only whether the final theorem was proved from scratch, but also of partial progress through the internal proof structure of a theorem. Our experiments show that explicit premises substantially improve performance for Lean4-capable prover models. To provide a comprehensive evaluation, we introduce theorem-level coverage and token-efficiency metrics that expose qualitative differences in proof behavior. The results show that current provers remain strongly biased toward easy subtheorems and often solve theorems through long and inefficient tactic traces rather than compact proof plans. TheoremBench therefore provides a more fine-grained view of formal reasoning ability and highlights the importance of structural benchmark design for evaluating Lean4 theorem provers.
• Abstract（参考訳）: LLMは、最近、公式な証明ベンチマークで大きな成果を上げている。 しかし、既存の評価は競争スタイルの問題に大きく集中しており、モデルがより長く、より依存に富んだ数学的発展に対してどのように振る舞うかを捉えるのに失敗することが多い。 TheoremBenchは、コンテストの設定を超えて定理の証明者を評価するために設計されたLean4ベンチマークである。 ベンチマークは100近い古典的定理から構築され、1インスタンス当たりの1つの目標定理を含むプレーンなメインバージョンと、各定理を主定理からなる関連する証明タスクの構造化されたファミリに拡張し、自動抽出された支持部分定理の2つの補完形式でリリースされている。 この設計により、最終的な定理がスクラッチから証明されたかどうかだけでなく、定理の内部証明構造を通じて部分的に進行したかどうかを評価することができる。 我々の実験は、明示的な前提がLean4対応の証明モデルの性能を大幅に改善していることを示している。 包括的評価として,証明行動の質的差異を明らかにするための定理レベルのカバレッジとトークン効率指標を導入する。 結果は、現在の証明者は簡単な部分定理に対して強く偏りを保ち、コンパクトな証明計画よりも長く非効率な戦術的トレースを通じてしばしば定理を解くことを示した。 したがってTheoremBench氏は、フォーマルな推論能力のよりきめ細かいビューを提供し、Lean4定理の証明者を評価するための構造的ベンチマーク設計の重要性を強調している。

関連論文リスト

• A Theoretical Framework for Self-Play Theorem Proving Algorithms [7.702779307300836]
  定理証明のための自己表現アルゴリズムの自己改善能力を理解するための理論的枠組みを提供する。 定理の基底グラフが十分に連結であれば、導出アルゴリズムが可逆ランダムウォークに基づいて証明された定理の集合を指数関数的に成長させるのに十分であることを示す。
  論文  参考訳（メタデータ） (2026-06-01T08:12:47Z)
• Benchmarking Testing in Automated Theorem Proving [39.65133452374143]
  T は形式定理の意味的正しさを評価する枠組みである。 5つの実世界のLean 4リポジトリからベンチマークを構築します。 実験により、最先端のモデルでは高いコンパイル成功を達成できるが、セマンティック・メトリックでは著しく性能が低下することが示された。
  論文  参考訳（メタデータ） (2026-04-26T13:24:20Z)
• 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)
• 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)
• INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving [36.194330645092634]
  本稿では,エージェントの一般化能力をテストするために,INequality Theorem Proving benchmarkを提案する。 Int は定理と証明を生成する手順に基づいており、この手順のノブは6つの異なる種類の一般化を測ることができる。 次に,モンテカルロ木探索(MCTS)で拡張したエージェントを試験時に評価し,MCTSが新たな定理を証明できることを示す。
  論文  参考訳（メタデータ） (2020-07-06T17:55:33Z)

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

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