Fugu-MT 論文翻訳(概要): Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving

論文の概要: Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving

arxiv url: http://arxiv.org/abs/2305.16366v1
Date: Thu, 25 May 2023 11:35:52 GMT
ステータス: 処理完了
システム内更新日: 2023-05-29 18:53:46.689656
Title: Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving
Title（参考訳）: エニグマの解法:形式的定理証明のためのサブゴールに基づく実証学習
Authors: Xueliang Zhao, Wenda Li, Lingpeng Kong
Abstract要約: 大型言語モデル(LLMs)は、形式定理証明の領域における興味深い探索の道を示す。本稿では,2つの要素からなるサブゴール型実演学習フレームワークを提案する。検証精度は38.9%から44.3%に向上した。
参考スコア（独自算出の注目度）: 15.624453757710798
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Large language models~(LLMs) present an intriguing avenue of exploration in the domain of formal theorem proving. Nonetheless, the full utilization of these models, particularly in terms of demonstration formatting and organization, remains an underexplored area. In an endeavor to enhance the efficacy of LLMs, we introduce a subgoal-based demonstration learning framework, consisting of two primary elements: Firstly, drawing upon the insights of subgoal learning from the domains of reinforcement learning and robotics, we propose the construction of distinct subgoals for each demonstration example and refine these subgoals in accordance with the pertinent theories of subgoal learning. Secondly, we build upon recent advances in diffusion models to predict the optimal organization, simultaneously addressing two intricate issues that persist within the domain of demonstration organization: subset selection and order determination. Through the integration of subgoal-based learning methodologies, we have successfully increased the prevailing proof accuracy from 38.9\% to 44.3\% on the miniF2F benchmark. Furthermore, the adoption of diffusion models for demonstration organization can lead to an additional enhancement in accuracy to 45.5\%, or a $5\times$ improvement in sampling efficiency compared with the long-standing state-of-the-art method. Our code is available at \url{https://github.com/HKUNLP/subgoal-theorem-prover}.
Abstract（参考訳）: 大規模言語モデル~(LLM)は形式定理証明の領域における興味深い探索の道を示す。にもかかわらず、これらのモデルの完全な利用、特にデモフォーマットと組織の観点からは、未調査領域である。まず, 強化学習とロボット工学の領域から, サブゴール学習の洞察を基礎として, 実演例ごとに異なるサブゴールの構築を提案し, サブゴール学習の関連する理論に従ってこれらのサブゴールを洗練させる。第二に, 拡散モデルの最近の進歩を活かして, 最適組織を予測し, デモ組織領域内で持続する2つの複雑な問題, サブセット選択と順序決定を同時に解決する。サブゴールをベースとした学習手法の統合により,MiniF2Fベンチマークの検証精度は38.9\%から44.3\%に向上した。さらに,実験組織への拡散モデルの適用により,45.5\%の精度向上や,長期間の最先端手法と比較してサンプリング効率の向上が5.5\times$に向上する可能性がある。我々のコードは \url{https://github.com/HKUNLP/subgoal-theorem-prover} で入手できる。

関連論文リスト

Proof Flow: Preliminary Study on Generative Flow Network Language Model Tuning for Formal Reasoning [11.268313729426627]
本稿では,形式的推論の領域,特にニューラル定理証明設定における概念実証について述べる。古典的な報酬最大化強化学習とは異なり、GFlowNetsは合成対象をサンプリングするための有望なアプローチとして登場した。我々の初期の結果は、GFlowNetが検索環境におけるモデル性能を向上させる可能性を示している。
論文参考訳（メタデータ） (2024-10-17T05:10:12Z)
Unleashing the Potential of the Diffusion Model in Few-shot Semantic Segmentation [56.87049651707208]
セマンティックはインコンテクストタスクへと発展し、一般化的セグメンテーションモデルを評価する上で重要な要素となった。我々の最初の焦点は、クエリイメージとサポートイメージの相互作用を容易にする方法を理解することであり、その結果、自己注意フレームワーク内のKV融合法が提案される。そこで我々はDiffewSというシンプルで効果的なフレームワークを構築し,従来の潜在拡散モデルの生成フレームワークを最大限に保持する。
論文参考訳（メタデータ） (2024-10-03T10:33:49Z)
SubgoalXL: Subgoal-based Expert Learning for Theorem Proving [37.115856591703974]
SubgoalXLは、正規の定理証明を強化するために、専門家の学習とサブゴールベースの証明を相乗化する新しいアプローチである。 SubgoalXLは、標準のminiF2Fデータセット上で、Isabelleで56.1%の最先端パフォーマンスを実現する。
論文参考訳（メタデータ） (2024-08-20T20:10:53Z)
Self-Refine Instruction-Tuning for Aligning Reasoning in Language Models [0.8133739801185272]
小さい言語モデルと大きい言語モデルの間の推論能力のアライメントは、主にスーパーバイザード・ファイン・チューニング(SFT)を通して行われる。そこで本研究では,より小さな言語モデルを用いて自己定義する自己記述型指導手法を提案する。コモンセンスと数学の推論タスクで得られた結果は、このアプローチがドメイン内とドメイン外の両方のシナリオでインストラクションチューニングを著しく上回っていることを示している。
論文参考訳（メタデータ） (2024-05-01T09:10:27Z)
Co-guiding for Multi-intent Spoken Language Understanding [53.30511968323911]
本稿では,2つのタスク間の相互指導を実現するための2段階のフレームワークを実装した,コガイドネットと呼ばれる新しいモデルを提案する。第1段階では,単一タスクによる教師付きコントラスト学習を提案し,第2段階ではコガイドによる教師付きコントラスト学習を提案する。マルチインテリジェントSLU実験の結果,我々のモデルは既存のモデルよりも大きなマージンで優れていることがわかった。
論文参考訳（メタデータ） (2023-11-22T08:06:22Z)
Knowledge Transfer-Driven Few-Shot Class-Incremental Learning [23.163459923345556]
FSCIL(Few-shot class-incremental Learning)は、古いクラスを忘れずに、いくつかのサンプルを使用して新しいクラスを継続的に学習することを目的としている。既存のFSCIL手法の進歩にもかかわらず、モデルの可塑性の最適化が不十分なため、提案手法は準最適である。本稿では,多種多様な擬似的漸進的タスクをエージェントとして頼りにし,知識伝達を実現するランダムエピソードサンプリング・拡張(RESA)戦略を提案する。
論文参考訳（メタデータ） (2023-06-19T14:02:45Z)
Variance-Preserving-Based Interpolation Diffusion Models for Speech Enhancement [53.2171981279647]
本稿では,VP-および分散拡散(VE)に基づく拡散法の両方をカプセル化するフレームワークを提案する。本研究では,拡散モデルで発生する一般的な困難を解析し,性能の向上とモデルトレーニングの容易化を図る。我々は,提案手法の有効性を示すために,公開ベンチマークを用いたいくつかの手法によるモデルの評価を行った。
論文参考訳（メタデータ） (2023-06-14T14:22:22Z)
Hierarchical Optimization-Derived Learning [58.69200830655009]
我々は,最適化モデル構築の本質的な動作とそれに対応する学習過程を同時に研究するために,階層型ODL(Hyerarchical ODL)という新しいフレームワークを構築した。これは、最適化と学習という2つの結合されたODLコンポーネントに対する最初の理論的保証である。
論文参考訳（メタデータ） (2023-02-11T03:35:13Z)
USER: Unified Semantic Enhancement with Momentum Contrast for Image-Text Retrieval [115.28586222748478]
Image-Text Retrieval (ITR) は、与えられたクエリに意味のあるターゲットインスタンスを、他のモダリティから検索することを目的としている。既存のアプローチは通常、2つの大きな制限に悩まされる。
論文参考訳（メタデータ） (2023-01-17T12:42:58Z)
Learning to Augment via Implicit Differentiation for Domain Generalization [107.9666735637355]
ドメイン一般化(DG)は、複数のソースドメインを活用してドメイン一般化可能なモデルを学ぶことで、この問題を克服することを目的としている。本稿では,AugLearnと呼ばれる新しい拡張型DG手法を提案する。 AugLearnは、PACS、Office-Home、Digits-DGの3つの標準DGベンチマークで効果を示す。
論文参考訳（メタデータ） (2022-10-25T18:51:51Z)
Let us Build Bridges: Understanding and Extending Diffusion Generative Models [19.517597928769042]
拡散に基づく生成モデルは、最近、有望な結果を得たが、多くのオープンな疑問を提起している。この研究は、理論的な理解を深めるために、全体的なフレームワークを再検討しようと試みている。 1)拡散生成モデルを学習するための最初の理論的誤り解析,2)異なる離散および制約された領域からのデータを学ぶための単純で統一的なアプローチを提案する。
論文参考訳（メタデータ） (2022-08-31T08:58:10Z)

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

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