論文の概要: Discovering New Theorems via LLMs with In-Context Proof Learning in Lean

• arxiv url: http://arxiv.org/abs/2509.14274v1
• Date: Tue, 16 Sep 2025 06:48:11 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-19 17:26:52.90598
• Title: Discovering New Theorems via LLMs with In-Context Proof Learning in Lean
• Title（参考訳）: リーンにおけるコンテキスト内学習によるLLMによる新しい理論の発見
• Authors: Kazumi Kasaura, Naoto Onda, Yuta Oriike, Masaya Taniguchi, Akiyoshi Sannai, Sho Sonoda,
• Abstract要約: 数理予想を自動的に生成し,それをLean 4フォーマットで証明するための導出-証明ループパイプラインを提案する。 このアプローチの特徴は、以前に生成された定理とその証明を含む文脈でさらなる予想を生成し、証明することである。 これらの定理のうちの少なくとも1つは、自然言語においても、文脈内学習なしでは LLM によって証明できない。
• 参考スコア（独自算出の注目度）: 6.097030695272925
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large Language Models have demonstrated significant promise in formal theorem proving. However, previous works mainly focus on solving existing problems. In this paper, we focus on the ability of LLMs to find novel theorems. We propose Conjecturing-Proving Loop pipeline for automatically generating mathematical conjectures and proving them in Lean 4 format. A feature of our approach is that we generate and prove further conjectures with context including previously generated theorems and their proofs, which enables the generation of more difficult proofs by in-context learning of proof strategies without changing parameters of LLMs. We demonstrated that our framework rediscovered theorems with verification, which were published in past mathematical papers and have not yet formalized. Moreover, at least one of these theorems could not be proved by the LLM without in-context learning, even in natural language, which means that in-context learning was effective for neural theorem proving. The source code is available at https://github.com/auto-res/ConjecturingProvingLoop.
• Abstract（参考訳）: 大規模言語モデルは形式的定理の証明において大きな可能性を証明している。 しかし、これまでの研究は主に既存の問題を解決することに焦点を当てていた。 本稿では, LLMの新たな定理の発見に焦点をあてる。 数理予想を自動的に生成し,それをLean 4フォーマットで証明するための導出-証明ループパイプラインを提案する。 提案手法の特徴は, LLM のパラメータを変化させることなく, 証明戦略の文脈内学習により, より難しい証明を生成できるような, 先に生成した定理とその証明を含む, 文脈によるさらなる予想の生成と証明を行うことである。 我々は、過去の数学的論文で発表され、まだ定式化されていない検証を伴う定理を再発見されたことを実証した。 さらに、これらの定理のうちの少なくとも1つは、自然言語においても、文脈内学習がなければLLMでは証明できないため、文脈内学習はニューラルネットワークの証明に有効であった。 ソースコードはhttps://github.com/auto-res/ConjecturingProvingLoopで公開されている。

関連論文リスト

• 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)
• 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)
• One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs [75.95179490687018]
  証明生成のための数学的大規模言語モデルを活用することは、LLM研究の基本的なトピックである。 現状のLCMが証明できる能力は、学習中に関連する証明プロセスに遭遇したかどうかに大きく依存していると論じる。 人間の数学教育で一般的に用いられる「反例による防御」の教育的手法に触発されて,我々の研究は,反例を通して数学的推論と証明を行うLLMの能力を高めることを目的としている。
  論文  参考訳（メタデータ） (2025-02-12T02:01:10Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• REFACTOR: Learning to Extract Theorems from Proofs [29.44286369265644]
  我々は、REFACTORが、人間が証明を書くのに使用する定理の19.6%を抽出できることを示した。 新たに抽出された定理により,既存のMetaMathデータベースが構築可能であることを示す。 また、新理論データセットでトレーニングされた証明者が、より多くのテスト定理を証明し、最先端のベースラインを上回ることを実証する。
  論文  参考訳（メタデータ） (2024-02-26T21:21:30Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。 実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
  論文  参考訳（メタデータ） (2020-02-17T16:06:02Z)

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

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