論文の概要: Self-Supervised Theorem Discovery in a Formal Axiomatic System

• arxiv url: http://arxiv.org/abs/2606.28747v1
• Date: Sat, 27 Jun 2026 05:55:18 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-30 18:07:15.674942
• Title: Self-Supervised Theorem Discovery in a Formal Axiomatic System
• Title（参考訳）: 形式的公理系における自己教師付き理論発見
• Authors: Kazuki Ota, Takayuki Osa, Tatsuya Harada,
• Abstract要約: エージェントが、そのような先入観のない有用な定理を自律的に発見できるかどうかを考察する。 本稿では,証明探索と有用な定理抽出を交互に行う自己教師付き定理発見アルゴリズムを提案する。 本結果は,人為的な定理ライブラリに頼らずに,有用な定理が証明探索から現れることを示すものである。
• 参考スコア（独自算出の注目度）: 44.603295025494674
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent artificial intelligence (AI) systems have shown remarkable progress in mathematical reasoning. Many existing approaches, including large language models (LLMs), draw on human prior knowledge in the form of mathematical text, code, or theorem libraries. Although these approaches are highly effective in practice, it remains an open question whether an agent can autonomously discover useful theorems without such human priors. We study this question in a formal axiomatic system by developing an agent that starts from axioms and inference rules alone and gradually grows a library of useful theorems. Concretely, we propose a self-supervised theorem-discovery algorithm that alternates between proof search and useful-theorem extraction, building a theorem library whose entries are reused as lemmas for subsequent proof search. Experiments show that the agent discovers tens of thousands of theorems and finds proofs for human-written benchmark problems, suggesting that its discoveries include theorems meaningful from a human mathematical perspective. Furthermore, the discovered theorems improve LLM proof performance when provided as prompt lemmas, indicating that they can serve as external knowledge for LLM reasoning. Our results provide evidence that useful theorems can emerge from proof search without relying on human-provided theorem libraries. More broadly, they suggest a path toward self-evolving AI systems for mathematics whose discoveries remain formally verifiable.
• Abstract（参考訳）: 最近の人工知能(AI)システムは、数学的推論において顕著な進歩を見せている。 大規模言語モデル(LLM)を含む多くの既存のアプローチは、数学的テキスト、コード、あるいは定理ライブラリの形式で人間の事前知識に基づいている。 これらの手法は実際は極めて効果的であるが、エージェントがそのような先入観のない有用な定理を自律的に発見できるかどうかには疑問が残る。 我々は、公理と推論規則のみから始まり、有用な定理のライブラリーを徐々に成長させるエージェントを開発することによって、この問題を形式的公理系で研究する。 具体的には,証明探索と有用な定理抽出を交互に行う自己教師付き定理探索アルゴリズムを提案する。 実験により、エージェントは数万の定理を発見し、人間によって書かれたベンチマーク問題の証明を見つけ、その発見には人間の数学的観点から意味のある定理が含まれることを示唆している。 さらに、発見された定理は、プロンプト補題として提供されるときのLLM証明性能を改善し、LLM推論の外部知識として機能することを示す。 本結果は,人為的な定理ライブラリに頼らずに,有用な定理が証明探索から現れることを示すものである。 より広くは、発見が正式に検証されている数学のための自己進化型AIシステムへの道のりを示唆している。

関連論文リスト

• A Theoretical Framework for Self-Play Theorem Proving Algorithms [7.702779307300836]
  定理証明のための自己表現アルゴリズムの自己改善能力を理解するための理論的枠組みを提供する。 定理の基底グラフが十分に連結であれば、導出アルゴリズムが可逆ランダムウォークに基づいて証明された定理の集合を指数関数的に成長させるのに十分であることを示す。
  論文  参考訳（メタデータ） (2026-06-01T08:12:47Z)
• Discovering New Theorems via LLMs with In-Context Proof Learning in Lean [6.097030695272925]
  数理予想を自動的に生成し,それをLean 4フォーマットで証明するための導出-証明ループパイプラインを提案する。 このアプローチの特徴は、以前に生成された定理とその証明を含む文脈でさらなる予想を生成し、証明することである。 これらの定理のうちの少なくとも1つは、自然言語においても、文脈内学習なしでは LLM によって証明できない。
  論文  参考訳（メタデータ） (2025-09-16T06:48:11Z)
• 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)
• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。 LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。 これは23のリーンリポジトリにわたる155の定理の正式な証明を生成する。
  論文  参考訳（メタデータ） (2024-10-08T17:11:24Z)
• ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
  人間はより広範に複雑な数学的結果を探求するために新しい定理を開発することができる。 現在の生成言語モデル(LM)は、定理の自動証明において著しく改善されている。 本稿では,エージェントが価値ある(あるいは新しい)定理を自動生成できるかどうかを評価する自動定理生成ベンチマークを提案する。
  論文  参考訳（メタデータ） (2024-05-05T02:06:37Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。 実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
  論文  参考訳（メタデータ） (2020-02-17T16:06:02Z)

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

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