Fugu-MT 論文翻訳(概要): Tactic Learning and Proving for the Coq Proof Assistant

論文の概要: 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%を証明している。

関連論文リスト

Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
論文参考訳（メタデータ） (2024-11-04T05:57:40Z)
QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning [8.116854714039452]
QEDCartographerは、教師付きと強化学習を組み合わせた自動証明合成ツールである。オープンソースCoqプロジェクトの68.5K定理のCoqGymベンチマークを用いて,QEDCartographerを評価した。本研究は,強化学習が証明合成ツールの探索機構を改善するための実りある研究方向であることを実証する。
論文参考訳（メタデータ） (2024-08-17T16:06:14Z)
Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文参考訳（メタデータ） (2024-07-14T01:43:07Z)
CoqPyt: Proof Navigation in Python in the Era of LLMs [5.029445580644576]
本稿では,Coq証明アシスタントと対話するPythonツールであるCoqPytについて述べる。 CoqPytは、リッチな前提データの抽出など、新しい機能を提供することで、他のCoq関連のツールを改善している。
論文参考訳（メタデータ） (2024-05-07T12:50:28Z)
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving [41.23045212775232]
探索経路の失敗から学習する訓練モデルの利点を実証する。既存のオープンソース定理証明データセットにそのような試行錯誤データが欠如しているにもかかわらず、直観論的命題論理定理のデータセットをキュレートする。比較的短いトライアル・アンド・エラー情報(TrialMaster)で訓練されたモデルと、正しい経路でのみ訓練されたモデルを比較し、前者が低いトライアル探索でより目に見えない定理を解くことを発見した。
論文参考訳（メタデータ） (2024-04-10T23:01:45Z)
MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文参考訳（メタデータ） (2024-02-14T05:57:58Z)
Progressive-Hint Prompting Improves Reasoning in Large Language Models [63.98629132836499]
本稿では,プログレッシブ・ヒント・プロンプト(PHP)と呼ばれる新しいプロンプト手法を提案する。事前に生成された回答をヒントとして使用することで、ユーザとLLM(Large Language Models)間の自動多元的対話を可能にする。我々は7つのベンチマークで広範囲かつ包括的な実験を行った。その結果、PHPは高い効率を保ちながら精度を大幅に向上することが示された。
論文参考訳（メタデータ） (2023-04-19T16:29:48Z)
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)
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)

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