論文の概要: CoqPyt: Proof Navigation in Python in the Era of LLMs

• arxiv url: http://arxiv.org/abs/2405.04282v1
• Date: Tue, 7 May 2024 12:50:28 GMT
• ステータス: 処理完了
• システム内更新日: 2024-05-08 14:10:19.052840
• Title: CoqPyt: Proof Navigation in Python in the Era of LLMs
• Title（参考訳）: CoqPyt: LLM時代のPythonでのナビゲーションの証明
• Authors: Pedro Carrott, Nuno Saavedra, Kyle Thompson, Sorin Lerner, João F. Ferreira, Emily First,
• Abstract要約: 本稿では,Coq証明アシスタントと対話するPythonツールであるCoqPytについて述べる。 CoqPytは、リッチな前提データの抽出など、新しい機能を提供することで、他のCoq関連のツールを改善している。
• 参考スコア（独自算出の注目度）: 5.029445580644576
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Proof assistants enable users to develop machine-checked proofs regarding software-related properties. Unfortunately, the interactive nature of these proof assistants imposes most of the proof burden on the user, making formal verification a complex, and time-consuming endeavor. Recent automation techniques based on neural methods address this issue, but require good programmatic support for collecting data and interacting with proof assistants. This paper presents CoqPyt, a Python tool for interacting with the Coq proof assistant. CoqPyt improves on other Coq-related tools by providing novel features, such as the extraction of rich premise data. We expect our work to aid development of tools and techniques, especially LLM-based, designed for proof synthesis and repair. A video describing and demonstrating CoqPyt is available at: https://youtu.be/fk74o0rePM8.
• Abstract（参考訳）: 証明アシスタントは、ユーザーがソフトウェア関連プロパティに関するマシンチェックされた証明を開発することを可能にする。 残念ながら、これらの証明アシスタントのインタラクティブな性質は、ユーザに対して証明の負担の大部分を課し、形式的検証を複雑で時間を要する作業にする。 ニューラルメソッドに基づく最近の自動化技術はこの問題に対処するが、データ収集や証明アシスタントとの対話に優れたプログラム的サポートが必要である。 本稿では,Coq証明アシスタントと対話するPythonツールであるCoqPytについて述べる。 CoqPytは、リッチな前提データの抽出など、新しい機能を提供することで、他のCoq関連のツールを改善している。 われわれは、証明合成と修復のために設計されたツールや技術、特にLLMベースの開発を支援することを期待している。 CoqPytを説明したビデオは、https://youtu.be/fk74o0rePM8で公開されている。

関連論文リスト

• Cobblestone: Iterative Automation for Formal Verification [11.445689801392657]
  Coqのような証明アシスタントを用いた形式的検証は、ソフトウェア品質を改善する効果的な方法であるが、高価である。 最近の研究では、機械学習を使って証明を自動的に合成し、検証の労力を削減しているが、これらのツールは、望まれるソフトウェアプロパティのほんの一部しか証明できない。 我々は, 証明合成における部分的な進歩を生かして, 技術状況を改善する新しい証明合成手法であるCobblestoneを紹介した。
  論文  参考訳（メタデータ） (2024-10-25T19:25:00Z)
• CoqPilot, a plugin for LLM-based generation of proofs [0.0]
  CoqPilotは、Coq証明の記述を自動化するために設計されたVS Codeエクステンションである。 プラグインは、Coqファイルの許容戦術でマークされた証明の一部を収集する。 LLMと非機械学習法を組み合わせて、ホールの証明候補を生成する。
  論文  参考訳（メタデータ） (2024-10-25T14:57:29Z)
• Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code [0.0]
  Coqの証明アシスタントは、数学的アサーションとソフトウェアの正確性を検証するための厳格なアプローチで際立っている。 人工知能と機械学習の進歩にもかかわらず、Coq構文と意味論の特殊性は大規模言語モデル(LLM)に固有の課題をもたらす。 このデータセットは、10,000以上のCoqソースファイルのコレクションから派生したもので、幅広い命題、証明、定義を含んでいる。
  論文  参考訳（メタデータ） (2024-03-19T10:53:40Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  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)
• Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
  Program-Guided Fact-Checking (ProgramFC)は、複雑なクレームを単純なサブタスクに分解する新しいファクトチェックモデルである。 まず,大規模言語モデルの文脈内学習能力を活用して推論プログラムを生成する。 我々は,各サブタスクを対応するサブタスクハンドラに委譲することでプログラムを実行する。
  論文  参考訳（メタデータ） (2023-05-22T06:11:15Z)
• Open-domain Question Answering via Chain of Reasoning over Heterogeneous Knowledge [82.5582220249183]
  異種知識ソース間のシングル/マルチホップ質問に応答する新しいオープンドメイン質問応答(ODQA)フレームワークを提案する。 分離された証拠を収集するためにレトリバーにのみ依存する従来の方法とは異なり、我々の仲介者は検索された集合に対する推論の連鎖を実行する。 本システムは,2つのODQAデータセットであるOTT-QAとNQに対して,Wikipediaの表や節に対する競合性能を実現する。
  論文  参考訳（メタデータ） (2022-10-22T03:21:32Z)
• Effidit: Your AI Writing Assistant [60.588370965898534]
  Effiditは、人工知能(AI)技術を使用して、ユーザーが高品質なテキストをより効率的に書けるようにするためのデジタルライティングアシスタントである。 Effiditでは、テキスト補完、エラーチェック、テキスト研磨、キーワード・トゥ・センテンス(K2S)、クラウド・インプット・メソッド(クラウドIME)の5つのカテゴリで機能を提供することで、筆記アシスタントの能力を大幅に拡大する。
  論文  参考訳（メタデータ） (2022-08-03T02:24:45Z)
• 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)
• Understanding Unnatural Questions Improves Reasoning over Text [54.235828149899625]
  生テキストに対する複雑な質問応答(CQA)は難しい課題である。 効果的なCQAモデルを学ぶには、大量の人間が注釈付けしたデータが必要である。 我々は、自然の人間生成の質問を非自然の機械生成の質問に投影することで、高品質なプログラマ(パーザ)を学ぶという課題に対処する。
  論文  参考訳（メタデータ） (2020-10-19T10:22:16Z)

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

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