論文の概要: 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秒で証明できることが証明される。

関連論文リスト

• On the Emergence of Thinking in LLMs I: Searching for the Right Intuition [34.32871896067864]
  自己学習による強化学習(RLSP)というポストトレーニングフレームワークを提案する。 RLSPは、推論プロセスの人間または合成的なデモンストレーションによる微調整、多種多様な効率的な推論行動を促進するための探索報酬信号の使用、報酬ハッキングを予防しながら正当性を確保するための結果検証器によるRLトレーニングの3段階を含む。 数学領域における実証的研究は、RLSPが推論を改善することを示している。
  論文  参考訳（メタデータ） (2025-02-10T18:52:04Z)
• STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving [33.61458249318183]
  セルフプレイ・セオレム・プロバー(STP)は、予想と証明という2つの役割を担っている。 STPは同時に、予想と証明という2つの役割を担っている。 私たちはLeanとIsabelleの2つの形式的検証ツールで評価します。
  論文  参考訳（メタデータ） (2025-01-31T23:01:48Z)
• Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,より優れたサンプル効率を有する定理証明手法であるProofAugを提案する。 本手法は,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• Kimi k1.5: Scaling Reinforcement Learning with LLMs [84.2229964736678]
  我々は、強化学習で訓練された最新のマルチモーダル言語モデル、Kimi k1.5の訓練実践について報告する。 長いコンテキストスケーリングと改善されたポリシー最適化手法が、我々のアプローチの鍵となる要素である。 本システムは,複数のベンチマークやモダリティに対して,最先端の推論性能を実現する。
  論文  参考訳（メタデータ） (2025-01-22T02:48:14Z)
• 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)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• LEGO-Prover: Neural Theorem Proving with Growing Libraries [86.1191481712352]
  LEGO-Prover では,証明された補題を含むスキルライブラリを,定理証明に使用される LLM の能力を高めるためのスキルとして活用する。 LEGO-Proverは、証明をモジュール的に構築することにより、ライブラリから取得した既存のスキルを活用し、証明プロセス中に新しいスキルを作成することができる。 我々のアブレーション研究は、これらの新たなスキルが定理の証明に役立つことを示唆し、47.1%から50.4%に改善した。
  論文  参考訳（メタデータ） (2023-10-01T12:47:59Z)
• 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)

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

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