論文の概要: A Theoretical Framework for Self-Play Theorem Proving Algorithms

• arxiv url: http://arxiv.org/abs/2606.01861v1
• Date: Mon, 01 Jun 2026 08:12:47 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-02 21:34:31.60218
• Title: A Theoretical Framework for Self-Play Theorem Proving Algorithms
• Title（参考訳）: 自己再生理論証明アルゴリズムの理論的枠組み
• Authors: Thomas Chen, Zhiyuan Li,
• Abstract要約: 定理証明のための自己表現アルゴリズムの自己改善能力を理解するための理論的枠組みを提供する。 定理の基底グラフが十分に連結であれば、導出アルゴリズムが可逆ランダムウォークに基づいて証明された定理の集合を指数関数的に成長させるのに十分であることを示す。
• 参考スコア（独自算出の注目度）: 7.702779307300836
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Self-play, a type of training algorithm that enables a model to self-improve, has recently shown promising empirical results in the context of formal theorem proving using Large Language Models (LLMs). (Dong & Ma, 2025) instantiate self-play with two cooperating agents: a prover, which proves theorems, and a conjecturer, which generates new theorems as a curriculum to the prover. In this paper, we provide a theoretical framework for understanding the self-improvement capabilities of self-play algorithms for theorem proving. First, we formalize the set of theorems as a graph, with nodes as theorems and edges between pairs of theorems with similar semantics. We introduce a set of primitive assumptions that characterize the guarantees of a trained prover and how a conjecturer can access the structure of the graph. Second, we show that if the underlying graph of theorems is well-connected, then a prover-conjecturer system, where the conjecturing algorithm is based on a reversible random walk, is sufficient to grow the set of proved theorems exponentially. Third, motivated by an issue encountered empirically by self-play algorithms, where the conjecturer tends to generate artificially complex and non-fundamental theorems, we propose a diversity measure for a training distribution of theorems generated by a conjecturer and an improved conjecturing algorithm that locally maximizes this diversity measure, by computing the diffusion similarity between neighboring theorems in the theorem graph. Finally, we describe a method to compute the diffusion similarity by using contrastive learning to embed nodes into Euclidean space and then computing the inner-product between embeddings.
• Abstract（参考訳）: モデルの自己改善を可能にする訓練アルゴリズムであるSelf-playは、最近、LLM(Large Language Models)を用いた形式的定理証明の文脈において、有望な実証結果を示した。 (Dong & Ma, 2025) は、定理を証明する証明器と、証明器のカリキュラムとして新しい定理を生成する予想器という、2つの協調エージェントで自己プレイをインスタンス化する。 本稿では,定理証明のための自己再生アルゴリズムの自己改善能力を理解するための理論的枠組みを提供する。 まず、定理の集合をグラフとして形式化し、ノードを定理とし、類似した意味論を持つ定理の対の間の縁を持つ。 我々は、訓練された証明者の保証と、予想者がグラフの構造にどのようにアクセスできるかを特徴付ける原始的な仮定のセットを紹介する。 第二に、基礎となる定理グラフが十分に連結であれば、導出アルゴリズムが可逆ランダムウォークに基づいて証明された定理の集合を指数関数的に成長させるのに十分であることを示す。 第三に、予想者が人工的に複雑で基礎的でない定理を生成する傾向にある自己プレイアルゴリズムによって経験的に遭遇した問題に動機づけられて、予想者が生成する定理のトレーニング分布に対する多様性尺度と、この多様性尺度を局所的に最大化する改良された導出アルゴリズムを、定理グラフ内の近傍の定理間の拡散類似性を計算することによって提案する。 最後に、対比学習を用いて、ユークリッド空間にノードを埋め込んだ上で、埋め込み間の内積を計算することで拡散類似性を計算する方法について述べる。

関連論文リスト

• Learning to Reason with Insight for Informal Theorem Proving [50.054221663394195]
  この研究では、非公式な定理における主要なボトルネックを洞察の欠如として証明する。 我々は,この本質的な推論スキルを育成し,LLMが洞察に富んだ推論を行うことを可能にする新しいフレームワークを提案する。 問題となる数学ベンチマークの実験では、この洞察・認識型生成戦略がベースラインを著しく上回ることを示した。
  論文  参考訳（メタデータ） (2026-04-17T17:36:21Z)
• LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving [6.220998637943786]
  LeanConjecturerは、Large Language Models(LLMs)を使用して、Lean 4で大学レベルの数学予想を自動的に生成するパイプラインである。 反復生成と評価により、LeanConjecturerは40のMathlibシードファイルから12,289の予想を生成し、3,776は構文的に有効で非自明であると同定された。
  論文  参考訳（メタデータ） (2025-06-27T08:17:18Z)
• From Axioms to Algorithms: Mechanized Proofs of the vNM Utility Theorem [0.0]
  我々は、選好完全性、推移性、連続性、独立性の古典的な公理を実践する。 我々の定式化は、宝くじに対する嗜好関係の数学的構造を捉えている。 この形式化は、経済モデリング、AIアライメント、管理決定システムにおける応用のための厳格な基盤を提供する。
  論文  参考訳（メタデータ） (2025-06-08T10:09:54Z)
• 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)
• Graph Stochastic Neural Process for Inductive Few-shot Knowledge Graph Completion [63.68647582680998]
  I-FKGC(inductive few-shot knowledge graph completion)と呼ばれる課題に焦点をあてる。 帰納的推論(inductive reasoning)の概念に着想を得て,I-FKGCを帰納的推論問題とした。 本稿では,仮説の連成分布をモデル化したニューラルプロセスに基づく仮説抽出器を提案する。 第2のモジュールでは、この仮説に基づいて、クエリセットのトリプルが抽出された仮説と一致するかどうかをテストするグラフアテンションベースの予測器を提案する。
  論文  参考訳（メタデータ） (2024-08-03T13:37:40Z)
• ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
  人間はより広範に複雑な数学的結果を探求するために新しい定理を開発することができる。 現在の生成言語モデル(LM)は、定理の自動証明において著しく改善されている。 本稿では,エージェントが価値ある(あるいは新しい)定理を自動生成できるかどうかを評価する自動定理生成ベンチマークを提案する。
  論文  参考訳（メタデータ） (2024-05-05T02:06:37Z)
• Learning to Guide a Saturation-Based Theorem Prover [9.228237801323042]
  TRAILは、ニューラルネットワーク内で証明される飽和に基づく定理の中核要素を特徴付ける、深い学習に基づく定理証明のアプローチである。 我々の知る限りでは、TRAILは最先端の伝統的な定理証明器の性能を超える最初の強化学習に基づくアプローチである。
  論文  参考訳（メタデータ） (2021-06-07T18:35:57Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。 実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
  論文  参考訳（メタデータ） (2020-02-17T16:06:02Z)

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

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