論文の概要: LeanAgent: Lifelong Learning for Formal Theorem Proving
- arxiv url: http://arxiv.org/abs/2410.06209v1
- Date: Tue, 08 Oct 2024 17:11:24 GMT
- ステータス: 翻訳完了
- システム内更新日: 2024-10-10 14:34:56.990236
- 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は継続的に一般化し、拡張可能な数学的知識を改善します。
以前は人間が証明していなかった162の定理を、23のリーンリポジトリで証明した。
- 参考スコア(独自算出の注目度): 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 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 162 theorems previously unproved by humans across 23 diverse Lean repositories, many from advanced mathematics. It performs up to 11$\times$ 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のリーンリポジトリで、以前は人間が証明していなかった162の定理の証明に成功した。
静的 LLM ベースラインよりも最大 11$\times$ の性能を発揮し、抽象代数や代数トポロジーのような領域における挑戦的な定理を証明し、基礎概念から先進的なトピックへの学習の明確な進展を示す。
さらに、LeanAgentの長寿命学習メトリクスにおける優れたパフォーマンスを分析します。
LeanAgentは、新しいタスクを学ぶことで、以前に学んだタスクのパフォーマンスが向上する、安定性と後方移行において、例外的なスコアを達成します。
これはLeanAgentの継続的一般化性と改善を強調し、その優れた定理による性能の証明を説明する。
関連論文リスト
- 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) - Mathify: Evaluating Large Language Models on Mathematical Problem Solving Tasks [34.09857430966818]
我々は,11番目と12番目の標準数学 NCERT 教科書から得られた数学データセット "MathQuest" を紹介する。
LLaMA-2, WizardMath, MAmmoTHの3つの大きな言語モデルを用いた微調整実験を行った。
この3つのモデルのうち,MAmmoTH-13Bが最も熟練したモデルとして登場し,提示された数理問題の解法において,最高レベルの能力を達成した。
論文 参考訳(メタデータ) (2024-04-19T08:45:42Z) - GSM-Plus: A Comprehensive Benchmark for Evaluating the Robustness of LLMs as Mathematical Problem Solvers [68.77382332826167]
大規模言語モデル (LLM) は、様々な数学的推論ベンチマークで顕著な性能を達成している。
1つの必須かつ頻繁な証拠は、数学の質問がわずかに変更されたとき、LLMは誤って振る舞うことができることである。
このことは, LLMの数学推論能力の頑健性を評価するために, 幅広い質問のバリエーションを試すことによるものである。
論文 参考訳(メタデータ) (2024-02-29T15:26:14Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。