論文の概要: LEGO-Prover: Neural Theorem Proving with Growing Libraries
- arxiv url: http://arxiv.org/abs/2310.00656v3
- Date: Fri, 27 Oct 2023 12:44:32 GMT
- ステータス: 処理完了
- システム内更新日: 2023-10-30 16:36:28.591264
- Title: LEGO-Prover: Neural Theorem Proving with Growing Libraries
- Title(参考訳): LEGO-Prover: ライブラリを成長させるニューラルネットワーク理論
- Authors: Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu,
Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo
Li, Heng Liao, Xiaodan Liang
- 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%に改善した。
コードと生成されたすべてのスキルもリリースします。
関連論文リスト
- REFACTOR: Learning to Extract Theorems from Proofs [29.44286369265644]
我々は、REFACTORが、人間が証明を書くのに使用する定理の19.6%を抽出できることを示した。
新たに抽出された定理により,既存のMetaMathデータベースが構築可能であることを示す。
また、新理論データセットでトレーニングされた証明者が、より多くのテスト定理を証明し、最先端のベースラインを上回ることを実証する。
論文 参考訳(メタデータ) (2024-02-26T21:21:30Z) - Enhancing Neural Theorem Proving through Data Augmentation and Dynamic
Sampling Method [1.8130068086063336]
本稿では,定理証明のための新しい動的サンプリング手法であるDS-Proverを紹介する。
単純化と書き直しの戦術を複数の前提で1つの前提で戦術に分解することで、トレーニングデータセットを強化します。
ProofNetデータセットでは14.2%の最先端パフォーマンス(Pass@1)、MiniF2Fでは29.8%のパフォーマンスを実現しています。
論文 参考訳(メタデータ) (2023-12-20T09:55:21Z) - ML-Bench: Large Language Models Leverage Open-source Libraries for
Machine Learning Tasks [75.12666425091702]
大規模な言語モデルは、コード生成ベンチマークで有望なパフォーマンスを示している。
この研究は、LLMがオープンソースのライブラリを使用して機械学習タスクを終了する、新たな評価設定を提案することを目的としている。
論文 参考訳(メタデータ) (2023-11-16T12:03:21Z) - Are LLMs Rigorous Logical Reasoner? Empowering Natural Language Proof
Generation with Contrastive Stepwise Decoding [11.385103498440932]
本稿では,論理的推論のためのモデルの能力を高めるために,負の推論経路を用いることにより,ステップワイズな証明生成に対照的な復号を導入する。
EntailmentBankの実験は、言語モデルの計画能力を実証する上で、我々の手法の成功を裏付けている。
論文 参考訳(メタデータ) (2023-11-12T05:12:49Z) - Democratizing Reasoning Ability: Tailored Learning from Large Language
Model [97.4921006089966]
そこで我々は,そのような推論能力をより小さなLMに蒸留する,適切な学習手法を提案する。
対話型多ラウンド学習パラダイムを構築することにより,理科教員としてのLLMの可能性を活用する。
より小さなLMの推論可能性を活用するために,学生が自作ミスから学習する動機付けを目的とした自己回帰学習を提案する。
論文 参考訳(メタデータ) (2023-10-20T07:50:10Z) - LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。
既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。
本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。
本研究では,LLM ベースの証明器 ReProver を開発した。
論文 参考訳(メタデータ) (2023-06-27T17:05:32Z) - TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
GPT-4のこれらの問題を解決する能力は非並列であり、Program-of-Thoughts Promptingの精度は51%である。
TheoremQAは、350の定理をカバーする800の高品質な質問を含むドメインの専門家によってキュレートされる。
論文 参考訳(メタデータ) (2023-05-21T17:51:35Z) - Learning Equational Theorem Proving [2.8784416089703955]
深層強化学習環境下で証明された方程式定理を学習するための最短解イミテーション学習(3SIL)を開発した。
自己学習されたモデルは、準群論におけるトップオープン予想の1つによって生じる問題を証明する上で、最先端のパフォーマンスを達成する。
論文 参考訳(メタデータ) (2021-02-10T16:33:07Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳(メタデータ) (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。