論文の概要: Tactic Learning and Proving for the Coq Proof Assistant
- arxiv url: http://arxiv.org/abs/2003.09140v1
- Date: Fri, 20 Mar 2020 08:22:30 GMT
- ステータス: 処理完了
- システム内更新日: 2022-12-21 22:50:44.561511
- Title: Tactic Learning and Proving for the Coq Proof Assistant
- Title(参考訳): coq証明アシスタントのための戦術学習と証明
- Authors: Lasse Blaauwbroek, Josef Urban, and Herman Geuvers
- Abstract要約: 我々のシステムは適切な戦術を予測し、戦術スクリプトの形で証明を見つける。
システムの性能は、Coq Standard Libraryで評価される。
CoqHammerシステムと組み合わせると、この2つのシステムは図書館の補題の56.7%を証明している。
- 参考スコア(独自算出の注目度): 0.5735035463793007
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We present a system that utilizes machine learning for tactic proof search in
the Coq Proof Assistant. In a similar vein as the TacticToe project for HOL4,
our system predicts appropriate tactics and finds proofs in the form of tactic
scripts. To do this, it learns from previous tactic scripts and how they are
applied to proof states. The performance of the system is evaluated on the Coq
Standard Library. Currently, our predictor can identify the correct tactic to
be applied to a proof state 23.4% of the time. Our proof searcher can fully
automatically prove 39.3% of the lemmas. When combined with the CoqHammer
system, the two systems together prove 56.7% of the library's lemmas.
- Abstract(参考訳): 本稿では,Coq Proof Assistantの戦術的証明探索に機械学習を利用するシステムを提案する。
HOL4のTacticToeプロジェクトと同様、我々のシステムは適切な戦術を予測し、戦術スクリプトの形で証明を見つける。
これを実現するために、従来の戦術スクリプトから学習し、証明状態に適用する方法を学ぶ。
システムの性能は、Coq Standard Libraryで評価される。
現在、我々の予測者は、証明状態に適用する正しい戦術を23.4%の確率で特定することができる。
我々の証明探索者は 39.3%の補題を 自動的に証明できる
CoqHammerシステムと組み合わせると、2つのシステムは図書館の補題の56.7%を証明している。
関連論文リスト
- MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [88.72298746872396]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳(メタデータ) (2024-02-14T05:57:58Z) - Towards Automatic Transformations of Coq Proof Scripts [0.0]
後続スクリプト変換を行うためのフレームワークを提案する。
これらの変換は、証明が完了すると、自動化された後処理ステップとして適用される。
当社のツールは,GeoCoqライブラリなど,さまざまなCoq証明スクリプトに適用しています。
論文 参考訳(メタデータ) (2024-01-22T12:48:34Z) - Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [102.00359477458029]
本稿では,ニューラル・シンボリック統合法について述べる。
LLMフリーのシンボリック・ソルバを用いて、知識を用いた熟考的推論を行う。
論文 参考訳(メタデータ) (2023-11-16T11:26:21Z) - An In-Context Learning Agent for Formal Theorem-Proving [11.433505167967983]
我々は、LeanやCoqのような環境で、形式的定理コンテキストのための即興学習エージェントを提示します。
COPRAは大規模言語モデルに対して、ステートフルなバックトラック検索から戦術的応用を提案することを何度も求めている。
我々はCompCertプロジェクトのMiniF2FベンチマークとCoqタスクセットに対するCOPRAの実装を評価した。
論文 参考訳(メタデータ) (2023-10-06T16:21:22Z) - Faithful Chain-of-Thought Reasoning [51.21714389639417]
CoT(Chain-of-Thought)は言語モデル(LM)のパフォーマンスを様々な推論タスクで向上させる。
翻訳と問題解決という2つの段階を含む推論フレームワークであるFithful CoTを提案する。
このことは、推論連鎖が最終回答の忠実な説明を提供することを保証している。
論文 参考訳(メタデータ) (2023-01-31T03:04:26Z) - Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal
Proofs [30.57062828812679]
本稿では,形式的証明スケッチに非公式な証明をマッピングするDraft, Sketch, Prove(DSP)を紹介する。
大規模言語モデルでは,形式的証明と同じ推論手順を踏襲して,構造化された形式的スケッチを作成可能であることを示す。
論文 参考訳(メタデータ) (2022-10-21T22:37:22Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳(メタデータ) (2022-05-25T02:22:30Z) - Online Machine Learning Techniques for Coq: A Comparison [2.9412498294532856]
我々は,Coq証明アシスタントにおける戦術学習と証明のためのオンライン機械学習技術の比較を行った。
この仕事は、ユーザーによって書かれた証明から新しい証明を合成するCoq用のプラグインであるTacticianをベースにしています。
論文 参考訳(メタデータ) (2021-04-12T05:12:35Z) - The Coq Proof Script Visualiser (coq-psv) [0.0]
このツールは、すべての証明ステップを視覚化できるので、教育とレビューのプロセスの両方をサポートする。
証明をハイパーテキストやマークダウン文書として視覚化する一般的な手法とは対照的に、生成されたファイルを簡単に印刷することができる。
論文 参考訳(メタデータ) (2021-01-15T08:52:31Z) - PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。
本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。
我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文 参考訳(メタデータ) (2020-10-06T15:47:53Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳(メタデータ) (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。