論文の概要: 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つの追加によって拡張性を示す。
プロログ設定は統計的学習法と記号的学習法を組み合わせるのに適している。
完全なツールキットが公開されている。
関連論文リスト
- Pruner: An Efficient Cross-Platform Tensor Compiler with Dual Awareness [8.381744079783278]
我々は,テンソルプログラムの最適化を階層的に向上させるハードウェア/ソフトウェア共同設計の原則に従い,$textbfPruner$を提案する。
Prunerは2つの主要なコンポーネントで構成されている。静的アナライザ(textbfPSA$)とパターン対応コストモデル(textbfPa$)である。
論文 参考訳(メタデータ) (2024-02-04T06:11:12Z) - 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) - When Do Program-of-Thoughts Work for Reasoning? [51.2699797837818]
本稿では,コードと推論能力の相関性を測定するために,複雑性に富んだ推論スコア(CIRS)を提案する。
具体的には、抽象構文木を用いて構造情報をエンコードし、論理的複雑性を計算する。
コードはhttps://github.com/zjunlp/EasyInstructのEasyInstructフレームワークに統合される。
論文 参考訳(メタデータ) (2023-08-29T17:22:39Z) - 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) - Online Machine Learning Techniques for Coq: A Comparison [2.9412498294532856]
我々は,Coq証明アシスタントにおける戦術学習と証明のためのオンライン機械学習技術の比較を行った。
この仕事は、ユーザーによって書かれた証明から新しい証明を合成するCoq用のプラグインであるTacticianをベースにしています。
論文 参考訳(メタデータ) (2021-04-12T05:12:35Z) - PalmTree: Learning an Assembly Language Model for Instruction Embedding [8.74990895782223]
汎用命令埋め込み生成のためのアセンブリ言語モデルであるPalmTreeの事前トレーニングを提案する。
PalmTreeは固有のメトリクスに対して最高のパフォーマンスを持ち、下流タスクの他の命令埋め込みスキームよりも優れています。
論文 参考訳(メタデータ) (2021-01-21T22:30:01Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。