論文の概要: Learning Equational Theorem Proving

• arxiv url: http://arxiv.org/abs/2102.05547v1
• Date: Wed, 10 Feb 2021 16:33:07 GMT
• ステータス: 処理完了
• システム内更新日: 2021-02-11 14:41:28.303785
• Title: Learning Equational Theorem Proving
• Title（参考訳）: 方程式定理の学習
• Authors: Jelle Piepenbrock, Tom Heskes, Mikol\'a\v{s} Janota, Josef Urban
• Abstract要約: 深層強化学習環境下で証明された方程式定理を学習するための最短解イミテーション学習(3SIL)を開発した。 自己学習されたモデルは、準群論におけるトップオープン予想の1つによって生じる問題を証明する上で、最先端のパフォーマンスを達成する。
• 参考スコア（独自算出の注目度）: 2.8784416089703955
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We develop Stratified Shortest Solution Imitation Learning (3SIL) to learn equational theorem proving in a deep reinforcement learning (RL) setting. The self-trained models achieve state-of-the-art performance in proving problems generated by one of the top open conjectures in quasigroup theory, the Abelian Inner Mapping (AIM) Conjecture. To develop the methods, we first use two simpler arithmetic rewriting tasks that share tree-structured proof states and sparse rewards with the AIM problems. On these tasks, 3SIL is shown to significantly outperform several established RL and imitation learning methods. The final system is then evaluated in a standalone and cooperative mode on the AIM problems. The standalone 3SIL-trained system proves in 60 seconds more theorems (70.2%) than the complex, hand-engineered Waldmeister system (65.5%). In the cooperative mode, the final system is combined with the Prover9 system, proving in 2 seconds what standalone Prover9 proves in 60 seconds.
• Abstract（参考訳）: 3SIL(Stratified Shortest Solution Imitation Learning)を開発して、深層強化学習(RL)設定で証明する方程式定理を学習します。 自己訓練モデルは、準群理論におけるトップオープン予想の1つであるAbelian Inner Mapping (AIM) 予想によって生じる問題を証明して、最先端のパフォーマンスを達成している。 提案手法の開発には,まず,木構造証明状態とAIM問題とのスパース報酬を共有可能な2つの簡単な算術書き換えタスクを使用する。 これらのタスクでは、3SILは、いくつかの確立されたRLおよび模倣学習方法を大幅に上回ることが示されている。 最終的なシステムは、AIM問題に関するスタンドアロンおよび協調モードで評価されます。 スタンドアロンの3SIL訓練システムは、複雑な手動のウォルドマイスターシステム(65.5%)よりも60秒間(70.2%)の定理を証明している。 協調モードでは、最終システムはProver9システムと組み合わせられ、2秒でスタンドアロンのProver9が60秒で証明できることが証明される。

関連論文リスト

• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。 我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。 我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
  論文  参考訳（メタデータ） (2024-11-04T05:57:40Z)
• Dualformer: Controllable Fast and Slow Thinking by Learning with Randomized Reasoning Traces [40.127653552777204]
  人間の思考は、システム1とシステム2の2つのシステムによって管理されている。 近年, System 2 プロセスを Transformer に組み込むことで推論能力が大きく向上することが報告されている。 高速かつ低速な推論モードをシームレスに統合する単一トランスフォーマーモデルであるDualformerを提案する。
  論文  参考訳（メタデータ） (2024-10-13T16:53:02Z)
• Networks of Networks: Complexity Class Principles Applied to Compound AI Systems Design [63.24275274981911]
  多くの言語モデル推論コールからなる複合AIシステムは、ますます採用されている。 本研究では,提案した回答の生成と正当性検証の区別を中心に,ネットワークネットワーク(NoN)と呼ばれるシステムを構築した。 我々は,Kジェネレータを備えた検証器ベースの判定器NoNを導入し,"Best-of-K"あるいは"judge-based"複合AIシステムのインスタンス化を行う。
  論文  参考訳（メタデータ） (2024-07-23T20:40:37Z)
• 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)
• Reinforcement Learning for Branch-and-Bound Optimisation using Retrospective Trajectories [72.15369769265398]
  機械学習は分岐のための有望なパラダイムとして登場した。 分岐のための単純かつ効果的なRLアプローチであるレトロ分岐を提案する。 我々は現在最先端のRL分岐アルゴリズムを3～5倍に上回り、500の制約と1000の変数を持つMILP上での最高のILメソッドの性能の20%以内である。
  論文  参考訳（メタデータ） (2022-05-28T06:08:07Z)
• HyperTree Proof Search for Neural Theorem Proving [14.677400513932852]
  本稿では,変圧器を用いた自動定理証明のためのオンライン学習手順を提案する。 我々のモデルは、オンライントレーニングを通じて以前の証明検索から学習し、トレーニング分布から遠く離れた領域に一般化することができる。 HTPSだけでは、アノテートされた証明に基づいて訓練されたモデルがメタマス定理の65.4%を証明し、GPT-fにより56.5%の先行状態を著しく上回ることを示した。
  論文  参考訳（メタデータ） (2022-05-23T17:49:55Z)
• RvS: What is Essential for Offline RL via Supervised Learning? [77.91045677562802]
  近年の研究では、時間差(TD)のない教師あり学習だけでオフラインRLに極めて効果的であることが示されている。 あらゆる環境スイートにおいて、2層フィードフォワードによる可能性の最大化は競争力がある。 彼らはまた、ランダムデータに対して比較的弱い既存のRvS法の限界を探索する。
  論文  参考訳（メタデータ） (2021-12-20T18:55:16Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。 実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
  論文  参考訳（メタデータ） (2020-02-17T16:06:02Z)

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

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