論文の概要: Prolog Technology Reinforcement Learning Prover

• arxiv url: http://arxiv.org/abs/2004.06997v1
• Date: Wed, 15 Apr 2020 10:52:04 GMT
• ステータス: 処理完了
• システム内更新日: 2022-12-13 04:16:37.851708
• Title: Prolog Technology Reinforcement Learning Prover
• Title（参考訳）: Prolog Technology Reinforcement Learning Prover
• Authors: Zsolt Zombori, Josef Urban, Chad E. Brown
• Abstract要約: ツールキットの中核はコンパクトで容易にPrologベースの自動定理証明であるplCoPである。 plCoPは、LeadCoP Prologの実装に基づいて構築されており、rlCoPシステムで実施された学習誘導のMonte-Carlo Tree Searchを追加している。 その他のコンポーネントには、plCoPとマシン学習者のPythonインターフェース、plCoP証明の有効性を検証する外部証明チェッカーなどがある。
• 参考スコア（独自算出の注目度）: 0.6445605125467572
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to extend Prolog-based automated theorem prover called plCoP. plCoP builds on the leanCoP Prolog implementation and adds learning-guided Monte-Carlo Tree Search as done in the rlCoP system. Other components include a Python interface to plCoP and machine learners, and an external proof checker that verifies the validity of plCoP proofs. The toolkit is evaluated on two benchmarks and we demonstrate its extendability by two additions: (1) guidance is extended to reduction steps and (2) the standard leanCoP calculus is extended with rewrite steps and their learned guidance. We argue that the Prolog setting is suitable for combining statistical and symbolic learning methods. The complete toolkit is publicly released.
• Abstract（参考訳）: 本稿では,接続計算における自動定理の導出実験のための強化学習ツールキットを提案する。 このツールキットのコアはコンパクトで拡張しやすいprologベースの自動定理証明器plcopである。 plCoPは、LeadCoP Prologの実装に基づいて構築されており、rlCoPシステムで実施された学習誘導のMonte-Carlo Tree Searchを追加している。 その他のコンポーネントには、plCoPとマシン学習者のPythonインターフェース、plCoP証明の有効性を検証する外部証明チェッカーなどがある。 このツールキットは2つのベンチマークで評価され,(1)ガイダンスを縮小ステップに拡張し,(2)標準の leanCoP 計算を書き換えステップと学習ガイダンスで拡張する,という2つの追加によって拡張性を示す。 プロログ設定は統計的学習法と記号的学習法を組み合わせるのに適している。 完全なツールキットが公開されている。

関連論文リスト

• Cobblestone: Iterative Automation for Formal Verification [11.445689801392657]
  Coqのような証明アシスタントを用いた形式的検証は、ソフトウェア品質を改善する効果的な方法であるが、高価である。 最近の研究では、機械学習を使って証明を自動的に合成し、検証の労力を削減しているが、これらのツールは、望まれるソフトウェアプロパティのほんの一部しか証明できない。 我々は, 証明合成における部分的な進歩を生かして, 技術状況を改善する新しい証明合成手法であるCobblestoneを紹介した。
  論文  参考訳（メタデータ） (2024-10-25T19:25:00Z)
• To CoT or not to CoT? Chain-of-thought helps mainly on math and symbolic reasoning [55.52872152909785]
  Chain-of-Thought (CoT) は,大規模言語モデル (LLM) から推論能力を引き出すデファクト手法である。 私たちは、CoTが主に数学や論理学を含むタスクに強いパフォーマンス上の利点をもたらし、他のタスクよりもはるかに少ない利益をもたらすことを示しています。
  論文  参考訳（メタデータ） (2024-09-18T17:55:00Z)
• CoqPyt: Proof Navigation in Python in the Era of LLMs [5.029445580644576]
  本稿では,Coq証明アシスタントと対話するPythonツールであるCoqPytについて述べる。 CoqPytは、リッチな前提データの抽出など、新しい機能を提供することで、他のCoq関連のツールを改善している。
  論文  参考訳（メタデータ） (2024-05-07T12:50:28Z)
• StepCoder: Improve Code Generation with Reinforcement Learning from Compiler Feedback [58.20547418182074]
  2つの主要コンポーネントからなるコード生成の新しいフレームワークであるStepCoderを紹介します。 CCCSは、長いシーケンスのコード生成タスクをCurriculum of Code Completion Subtaskに分割することで、探索課題に対処する。 FGOは、未実行のコードセグメントをマスクすることでのみモデルを最適化し、Fine-Grained Optimizationを提供する。 提案手法は,出力空間を探索し,対応するベンチマークにおいて最先端の手法より優れた性能を発揮する。
  論文  参考訳（メタデータ） (2024-02-02T13:14:31Z)
• Generalized Convergence Analysis of Tsetlin Machines: A Probabilistic Approach to Concept Learning [20.519261060300302]
  本稿では,Tsetlinオートマトンに基づく機械学習アルゴリズムの総合収束解析について述べる。 本稿では,確率論的概念学習(PCL, Probabilistic Concept Learning)と呼ばれる新しいフレームワークを提案する。 我々は、任意の節$C_k$に対して、PCLが0.5p_k1$のときにリテラルの結合に収束することを確認する理論的証明を確立する。
  論文  参考訳（メタデータ） (2023-10-03T12:21:41Z)
• Reinforcement Learning and Data-Generation for Syntax-Guided Synthesis [0.0]
  我々はモンテカルロ木探索(MCTS)を用いて候補解の空間を探索するSyGuSの強化学習アルゴリズムを提案する。 我々のアルゴリズムは,木に縛られた高信頼度と組み合わさって,探索と利用のバランスをとるためのポリシーと価値関数を学習する。
  論文  参考訳（メタデータ） (2023-07-13T11:30:50Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• Evaluating and Improving Tool-Augmented Computation-Intensive Math Reasoning [75.74103236299477]
  CoT(Chain-of- Thought prompting)とツール拡張は、大きな言語モデルを改善するための効果的なプラクティスとして検証されている。 ツールインターフェース,すなわち textbfDELI を用いた推論ステップを考慮に入れた新しい手法を提案する。 CARPと他の6つのデータセットの実験結果から、提案されたDELIは、主に競合ベースラインを上回っていることが示された。
  論文  参考訳（メタデータ） (2023-06-04T17:02:59Z)
• CLAWSAT: Towards Both Robust and Accurate Code Models [74.57590254102311]
  比較学習(CL)と逆学習を統合して、コードモデルの堅牢性と精度を協調的に最適化する。 私たちの知る限りでは、これはコードモデルにおける(マルチビュー)コードの難読化の堅牢性と正確性について調査し、活用する最初の体系的な研究です。
  論文  参考訳（メタデータ） (2022-11-21T18:32:50Z)
• Latte: Cross-framework Python Package for Evaluation of Latent-Based Generative Models [65.51757376525798]
  Latteは、潜伏型生成モデルを評価するためのPythonライブラリである。 LatteはPyTorchと/Kerasの両方と互換性があり、関数型APIとモジュール型APIの両方を提供する。
  論文  参考訳（メタデータ） (2021-12-20T16:00:28Z)
• PalmTree: Learning an Assembly Language Model for Instruction Embedding [8.74990895782223]
  汎用命令埋め込み生成のためのアセンブリ言語モデルであるPalmTreeの事前トレーニングを提案する。 PalmTreeは固有のメトリクスに対して最高のパフォーマンスを持ち、下流タスクの他の命令埋め込みスキームよりも優れています。
  論文  参考訳（メタデータ） (2021-01-21T22:30:01Z)

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

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