論文の概要: 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のプロセスを定式化する。 エージェントは、深い政策勾配を用いて、有望な導出と各導出の中から適切な戦術を選択することを学習する。 この構造により、エージェントが(予測された)デッドエンド導出を効率的に破棄し、有望な代替品から導出を再開できる新しいバックトラッキング機構を導入することができる。 実験結果は、このフレームワークは人間の専門家を使用するアプローチのそれと匹敵するパフォーマンスを提供し、トレーニング中に見たことのない定理を証明できることを示しています。 さらに, フレームワークの各コンポーネントの役割について, アブレーション研究を用いて詳述する。

関連論文リスト

• Learning Rules Explaining Interactive Theorem Proving Tactic Prediction [5.229806149125529]
  この問題を帰納論理プログラミング(ILP)タスクとして表現する。 ILP表現を使用することで、追加で計算コストの高いプロパティをエンコードすることで、機能空間を豊かにしました。 我々は、このリッチな特徴空間を用いて、与えられた証明状態に戦術がいつ適用されたかを説明する規則を学ぶ。
  論文  参考訳（メタデータ） (2024-11-02T09:18:33Z)
• 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)
• 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)

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

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