論文の概要: Towards Automatic Transformations of Coq Proof Scripts

• arxiv url: http://arxiv.org/abs/2401.11897v1
• Date: Mon, 22 Jan 2024 12:48:34 GMT
• ステータス: 処理完了
• システム内更新日: 2024-01-23 14:10:59.916690
• Title: Towards Automatic Transformations of Coq Proof Scripts
• Title（参考訳）: Coq証明スクリプトの自動変換に向けて
• Authors: Nicolas Magaud (Lab. ICube CNRS Universit\'e de Strasbourg, France)
• Abstract要約: 後続スクリプト変換を行うためのフレームワークを提案する。 これらの変換は、証明が完了すると、自動化された後処理ステップとして適用される。 当社のツールは,GeoCoqライブラリなど,さまざまなCoq証明スクリプトに適用しています。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Proof assistants like Coq are increasingly popular to help mathematicians carry out proofs of the results they conjecture. However, formal proofs remain highly technical and are especially difficult to reuse. In this paper, we present a framework to carry out a posteriori script transformations. These transformations are meant to be applied as an automated post-processing step, once the proof has been completed. As an example, we present a transformation which takes an arbitrary large proof script and produces an equivalent single-line proof script, which can be executed by Coq in one single step. Other applications, such as fully expanding a proof script (for debugging purposes), removing all named hypotheses, etc. could be developed within this framework. We apply our tool to various Coq proof scripts, including some from the GeoCoq library.
• Abstract（参考訳）: coqのような証明アシスタントは、数学者が予想した結果の証明を行うのを助けるためにますます人気がある。 しかし、形式的な証明は高度に技術的であり、特に再利用が難しい。 本稿では,後述のスクリプト変換を行うためのフレームワークを提案する。 これらの変換は、証明が完了すると、自動化された後処理ステップとして適用される。 一例として、任意の大きな証明スクリプトを取り込み、これに相当する1行の証明スクリプトを生成する変換をCoqが1ステップで実行可能にする。 証明スクリプトを完全に拡張したり(デバッグ目的で)、名前付き仮説をすべて削除したりといった他のアプリケーションもこのフレームワーク内で開発できる。 当社のツールは,GeoCoqライブラリなど,さまざまなCoq証明スクリプトに適用しています。

関連論文リスト

• Cobblestone: Iterative Automation for Formal Verification [11.445689801392657]
  Coqのような証明アシスタントを用いた形式的検証は、ソフトウェア品質を改善する効果的な方法であるが、高価である。 最近の研究では、機械学習を使って証明を自動的に合成し、検証の労力を削減しているが、これらのツールは、望まれるソフトウェアプロパティのほんの一部しか証明できない。 我々は, 証明合成における部分的な進歩を生かして, 技術状況を改善する新しい証明合成手法であるCobblestoneを紹介した。
  論文  参考訳（メタデータ） (2024-10-25T19:25:00Z)
• MathGAP: Out-of-Distribution Evaluation on Problems with Arbitrarily Complex Proofs [80.96119560172224]
  大規模言語モデル(LLM)は、高い精度で算術語問題を解くことができるが、訓練された言語よりも複雑な問題にどのように一般化するかは、ほとんど分かっていない。 本研究では、任意に複雑な算術証明問題に対する LLM の評価フレームワーク、MathGAP を提案する。
  論文  参考訳（メタデータ） (2024-10-17T12:48:14Z)
• CoqPyt: Proof Navigation in Python in the Era of LLMs [5.029445580644576]
  本稿では,Coq証明アシスタントと対話するPythonツールであるCoqPytについて述べる。 CoqPytは、リッチな前提データの抽出など、新しい機能を提供することで、他のCoq関連のツールを改善している。
  論文  参考訳（メタデータ） (2024-05-07T12:50:28Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Baldur: Whole-Proof Generation and Repair with Large Language Models [8.100054850290507]
  我々は、自然言語のテキストとコードに基づいて訓練され、証明について微調整された大きな言語モデルを使用して、一度に定理のすべての証明を生成する。 我々は、この証明生成モデルと微調整の補修モデルを組み合わせて、生成した証明を修復し、さらに証明力を増強する。 本手法をプロトタイプであるBaldurで評価し、6,336 Isabelle/HOL定理とその証明のベンチマークで評価する。
  論文  参考訳（メタデータ） (2023-03-08T22:00:15Z)
• 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)
• multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning [73.09791959325204]
  我々は、自然言語の事実と規則の形で明示的な知識を推論することを目的としている言語形式推論の一種に焦点を当てる。 PRoverという名前の最近の研究は、質問に答え、答えを説明する証明グラフを生成することによって、そのような推論を行う。 本研究では,自然言語規則ベースの推論のために複数の証明グラフを生成するという,新たな課題に対処する。
  論文  参考訳（メタデータ） (2021-06-02T17:58:35Z)
• Zero-shot Fact Verification by Claim Generation [85.27523983027471]
  我々は,堅牢な事実検証モデルをトレーニングするフレームワークであるQACGを開発した。 われわれは自動的に生成されたクレームを使って、Wikipediaのエビデンスからサポートしたり、反論したり、検証したりできる。 ゼロショットシナリオでは、QACGはRoBERTaモデルのF1を50%から77%に改善し、パフォーマンスは2K以上の手作業による例に相当する。
  論文  参考訳（メタデータ） (2021-05-31T03:13:52Z)
• 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)

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

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