論文の概要: LeanAgent: Lifelong Learning for Formal Theorem Proving

• arxiv url: http://arxiv.org/abs/2410.06209v7
• Date: Mon, 25 Nov 2024 02:39:03 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-11-26 14:16:20.477428
• Title: LeanAgent: Lifelong Learning for Formal Theorem Proving
• Title（参考訳）: LeanAgent: 形式理論の証明のための生涯学習
• Authors: Adarsh Kumarappan, Mo Tiwari, Peiyang Song, Robert Joseph George, Chaowei Xiao, Anima Anandkumar,
• Abstract要約: フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。 LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。 以前、23のリーンリポジトリで人間が公式に証明していなかった155の定理の証明に成功した。
• 参考スコア（独自算出の注目度）: 85.39415834798385
• License:
• Abstract: Large Language Models (LLMs) have been successful in mathematical reasoning tasks such as formal theorem proving when integrated with interactive proof assistants like Lean. Existing approaches involve training or fine-tuning an LLM on a specific dataset to perform well on particular domains, such as undergraduate-level mathematics. These methods struggle with generalizability to advanced mathematics. A fundamental limitation is that these approaches operate on static domains, failing to capture how mathematicians often work across multiple domains and projects simultaneously or cyclically. We present LeanAgent, a novel lifelong learning framework for formal theorem proving that continuously generalizes to and improves on ever-expanding mathematical knowledge without forgetting previously learned knowledge. LeanAgent introduces several key innovations, including a curriculum learning strategy that optimizes the learning trajectory in terms of mathematical difficulty, a dynamic database for efficient management of evolving mathematical knowledge, and progressive training to balance stability and plasticity. LeanAgent successfully proves 155 theorems previously unproved formally by humans across 23 diverse Lean repositories, many from advanced mathematics. It performs significantly better than the static LLM baseline, proving challenging theorems in domains like abstract algebra and algebraic topology while showcasing a clear progression of learning from basic concepts to advanced topics. In addition, we analyze LeanAgent's superior performance on key lifelong learning metrics. LeanAgent achieves exceptional scores in stability and backward transfer, where learning new tasks improves performance on previously learned tasks. This emphasizes LeanAgent's continuous generalizability and improvement, explaining its superior theorem-proving performance.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、リーンのようなインタラクティブな証明アシスタントと統合された際の形式的定理証明のような数学的推論タスクで成功している。 既存のアプローチでは、学部レベルの数学のような特定の領域でうまく機能するために、特定のデータセット上でLLMを訓練または微調整する。 これらの手法は高度な数学への一般化性に苦しむ。 基本的な制限は、これらのアプローチが静的なドメイン上で動作し、数学者が複数のドメインやプロジェクトを同時に、あるいは循環的にどのように機能するかを捉えることができないことである。 これまでに学習された知識を忘れることなく、絶え間なく拡張された数学的知識を継続的に一般化し、改善するフォーマルな定理証明のための、新しい生涯学習フレームワークであるLeanAgentを紹介する。 LeanAgentは、数学的難易度の観点から学習軌道を最適化するカリキュラム学習戦略、進化する数学的知識の効率的な管理のための動的データベース、安定性と可塑性のバランスをとるための進歩的なトレーニングなど、いくつかの重要なイノベーションを紹介している。 LeanAgentは、23のリーンレポジトリに対して、以前は人間が公式に証明していなかった155の定理の証明に成功した。 静的 LLM ベースラインよりもはるかに優れた性能を示し、抽象代数や代数トポロジーのような領域における挑戦的な定理を証明し、基礎概念から高度なトピックへの学習の明確な進歩を示している。 さらに、LeanAgentの長寿命学習メトリクスにおける優れたパフォーマンスを分析します。 LeanAgentは、新しいタスクを学ぶことで、以前に学んだタスクのパフォーマンスが向上する、安定性と後方移行において、例外的なスコアを達成します。 これはLeanAgentの継続的一般化性と改善を強調し、その優れた定理を提供するパフォーマンスを説明する。

関連論文リスト

• MathFimer: Enhancing Mathematical Reasoning by Expanding Reasoning Steps through Fill-in-the-Middle Task [49.355810887265925]
  数学的推論ステップ拡張のための新しいフレームワークであるMathFimerを紹介する。 我々は、慎重にキュレートしたNuminaMath-FIMデータセットに基づいて、特殊モデルMathFimer-7Bを開発した。 次に、これらのモデルを適用して、解鎖に詳細な中間ステップを挿入することで、既存の数学的推論データセットを強化する。
  論文  参考訳（メタデータ） (2025-02-17T11:22:24Z)
• One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs [57.48325300739872]
  証明生成のための数学的大規模言語モデルを活用することは、LLM研究の基本的なトピックである。 現状のLCMが証明できる能力は、学習中に関連する証明プロセスに遭遇したかどうかに大きく依存していると論じる。 人間の数学教育で一般的に用いられる「反例による防御」の教育的手法に触発されて,我々の研究は,反例を通して数学的推論と証明を行うLLMの能力を高めることを目的としている。
  論文  参考訳（メタデータ） (2025-02-12T02:01:10Z)
• LemmaHead: RAG Assisted Proof Generation Using Large Language Models [0.0]
  我々は、関連する数学的文脈でモデルにクエリを補足する知識ベースであるLemmaHeadを開発した。 数学的推論におけるモデルの性能を測定するため、我々のテストパラダイムは自動定理証明の課題に焦点を当てている。
  論文  参考訳（メタデータ） (2025-01-27T05:46:06Z)
• Large Language Models for Mathematical Analysis [3.7325315394927023]
  この研究は、数学的推論における重要なギャップに対処し、信頼できるAIの進歩に寄与する。 DEMI-MathAnalysisデータセットを開発した。 また,LLMの問題解決能力を高めるためのガイドフレームワークも設計した。
  論文  参考訳（メタデータ） (2024-12-28T20:37:55Z)
• Formal Mathematical Reasoning: A New Frontier in AI [60.26950681543385]
  我々は公式な数学的推論を提唱し、AI4Mathを次のレベルに進めるには不可欠であると主張している。 既存の進捗を要約し、オープンな課題について議論し、将来の成功を測るための重要なマイルストーンを想定します。
  論文  参考訳（メタデータ） (2024-12-20T17:19:24Z)
• MathLearner: A Large Language Model Agent Framework for Learning to Solve Mathematical Problems [0.936726079405677]
  本稿では,帰納的推論に基づく数学的問題を解くためのエージェントフレームワークを提案する。 学習情報の一般化に関する人間の学習過程をエミュレートすることにより、この枠組みは数学的推論プロセスにおいて優れた性能を発揮する。 我々のモデルは個人化された学習支援として利用でき、教育資源の不平等を軽減できる。
  論文  参考訳（メタデータ） (2024-08-03T13:28:19Z)
• MathBench: Evaluating the Theory and Application Proficiency of LLMs with a Hierarchical Mathematics Benchmark [82.64129627675123]
  MathBenchは、大規模言語モデルの数学的能力を厳格に評価する新しいベンチマークである。 MathBenchは幅広い数学の分野にまたがっており、理論的な理解と実践的な問題解決のスキルの両方を詳細に評価している。
  論文  参考訳（メタデータ） (2024-05-20T17:52:29Z)
• InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning [98.53491178426492]
  InternLM2から事前学習を継続するILMs InternLM-Mathをオープンソースとして公開する。 我々は、連鎖推論、報酬モデリング、形式推論、データ拡張、コードインタプリタを、統一されたSeq2seqフォーマットで統一する。 我々の事前学習モデルは、微調整なしでMiniF2Fテストセットで30.3を達成する。
  論文  参考訳（メタデータ） (2024-02-09T11:22:08Z)
• math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories [10.416375584563728]
  本研究では,大規模言語モデル(LLM)の高度な数学的概念の定式化への適用性について検討する。 我々は、研究論文から数学的定理を抽出し、形式化する、Emphmath-PVSと呼ばれる自動過程を構想する。
  論文  参考訳（メタデータ） (2023-10-25T23:54:04Z)

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

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