論文の概要: LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving

• arxiv url: http://arxiv.org/abs/2506.22005v1
• Date: Fri, 27 Jun 2025 08:17:18 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-30 21:12:23.131976
• Title: LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving
• Title（参考訳）: LeanConjecturer: 定理証明のための数学的推論の自動生成
• Authors: Naoto Onda, Kazumi Kasaura, Yuta Oriike, Masaya Taniguchi, Akiyoshi Sannai, Sho Sonoda,
• Abstract要約: LeanConjecturerは、Large Language Models(LLMs)を使用して、Lean 4で大学レベルの数学予想を自動的に生成するパイプラインである。 反復生成と評価により、LeanConjecturerは40のMathlibシードファイルから12,289の予想を生成し、3,776は構文的に有効で非自明であると同定された。
• 参考スコア（独自算出の注目度）: 6.220998637943786
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We introduce LeanConjecturer, a pipeline for automatically generating university-level mathematical conjectures in Lean 4 using Large Language Models (LLMs). Our hybrid approach combines rule-based context extraction with LLM-based theorem statement generation, addressing the data scarcity challenge in formal theorem proving. Through iterative generation and evaluation, LeanConjecturer produced 12,289 conjectures from 40 Mathlib seed files, with 3,776 identified as syntactically valid and non-trivial, that is, cannot be proven by \texttt{aesop} tactic. We demonstrate the utility of these generated conjectures for reinforcement learning through Group Relative Policy Optimization (GRPO), showing that targeted training on domain-specific conjectures can enhance theorem proving capabilities. Our approach generates 103.25 novel conjectures per seed file on average, providing a scalable solution for creating training data for theorem proving systems. Our system successfully verified several non-trivial theorems in topology, including properties of semi-open, alpha-open, and pre-open sets, demonstrating its potential for mathematical discovery beyond simple variations of existing results.
• Abstract（参考訳）: LeanConjecturerは、Large Language Models (LLMs)を使用して、Lean 4で大学レベルの数学予想を自動的に生成するパイプラインである。 我々のハイブリッドアプローチは規則に基づく文脈抽出とLCMに基づく定理文の生成を組み合わせ、形式的定理証明におけるデータ不足問題に対処する。 反復生成と評価を通じて、LeanConjecturerは40のMathlibシードファイルから12,289の予想を生成し、3,776は構文的に有効であり、非自明であると同定された。 グループ相対政策最適化(GRPO)による強化学習におけるこれらの予測の有効性を実証し、ドメイン固有予想に対する目標学習が定理証明能力を向上させることを示した。 提案手法は,1シードファイル当たり103.25の新たな予想を平均で生成し,定理証明システムのためのトレーニングデータを作成するためのスケーラブルなソリューションを提供する。 本システムでは, 半開集合, アルファ開集合, プレ開集合の性質を含むトポロジーにおけるいくつかの非自明な定理の検証に成功した。

関連論文リスト

• 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)
• Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions [37.10426226729792]
  本稿では,パターン駆動型推論と形式的定理証明を統合するモジュール型ニューロシンボリック手法であるLLMe-Conjecture-Prove(ECP)フレームワークを紹介する。 本稿では,様々な数学コンペティションにおける3,431の解題問題のデータセットであるConstructiveBenchを紹介する。
  論文  参考訳（メタデータ） (2025-05-24T03:52:25Z)
• 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)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)

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

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