Fugu-MT 論文翻訳(概要): Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically

論文の概要: Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically

arxiv url: http://arxiv.org/abs/2411.01829v1
Date: Mon, 04 Nov 2024 05:57:40 GMT
ステータス: 翻訳完了
システム内更新日: 2024-11-05 14:47:00.413337
Title: Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically
Title（参考訳）: LLMを階層的に分解する形式的定理証明
Authors: Kefan Dong, Arvind Mahankali, Tengyu Ma,
Abstract要約: 本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
参考スコア（独自算出の注目度）: 29.908878832382523
License:
Abstract: Mathematical theorem proving is an important testbed for large language models' deep and abstract reasoning capability. This paper focuses on improving LLMs' ability to write proofs in formal languages that permit automated proof verification/evaluation. Most previous results provide human-written lemmas to the theorem prover, which is an arguably oversimplified setting that does not sufficiently test the provers' planning and decomposition capabilities. Instead, we work in a more natural setup where the lemmas that are directly relevant to the theorem are not given to the theorem prover at test time. We design an RL-based training algorithm that encourages the model to decompose a theorem into lemmas, prove the lemmas, and then prove the theorem by using the lemmas. Our reward mechanism is inspired by how mathematicians train themselves: even if a theorem is too challenging to be proved by the current model, a positive reward is still given to the model for any correct and novel lemmas that are proposed and proved in this process. During training, our model proposes and proves lemmas that are not in the training dataset. In fact, these newly-proposed correct lemmas consist of 37.7% of the training replay buffer when we train on the dataset extracted from Archive of Formal Proofs (AFP). The model trained by our RL algorithm outperforms that trained by supervised finetuning, improving the pass rate from 40.8% to 45.5% on AFP test set, and from 36.5% to 39.5% on an out-of-distribution test set.
Abstract（参考訳）: 数学的定理の証明は、大言語モデルの深く抽象的な推論能力にとって重要なテストベッドである。本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。これまでのほとんどの結果は、証明者に対して人間による補題を提供しており、これは証明者の計画と分解能力を十分にテストしない、明らかに単純化された設定である。代わりに、定理に直接関係する補題がテスト時に定理証明者に与えられないより自然な設定で作業する。我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。定理が現在のモデルによって証明されるには難しすぎるとしても、このプロセスで提案され、証明される任意の正新な補題に対して、肯定的な報酬がモデルに与えられる。トレーニング中に、トレーニングデータセットにないレムマを提案し、証明する。実際、これら新たに提案された正しい補題は、Archive of Formal Proofs (AFP)から抽出されたデータセットでトレーニングする際のトレーニング再生バッファの37.7%で構成されている。我々のRLアルゴリズムによって訓練されたモデルは、教師による微調整によって訓練されたモデルよりも優れており、AFPテストセットではパスレートが40.8%から45.5%、アウト・オブ・ディストリビューションテストセットでは36.5%から39.5%に改善されている。

関連論文リスト

Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文参考訳（メタデータ） (2024-10-21T08:04:21Z)
Proof Automation with Large Language Models [6.587933406842906]
大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
論文参考訳（メタデータ） (2024-09-22T00:19:27Z)
Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文参考訳（メタデータ） (2024-07-14T01:43:07Z)
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。この合成データセットでDeepSeekMath 7Bモデルを微調整します。我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
論文参考訳（メタデータ） (2024-05-23T09:03:42Z)
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving [41.23045212775232]
探索経路の失敗から学習する訓練モデルの利点を実証する。既存のオープンソース定理証明データセットにそのような試行錯誤データが欠如しているにもかかわらず、直観論的命題論理定理のデータセットをキュレートする。比較的短いトライアル・アンド・エラー情報(TrialMaster)で訓練されたモデルと、正しい経路でのみ訓練されたモデルを比較し、前者が低いトライアル探索でより目に見えない定理を解くことを発見した。
論文参考訳（メタデータ） (2024-04-10T23:01:45Z)
REFACTOR: Learning to Extract Theorems from Proofs [29.44286369265644]
我々は、REFACTORが、人間が証明を書くのに使用する定理の19.6%を抽出できることを示した。新たに抽出された定理により,既存のMetaMathデータベースが構築可能であることを示す。また、新理論データセットでトレーニングされた証明者が、より多くのテスト定理を証明し、最先端のベースラインを上回ることを実証する。
論文参考訳（メタデータ） (2024-02-26T21:21:30Z)
MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文参考訳（メタデータ） (2024-02-14T05:57:58Z)
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。本研究では,LLM ベースの証明器 ReProver を開発した。
論文参考訳（メタデータ） (2023-06-27T17:05:32Z)
Proof Artifact Co-training for Theorem Proving with Language Models [4.934817254755007]
PACT(bf Proof bf Artifact bf Co-bf Training)は、カーネルレベルのコトレーニング用証明項から自己教師付きデータを抽出する一般的な手法である。我々は、Transformer言語モデルによって駆動されるニューラル定理証明器でリーンを計測し、PACTがテスト定理の保留組における成功率を証明する定理を32%から48%に改善することを示す。
論文参考訳（メタデータ） (2021-02-11T18:59:24Z)
PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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