論文の概要: TacticZero: Learning to Prove Theorems from Scratch with Deep
Reinforcement Learning
- arxiv url: http://arxiv.org/abs/2102.09756v1
- Date: Fri, 19 Feb 2021 06:08:39 GMT
- ステータス: 処理完了
- システム内更新日: 2021-02-22 13:32:11.203289
- Title: TacticZero: Learning to Prove Theorems from Scratch with Deep
Reinforcement Learning
- Title(参考訳): TacticZero: 深層強化学習によるスクラッチからの定理の学習
- Authors: Minchao Wu, Michael Norrish, Christian Walder, Amir Dezfouli
- Abstract要約: 深層強化学習を用いた対話型定理証明(ITP)の新しい手法を提案する。
我々は、各状態が潜在的な導出経路の集合を表すマルコフ決定プロセス(MDP)としてITPのプロセスを定式化する。
このフレームワークは、人間の専門家を使ったアプローチに匹敵するパフォーマンスを提供する。
- 参考スコア(独自算出の注目度): 6.764610878007278
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We propose a novel approach to interactive theorem-proving (ITP) using deep
reinforcement learning. Unlike previous work, our framework is able to prove
theorems both end-to-end and from scratch (i.e., without relying on example
proofs from human experts). We formulate the process of ITP as a Markov
decision process (MDP) in which each state represents a set of potential
derivation paths. The agent learns to select promising derivations as well as
appropriate tactics within each derivation using deep policy gradients. This
structure allows us to introduce a novel backtracking mechanism which enables
the agent to efficiently discard (predicted) dead-end derivations and restart
the derivation from promising alternatives. Experimental results show that the
framework provides comparable performance to that of the approaches that use
human experts, and that it is also capable of proving theorems that it has
never seen during training. We further elaborate the role of each component of
the framework using ablation studies.
- Abstract(参考訳): 深層強化学習を用いた対話型定理証明(ITP)の新しい手法を提案する。
これまでの研究とは異なり、我々のフレームワークは、エンドツーエンドとスクラッチの両方(つまり、人間の専門家による例証に頼ることなく)の定理を証明できる。
我々は、各状態が潜在的な導出経路の集合を表すマルコフ決定プロセス(MDP)としてITPのプロセスを定式化する。
エージェントは、深い政策勾配を用いて、有望な導出と各導出の中から適切な戦術を選択することを学習する。
この構造により、エージェントが(予測された)デッドエンド導出を効率的に破棄し、有望な代替品から導出を再開できる新しいバックトラッキング機構を導入することができる。
実験結果は、このフレームワークは人間の専門家を使用するアプローチのそれと匹敵するパフォーマンスを提供し、トレーニング中に見たことのない定理を証明できることを示しています。
さらに, フレームワークの各コンポーネントの役割について, アブレーション研究を用いて詳述する。
関連論文リスト
- Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳(メタデータ) (2024-07-14T01:43:07Z) - Proving Theorems Recursively [80.42431358105482]
本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。
従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。
また,POETRYが検出した最大証明長は10~26。
論文 参考訳(メタデータ) (2024-05-23T10:35:08Z) - A Survey on Deep Learning for Theorem Proving [16.28502772608166]
定理証明は数学の基本的側面であり、数学言語の非公式な推論から形式体系における厳密な導出まで及ぶ。
近年、ディープラーニングの進歩は、定理証明のプロセスを強化するためにこれらの技術を探究する研究の急増を引き起こしている。
本調査は, この急速に成長する分野において, さらなる研究努力の触媒となることを目的として, 定理証明における深層学習アプローチの基礎的参考として機能することを目的としている。
論文 参考訳(メタデータ) (2024-04-15T17:07:55Z) - Automated Completion of Statements and Proofs in Synthetic Geometry: an
Approach based on Constraint Solving [0.0]
不完全予想と不完全証明を完遂する枠組みを提案する。
このフレームワークは、不足した仮定を持つ予想を適切な定理に変えることができる。
また、提案したフレームワークは、人間の読みやすいマシンチェック可能な証明に証明スケッチを完成させるのに役立ちます。
論文 参考訳(メタデータ) (2024-01-22T12:49:08Z) - Towards a General Framework for Continual Learning with Pre-training [55.88910947643436]
本稿では,事前学習を用いた逐次到着タスクの連続学習のための一般的な枠組みを提案する。
我々はその目的を,タスク内予測,タスク同一性推論,タスク適応予測という3つの階層的構成要素に分解する。
本稿では,パラメータ効率細調整(PEFT)技術と表現統計量を用いて,これらのコンポーネントを明示的に最適化する革新的な手法を提案する。
論文 参考訳(メタデータ) (2023-10-21T02:03:38Z) - Hierarchical Decomposition of Prompt-Based Continual Learning:
Rethinking Obscured Sub-optimality [55.88910947643436]
大量のラベルのないデータを実際に扱うためには、自己教師付き事前トレーニングが不可欠である。
HiDe-Promptは、タスク固有のプロンプトと統計のアンサンブルで階層的なコンポーネントを明示的に最適化する革新的なアプローチである。
実験では,HiDe-Promptの優れた性能と,継続学習における事前学習パラダイムへの頑健さを実証した。
論文 参考訳(メタデータ) (2023-10-11T06:51:46Z) - PACER: A Fully Push-forward-based Distributional Reinforcement Learning
Algorithm [13.18145235926629]
我々は,Push-forward-based Actor-Critic EncourageR (PACER)と呼ばれる,Push-forward-based DistributionReinforcement Learningアルゴリズムを提案する。
PACERは最大効用値ポリシー勾配を確立し、アクターと批評家の両方の構築においてプッシュフォワード演算子を同時に活用する。
各種連続制御ベンチマークの実験的評価は、最先端のアルゴリズムよりもアルゴリズムの方が優れていることを示す。
論文 参考訳(メタデータ) (2023-06-11T09:45:31Z) - Reinforcement Learning with a Terminator [80.34572413850186]
我々は, TerMDP のパラメータを学習し, 推定問題の構造を活用し, 状態ワイドな信頼境界を提供する。
我々はこれらを用いて証明可能な効率のよいアルゴリズムを構築し、終端を考慮し、その後悔を抑える。
論文 参考訳(メタデータ) (2022-05-30T18:40:28Z) - Learning to Guide a Saturation-Based Theorem Prover [9.228237801323042]
TRAILは、ニューラルネットワーク内で証明される飽和に基づく定理の中核要素を特徴付ける、深い学習に基づく定理証明のアプローチである。
我々の知る限りでは、TRAILは最先端の伝統的な定理証明器の性能を超える最初の強化学習に基づくアプローチである。
論文 参考訳(メタデータ) (2021-06-07T18:35:57Z) - Learning to Prove from Synthetic Theorems [41.74768503409581]
自動定理証明に機械学習を適用する上での大きな課題は、トレーニングデータの不足である。
本稿では,一組の公理から生成される合成定理による学習に依存するアプローチを提案する。
このような定理が自動証明器の訓練に利用でき、学習された証明器が人間の生成した定理にうまく移行できることが示される。
論文 参考訳(メタデータ) (2020-06-19T17:48:09Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳(メタデータ) (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。