論文の概要: LEGO-Prover: Neural Theorem Proving with Growing Libraries
- arxiv url: http://arxiv.org/abs/2310.00656v2
- Date: Thu, 12 Oct 2023 03:01:27 GMT
- ステータス: 処理完了
- システム内更新日: 2023-10-14 14:42:24.978699
- Title: LEGO-Prover: Neural Theorem Proving with Growing Libraries
- Title（参考訳）: LEGO-Prover: ライブラリを成長させるニューラルネットワーク理論
- Authors: Huajian Xin, Haiming Wang, Chuanyang Zheng, Lin Li, Zhengying Liu,
Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo
Li, Xiaodan Liang, Heng Liao
- Abstract要約: LEGO-Prover では,証明された補題を含むスキルライブラリを,定理証明に使用される LLM の能力を高めるためのスキルとして活用する。
LEGO-Proverは、証明をモジュール的に構築することにより、ライブラリから取得した既存のスキルを活用し、証明プロセス中に新しいスキルを作成することができる。
我々のアブレーション研究は、これらの新たなスキルが定理の証明に役立つことを示唆し、47.1%から50.4%に改善した。
- 参考スコア（独自算出の注目度）: 86.1191481712352
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Despite the success of large language models (LLMs), the task of theorem
proving still remains one of the hardest reasoning tasks that is far from being
fully solved. Prior methods using language models have demonstrated promising
results, but they still struggle to prove even middle school level theorems.
One common limitation of these methods is that they assume a fixed theorem
library during the whole theorem proving process. However, as we all know,
creating new useful theorems or even new theories is not only helpful but
crucial and necessary for advancing mathematics and proving harder and deeper
results. In this work, we present LEGO-Prover, which employs a growing skill
library containing verified lemmas as skills to augment the capability of LLMs
used in theorem proving. By constructing the proof modularly, LEGO-Prover
enables LLMs to utilize existing skills retrieved from the library and to
create new skills during the proving process. These skills are further evolved
(by prompting an LLM) to enrich the library on another scale. Modular and
reusable skills are constantly added to the library to enable tackling
increasingly intricate mathematical problems. Moreover, the learned library
further bridges the gap between human proofs and formal proofs by making it
easier to impute missing steps. LEGO-Prover advances the state-of-the-art pass
rate on miniF2F-valid (48.0% to 57.0%) and miniF2F-test (45.5% to 47.1%).
During the proving process, LEGO-Prover also manages to generate over 20,000
skills (theorems/lemmas) and adds them to the growing library. Our ablation
study indicates that these newly added skills are indeed helpful for proving
theorems, resulting in an improvement from a success rate of 47.1% to 50.4%. We
also release our code and all the generated skills.
- Abstract（参考訳）: 大規模言語モデル(llm)の成功にもかかわらず、定理証明のタスクは、まだ完全には解決されていない最も難しい推論タスクの1つである。
言語モデルを用いた以前の手法は有望な結果を示しているが、中学レベルの定理を証明するのに苦労している。
これらの方法の一般的な制限の1つは、定理証明過程全体において固定定理ライブラリを仮定することである。
しかし、誰もが知っているように、新しい有用な定理や新しい理論を作ることは、数学を進歩させ、より強くより深い結果を証明するのに有用であるだけでなく、必要不可欠である。
本稿では,証明された補題を含むスキルライブラリを,定理証明に使用されるLLMの能力を高めるためのスキルとして活用するLEGO-Proverを提案する。
LEGO-Proverは、証明をモジュール的に構築することにより、ライブラリから取得した既存のスキルを活用し、証明プロセス中に新しいスキルを作成することができる。
これらのスキルはさらに進化し(llmを促すことによって)、別のスケールでライブラリを豊かにします。
モジュール性と再利用可能なスキルがライブラリに絶えず追加され、複雑な数学的問題に取り組むことができる。
さらに、学習ライブラリは、人間の証明と形式的証明のギャップをさらに橋渡しし、欠落したステップを挿入しやすくする。
LEGO-Proverは、MiniF2F-valid(48.0%から57.0%)とMiniF2F-test(45.5%から47.1%)の最先端パスレートを推し進めている。
証明プロセスの間、lego-proverは20,000以上のスキル(理論/補題)を生成し、成長中のライブラリに追加する。
我々のアブレーション研究は、これらの新たなスキルが定理の証明に役立つことを示唆し、47.1%から50.4%に改善した。
コードと生成されたすべてのスキルもリリースします。
関連論文リスト
- Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。
我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。
我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
論文 参考訳（メタデータ） (2024-11-04T05:57:40Z) - LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。
LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。
以前、23のリーンリポジトリで人間が公式に証明していなかった155の定理の証明に成功した。
論文 参考訳（メタデータ） (2024-10-08T17:11:24Z) - SubgoalXL: Subgoal-based Expert Learning for Theorem Proving [37.115856591703974]
SubgoalXLは、正規の定理証明を強化するために、専門家の学習とサブゴールベースの証明を相乗化する新しいアプローチである。
SubgoalXLは、標準のminiF2Fデータセット上で、Isabelleで56.1%の最先端パフォーマンスを実現する。
論文 参考訳（メタデータ） (2024-08-20T20:10:53Z) - TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts [26.98890165420689]
TheoremLlamaは、汎用的なLean4エキスパートをトレーニングするエンドツーエンドフレームワークである。
我々のフレームワークは,MiniF2F-ValidデータセットとTestデータセットでそれぞれ36.48%,33.61%の累積精度を達成した。
論文 参考訳（メタデータ） (2024-07-03T15:36:18Z) - ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
人間はより広範に複雑な数学的結果を探求するために新しい定理を開発することができる。
現在の生成言語モデル(LM)は、定理の自動証明において著しく改善されている。
本稿では,エージェントが価値ある(あるいは新しい)定理を自動生成できるかどうかを評価する自動定理生成ベンチマークを提案する。
論文 参考訳（メタデータ） (2024-05-05T02:06:37Z) - Towards Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
大規模な言語モデルでリーン推論を実行するためのフレームワークであるLean Copilotを紹介します。
証明手順を提案し、中間的な証明目標を完了し、関連する前提を選択するためのツールを構築します。
実験により, 提案手法の有効性を実証し, 提案手法の有効性を検証した。
論文 参考訳（メタデータ） (2024-04-18T22:54:08Z) - LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。
既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。
本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。
本研究では,LLM ベースの証明器 ReProver を開発した。
論文 参考訳（メタデータ） (2023-06-27T17:05:32Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳（メタデータ） (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。