論文の概要: Lean-STaR: Learning to Interleave Thinking and Proving

• arxiv url: http://arxiv.org/abs/2407.10040v1
• Date: Sun, 14 Jul 2024 01:43:07 GMT
• ステータス: 処理完了
• システム内更新日: 2024-07-16 19:48:19.188193
• Title: Lean-STaR: Learning to Interleave Thinking and Proving
• Title（参考訳）: Lean-STaR: 思考と証明のインターリーブを学ぶ
• Authors: Haohan Lin, Zhiqing Sun, Yiming Yang, Sean Welleck,
• Abstract要約: 証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
• 参考スコア（独自算出の注目度）: 53.923617816215774
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Traditional language model-based theorem proving assumes that by training on a sufficient amount of formal proof data, a model will learn to prove theorems. Our key observation is that a wealth of informal information that is not present in formal proofs can be useful for learning to prove theorems. For instance, humans think through steps of a proof, but this thought process is not visible in the resulting code. We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof, thereby boosting the model's theorem-proving capabilities. Lean-STaR uses retrospective ground-truth tactics to generate synthetic thoughts for training the language model. At inference time, the trained model directly generates the thoughts prior to the prediction of the tactics in each proof step. Building on the self-taught reasoner framework, we then apply expert iteration to further fine-tune the model on the correct proofs it samples and verifies using the Lean solver. Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment, significantly outperforming base models ($\boldsymbol{43.4\% \rightarrow 46.3\%,}$ Pass@64). We also analyze the impact of the augmented thoughts on various aspects of the theorem proving process, providing insights into their effectiveness.
• Abstract（参考訳）: 従来の言語モデルに基づく定理証明は、十分な量の形式的証明データをトレーニングすることで、モデルが定理を証明することを学ぶと仮定する。 我々のキーとなる観察は、形式的な証明に存在しない多くの非公式な情報が、定理を証明するための学習に役立つことである。 例えば、人間は証明のステップを通して考えるが、この思考プロセスは結果のコードでは見えない。 証明の各ステップに先立って非公式な思考を生成するために、言語モデルをトレーニングするためのフレームワークであるLean-STaRを紹介します。 Lean-STaRは、言語モデルをトレーニングするための合成思考を生成するために、レトロスペクティブの地道戦略を使用している。 推論時に、トレーニングされたモデルは、各証明ステップにおける戦術の予測に先立って、直接思考を生成する。 自己学習の推論フレームワークに基づいて、専門家のイテレーションを適用して、モデルがサンプリングした正しい証明をさらに微調整し、リーンソルバを使って検証します。 Lean-STaRは、Lean定理の証明環境におけるminiF2F-testベンチマークの最先端の結果を達成し、ベースモデル(\boldsymbol{43.4\% \rightarrow 46.3\%,}$ Pass@64)よりも大幅に優れています。 また,拡張思考が定理証明過程の諸側面に与える影響を分析し,その効果について考察する。

関連論文リスト

• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。 我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。 我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
  論文  参考訳（メタデータ） (2024-11-04T05:57:40Z)
• Next-Token Prediction Task Assumes Optimal Data Ordering for LLM Training in Proof Generation [27.60611509339328]
  1つのトレーニングデータサンプルの最適順序は、特定の証明ステップの関連中間監督が、その証明ステップの左側に常に配置されているときに発生すると論じる。 証明が直感的に逐次順序にある場合、トレーニングが最も効果的であることを示す。
  論文  参考訳（メタデータ） (2024-10-30T18:00:04Z)
• Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving [41.23045212775232]
  探索経路の失敗から学習する訓練モデルの利点を実証する。 既存のオープンソース定理証明データセットにそのような試行錯誤データが欠如しているにもかかわらず、直観論的命題論理定理のデータセットをキュレートする。 比較的短いトライアル・アンド・エラー情報(TrialMaster)で訓練されたモデルと、正しい経路でのみ訓練されたモデルを比較し、前者が低いトライアル探索でより目に見えない定理を解くことを発見した。
  論文  参考訳（メタデータ） (2024-04-10T23:01:45Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• Baldur: Whole-Proof Generation and Repair with Large Language Models [8.100054850290507]
  我々は、自然言語のテキストとコードに基づいて訓練され、証明について微調整された大きな言語モデルを使用して、一度に定理のすべての証明を生成する。 我々は、この証明生成モデルと微調整の補修モデルを組み合わせて、生成した証明を修復し、さらに証明力を増強する。 本手法をプロトタイプであるBaldurで評価し、6,336 Isabelle/HOL定理とその証明のベンチマークで評価する。
  論文  参考訳（メタデータ） (2023-03-08T22:00:15Z)
• NaturalProver: Grounded Mathematical Proof Generation with Language Models [84.2064569475095]
  自然数理言語における定理証明は、数学の進歩と教育において中心的な役割を果たす。 本研究では,背景参照を条件づけて証明を生成する言語モデルであるNaturalProverを開発する。 NaturalProverは、短い(2-6ステップ)証明を必要とするいくつかの定理を証明でき、40%の時間で正しいと評価された次のステップの提案を提供することができる。
  論文  参考訳（メタデータ） (2022-05-25T17:01:18Z)
• Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
  本稿では, 忠実度スルー・カウンタファクトの方法論について紹介する。 これは、説明に表される論理述語に基づいて、反実仮説を生成する。 そして、そのモデルが表現された論理と反ファクトの予測が一致しているかどうかを評価する。
  論文  参考訳（メタデータ） (2022-05-25T03:40:59Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)
• 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)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)

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

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