論文の概要: SubgoalXL: Subgoal-based Expert Learning for Theorem Proving

• arxiv url: http://arxiv.org/abs/2408.11172v1
• Date: Tue, 20 Aug 2024 20:10:53 GMT
• ステータス: 処理完了
• システム内更新日: 2024-08-22 21:06:50.098964
• Title: SubgoalXL: Subgoal-based Expert Learning for Theorem Proving
• Title（参考訳）: SubgoalXL: 定理証明のためのサブゴールベースエキスパートラーニング
• Authors: Xueliang Zhao, Lin Zheng, Haige Bo, Changran Hu, Urmish Thakker, Lingpeng Kong,
• Abstract要約: SubgoalXLは、正規の定理証明を強化するために、専門家の学習とサブゴールベースの証明を相乗化する新しいアプローチである。 SubgoalXLは、標準のminiF2Fデータセット上で、Isabelleで56.1%の最先端パフォーマンスを実現する。
• 参考スコア（独自算出の注目度）: 37.115856591703974
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal theorem proving, a field at the intersection of mathematics and computer science, has seen renewed interest with advancements in large language models (LLMs). This paper introduces SubgoalXL, a novel approach that synergizes subgoal-based proofs with expert learning to enhance LLMs' capabilities in formal theorem proving within the Isabelle environment. SubgoalXL addresses two critical challenges: the scarcity of specialized mathematics and theorem-proving data, and the need for improved multi-step reasoning abilities in LLMs. By optimizing data efficiency and employing subgoal-level supervision, SubgoalXL extracts richer information from limited human-generated proofs. The framework integrates subgoal-oriented proof strategies with an expert learning system, iteratively refining formal statement, proof, and subgoal generators. Leveraging the Isabelle environment's advantages in subgoal-based proofs, SubgoalXL achieves a new state-of-the-art performance of 56.1\% in Isabelle on the standard miniF2F dataset, marking an absolute improvement of 4.9\%. Notably, SubgoalXL successfully solves 41 AMC12, 9 AIME, and 3 IMO problems from miniF2F. These results underscore the effectiveness of maximizing limited data utility and employing targeted guidance for complex reasoning in formal theorem proving, contributing to the ongoing advancement of AI reasoning capabilities. The implementation is available at \url{https://github.com/zhaoxlpku/SubgoalXL}.
• Abstract（参考訳）: 数学と計算機科学の交差する分野である形式的定理証明は、大きな言語モデル(LLM)の進歩に新たな関心を抱いている。 本稿では,Isabelle 環境での形式的定理証明における LLM の能力を高めるために,サブゴールに基づく証明をエキスパートラーニングと相乗化するための新しいアプローチである SubgoalXL を紹介する。 SubgoalXLは2つの重要な課題に対処する: 特殊数学と定理証明データの不足と、LLMにおける多段階推論能力の改善の必要性。 データの効率を最適化し、サブゴールレベルの監視を採用することで、SubgoalXLは、限られた人間生成証明からよりリッチな情報を抽出する。 このフレームワークは、サブゴール指向の証明戦略をエキスパート学習システムと統合し、形式文、証明、サブゴール生成を反復的に洗練する。 SubgoalXLは、Isabelle環境の利点をサブゴールベースの証明で活用し、標準のminiF2Fデータセット上で56.1\%の最先端パフォーマンスを実現し、4.9\%の絶対的な改善を示している。 特にSubgoalXLは、MiniF2Fから41のAMC12、9のAIME、3のIMO問題を解くことに成功した。 これらの結果は、AI推論能力の継続的な進歩に寄与し、限定データユーティリティの最大化と、フォーマルな定理証明における複雑な推論のための目標ガイダンスの活用の有効性を裏付けるものである。 実装は \url{https://github.com/zhaoxlpku/SubgoalXL} で公開されている。

関連論文リスト

• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts [26.98890165420689]
  TheoremLlamaは、汎用的なLean4エキスパートをトレーニングするエンドツーエンドフレームワークである。 我々のフレームワークは,MiniF2F-ValidデータセットとTestデータセットでそれぞれ36.48%,33.61%の累積精度を達成した。
  論文  参考訳（メタデータ） (2024-07-03T15:36:18Z)
• Proving Theorems Recursively [80.42431358105482]
  本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。 従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。 また,POETRYが検出した最大証明長は10～26。
  論文  参考訳（メタデータ） (2024-05-23T10:35:08Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• 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)
• Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving [15.624453757710798]
  大型言語モデル(LLMs)は、形式定理証明の領域における興味深い探索の道を示す。 本稿では,2つの要素からなるサブゴール型実演学習フレームワークを提案する。 検証精度は38.9%から44.3%に向上した。
  論文  参考訳（メタデータ） (2023-05-25T11:35:52Z)

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

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