Fugu-MT 論文翻訳(概要): STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving

論文の概要: STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving

arxiv url: http://arxiv.org/abs/2502.00212v2
Date: Tue, 04 Feb 2025 07:20:28 GMT
ステータス: 翻訳完了
システム内更新日: 2025-02-05 15:01:30.112306
Title: STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
Title（参考訳）: STP:反復的推論と証明による自己再生LLM定理証明器
Authors: Kefan Dong, Tengyu Ma,
Abstract要約: セルフプレイ・セオレム・プロバー(STP)は、予想と証明という2つの役割を担っている。 STPは同時に、予想と証明という2つの役割を担っている。私たちはLeanとIsabelleの2つの形式的検証ツールで評価します。
参考スコア（独自算出の注目度）: 33.61458249318183
License:
Abstract: A fundamental challenge in formal theorem proving by LLMs is the lack of high-quality training data. Although reinforcement learning or expert iteration partially mitigates this issue by alternating between LLM generating proofs and finetuning them on correctly generated ones, performance quickly plateaus due to the scarcity of correct proofs (sparse rewards). To keep improving the models with limited data, we draw inspiration from mathematicians, who continuously develop new results, partly by proposing novel conjectures or exercises (which are often variants of known results) and attempting to solve them. We design the Self-play Theorem Prover (STP) that simultaneously takes on two roles, conjecturer and prover, each providing training signals to the other. The conjecturer is trained iteratively on previously generated conjectures that are barely provable by the current prover, which incentivizes it to generate increasingly challenging conjectures over time. The prover attempts to prove the conjectures with standard expert iteration. We evaluate STP with both Lean and Isabelle formal versifiers. With 19.8 billion tokens generated during the training in Lean, STP proves 26.3% of the statements in the LeanWorkbook dataset, doubling the previous best result of 13.2% achieved through expert iteration. The final model achieves state-of-the-art performance among whole-proof generation methods on miniF2F-test (61.1%, pass@3200), Proofnet-test (23.1%, pass@3200) and PutnamBench (8/644, pass@64).
Abstract（参考訳）: LLMによる形式定理の証明における基本的な課題は、高品質なトレーニングデータの欠如である。強化学習や専門家の反復は、LSM生成証明と正しい生成証明の微調整を交互に行い、この問題を部分的に緩和するが、正しい証明の不足(わずかな報奨)により、性能は急速に低下する。限られたデータでモデルを改良し続けるため、数学者からインスピレーションを得て、新しい予想やエクササイズ(しばしば既知の結果の変種である)を提案し、それを解こうとする。我々は,2つの役割,推測と証明を同時に行うセルフプレイ・セオリーム・プロバー(STP)を設計し,それぞれが他方にトレーニング信号を提供する。予想者は、現在の証明者によってほとんど証明できない以前に生成された予想に基づいて反復的に訓練される。証明者は、標準的な専門家反復で予想を証明しようと試みる。 STPをLeanとIsabelleの両形式変換器で評価する。リーンのトレーニング中に18億のトークンが生成されるSTPは、LeanWorkbookデータセットの文の26.3%を証明している。最終モデルは、miniF2F-test (61.1%、pass@3200)、Proofnet-test (23.1%、pass@3200)、PatnamBench (8/644、pass@64) における全防御生成メソッドの最先端のパフォーマンスを達成する。

関連論文リスト

Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
論文参考訳（メタデータ） (2024-11-04T05:57:40Z)
Proof Automation with Large Language Models [6.587933406842906]
大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
論文参考訳（メタデータ） (2024-09-22T00:19:27Z)
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)
MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文参考訳（メタデータ） (2024-02-14T05:57:58Z)
Learning Better Representations From Less Data For Propositional Satisfiability [7.449724123186386]
我々は、命題が満足できるという2つの課題に対処するニュールレス(NeuRes)というニューロシンボリックなアプローチを提案する。我々のモデルは、分類のみのために訓練されたモデルよりも優れた表現を学習し、データ効率はずっと高い。このモデルでは,NuroSATよりも,正しく分類された例と証明された例の両方において,はるかに優れた性能が得られることを示す。
論文参考訳（メタデータ） (2024-02-13T10:50:54Z)
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)
LEGO-Prover: Neural Theorem Proving with Growing Libraries [86.1191481712352]
LEGO-Prover では,証明された補題を含むスキルライブラリを,定理証明に使用される LLM の能力を高めるためのスキルとして活用する。 LEGO-Proverは、証明をモジュール的に構築することにより、ライブラリから取得した既存のスキルを活用し、証明プロセス中に新しいスキルを作成することができる。我々のアブレーション研究は、これらの新たなスキルが定理の証明に役立つことを示唆し、47.1%から50.4%に改善した。
論文参考訳（メタデータ） (2023-10-01T12:47:59Z)
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。本研究では,LLM ベースの証明器 ReProver を開発した。
論文参考訳（メタデータ） (2023-06-27T17:05:32Z)
Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文参考訳（メタデータ） (2022-05-25T02:22:30Z)
PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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