Fugu-MT 論文翻訳(概要): LeanAgent: Lifelong Learning for Formal Theorem Proving

論文の概要: 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の継続的一般化性と改善を強調し、その優れた定理を提供するパフォーマンスを説明する。

関連論文リスト

Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4 [0.0]
本稿では,Large Language Models (LLMs) を用いて,形式的証明ステップと完全形式的証明を生成する。目標は、AIをどのように活用して数学的形式化プロセスを支援し、パフォーマンスを向上させるかを決定することである。
論文参考訳（メタデータ） (2024-09-09T18:21:28Z)
MathLearner: A Large Language Model Agent Framework for Learning to Solve Mathematical Problems [0.936726079405677]
本稿では,帰納的推論に基づく数学的問題を解くためのエージェントフレームワークを提案する。学習情報の一般化に関する人間の学習過程をエミュレートすることにより、この枠組みは数学的推論プロセスにおいて優れた性能を発揮する。我々のモデルは個人化された学習支援として利用でき、教育資源の不平等を軽減できる。
論文参考訳（メタデータ） (2024-08-03T13:28:19Z)
Learning Beyond Pattern Matching? Assaying Mathematical Understanding in LLMs [58.09253149867228]
本稿では,LLMのドメイン知識を,問題解決に必要な数学的スキルの理解を通じて評価する。汎用科学アシスタントとしてLLMを用いることで, LLMの確率分布の変化を評価するためにtextitNTKEvalを提案する。系統的な分析では、文脈内学習中にドメイン理解の証拠が見つかる。ある命令チューニングは、異なるデータでのトレーニングに関係なく、同様のパフォーマンス変化をもたらし、異なるスキルに対するドメイン理解の欠如を示唆している。
論文参考訳（メタデータ） (2024-05-24T12:04:54Z)
MathBench: Evaluating the Theory and Application Proficiency of LLMs with a Hierarchical Mathematics Benchmark [82.64129627675123]
MathBenchは、大規模言語モデルの数学的能力を厳格に評価する新しいベンチマークである。 MathBenchは幅広い数学の分野にまたがっており、理論的な理解と実践的な問題解決のスキルの両方を詳細に評価している。
論文参考訳（メタデータ） (2024-05-20T17:52:29Z)
AlphaMath Almost Zero: Process Supervision without Process [6.318873143509028]
我々はモンテカルロ木探索(MCTS)を活用することによってプロセスアノテーションの必要性を回避できる革新的なフレームワークAlphaMathを提案する。このフレームワークは、その数学的推論を自律的に強化する、よく訓練されたLLMの可能性を解き放つことに焦点を当てている。ドメイン内データセットとドメイン外データセットの両方の実験結果から,GPT-4や人手によるプロセス監視がなくても,AlphaMathフレームワークは従来の最先端手法と同等あるいは優れた結果が得られることが示された。
論文参考訳（メタデータ） (2024-05-06T15:20:30Z)
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)
A Survey of Deep Learning for Mathematical Reasoning [71.88150173381153]
我々は過去10年間の数学的推論とディープラーニングの交差点における重要なタスク、データセット、方法についてレビューする。大規模ニューラルネットワークモデルの最近の進歩は、新しいベンチマークと、数学的推論にディープラーニングを使用する機会を開放している。
論文参考訳（メタデータ） (2022-12-20T18:46:16Z)
JiuZhang: A Chinese Pre-trained Language Model for Mathematical Problem Understanding [74.12405417718054]
本稿では,中国初の数学的事前学習言語モデル(PLM)を提示することにより,機械の数学的知性向上を目指す。他の標準のNLPタスクとは異なり、数学的テキストは問題文に数学的用語、記号、公式を含むため理解が難しい。基礎課程と上級課程の両方からなる数学PLMの学習を改善するための新しいカリキュラム事前学習手法を設計する。
論文参考訳（メタデータ） (2022-06-13T17:03:52Z)

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

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