論文の概要: CoqPilot, a plugin for LLM-based generation of proofs

• arxiv url: http://arxiv.org/abs/2410.19605v1
• Date: Fri, 25 Oct 2024 14:57:29 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-10-28 13:38:02.615898
• Title: CoqPilot, a plugin for LLM-based generation of proofs
• Title（参考訳）: CoqPilot - LLMベースの証明生成用プラグイン
• Authors: Andrei Kozyrev, Gleb Solovev, Nikita Khramov, Anton Podkopaev,
• Abstract要約: CoqPilotは、Coq証明の記述を自動化するために設計されたVS Codeエクステンションである。 プラグインは、Coqファイルの許容戦術でマークされた証明の一部を収集する。 LLMと非機械学習法を組み合わせて、ホールの証明候補を生成する。
• 参考スコア（独自算出の注目度）: 0.0
• License:
• Abstract: We present CoqPilot, a VS Code extension designed to help automate writing of Coq proofs. The plugin collects the parts of proofs marked with the admit tactic in a Coq file, i.e., proof holes, and combines LLMs along with non-machine-learning methods to generate proof candidates for the holes. Then, CoqPilot checks if each proof candidate solves the given subgoal and, if successful, replaces the hole with it. The focus of CoqPilot is twofold. Firstly, we want to allow users to seamlessly combine multiple Coq generation approaches and provide a zero-setup experience for our tool. Secondly, we want to deliver a platform for LLM-based experiments on Coq proof generation. We developed a benchmarking system for Coq generation methods, available in the plugin, and conducted an experiment using it, showcasing the framework's possibilities. Demo of CoqPilot is available at: https://youtu.be/oB1Lx-So9Lo. Code at: https://github.com/JetBrains-Research/coqpilot
• Abstract（参考訳）: 私たちは、Coq証明の記述を自動化するために設計されたVS CodeエクステンションであるCoqPilotを紹介します。 このプラグインは、Coqファイルの許容戦術でマークされた証明の部分、すなわち証明ホールを収集し、LLMと非機械学習法を組み合わせて、穴の証明候補を生成する。 次に、CoqPilotは、各証明候補が与えられた部分ゴールを解くかどうかを確認し、成功すれば、ホールをそれで置き換える。 CoqPilotの焦点は2つある。 まず、ユーザは複数のCoq生成アプローチをシームレスに組み合わせて、ツールにゼロセットアップエクスペリエンスを提供したいと思っています。 第二に、私たちはLLMベースの実証生成実験のためのプラットフォームを提供したいと思っています。 我々は,プラグインで利用可能なCoq生成手法のベンチマークシステムを開発し,それを用いた実験を行い,フレームワークの可能性を示した。 CoqPilotのデモは、https://youtu.be/oB1Lx-So9Loで公開されている。 Code at: https://github.com/JetBrains-Research/coqpilot

関連論文リスト

• Benchmarking Uncertainty Quantification Methods for Large Language Models with LM-Polygraph [83.90988015005934]
  不確実性定量化(英: Uncertainty Quantification、UQ)は、機械学習(ML)アプリケーションにおいて重要なコンポーネントである。 最新のUQベースラインの集合を実装した新しいベンチマークを導入する。 我々は、9つのタスクにわたるUQと正規化技術に関する大規模な実証的研究を行い、最も有望なアプローチを特定した。
  論文  参考訳（メタデータ） (2024-06-21T20:06:31Z)
• CoqPyt: Proof Navigation in Python in the Era of LLMs [5.029445580644576]
  本稿では,Coq証明アシスタントと対話するPythonツールであるCoqPytについて述べる。 CoqPytは、リッチな前提データの抽出など、新しい機能を提供することで、他のCoq関連のツールを改善している。
  論文  参考訳（メタデータ） (2024-05-07T12:50:28Z)
• Towards Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
  大規模な言語モデルでリーン推論を実行するためのフレームワークであるLean Copilotを紹介します。 証明手順を提案し、中間的な証明目標を完了し、関連する前提を選択するためのツールを構築します。 実験により, 提案手法の有効性を実証し, 提案手法の有効性を検証した。
  論文  参考訳（メタデータ） (2024-04-18T22:54:08Z)
• 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)
• Towards Automatic Transformations of Coq Proof Scripts [0.0]
  後続スクリプト変換を行うためのフレームワークを提案する。 これらの変換は、証明が完了すると、自動化された後処理ステップとして適用される。 当社のツールは,GeoCoqライブラリなど,さまざまなCoq証明スクリプトに適用しています。
  論文  参考訳（メタデータ） (2024-01-22T12:48:34Z)
• Merging Generated and Retrieved Knowledge for Open-Domain QA [72.42262579925911]
  COMBOは、より良いオープンドメインQAフレームワークのための互換性指向の知識の融合である。 COMBOは4つのテスト済みオープンドメインQAベンチマークのうち3つで競合ベースラインを上回っていることを示す。
  論文  参考訳（メタデータ） (2023-10-22T19:37:06Z)
• A Practical Toolkit for Multilingual Question and Answer Generation [79.31199020420827]
  我々は,マルチ言語QAGのオンラインサービスであるAutoQGと,モデル微調整,生成,評価のためのオールインワンPythonパッケージであるlmqgを紹介した。 また、事前訓練されたエンコーダ-デコーダ言語モデルのいくつかの変種を微調整した8言語でQAGモデルをリリースしています。
  論文  参考訳（メタデータ） (2023-05-27T08:42:37Z)
• 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)
• Multi-hop Question Generation with Graph Convolutional Network [58.31752179830959]
  マルチホップ質問生成(Multi-hop Question Generation, QG)は,異なる段落から散在する複数の証拠を集約・推論することで,回答に関連する質問を生成することを目的とする。 複数のホップでコンテキストエンコーディングを行うMulQG(Multi-Hop volution Fusion Network for Question Generation)を提案する。 提案モデルでは,高い完全性を有する流動的な質問を生成することができ,マルチホップ評価において,最強のベースラインを20.8%向上させることができる。
  論文  参考訳（メタデータ） (2020-10-19T06:15:36Z)
• Learning to Format Coq Code Using Language Models [35.21093297227429]
  Coqコードは、異なる人々やチームによって異なる方法で書かれる傾向があります。 特に、経験の浅いユーザでさえ、標準ライブラリと普通のLtacを使って、頂点を区別することができる。 Coqの美容整形器のようなルールベースのフォーマッターは柔軟性が限られており、所望の規約のごく一部しか取得できない。
  論文  参考訳（メタデータ） (2020-06-18T14:46:15Z)
• Prolog Technology Reinforcement Learning Prover [0.6445605125467572]
  ツールキットの中核はコンパクトで容易にPrologベースの自動定理証明であるplCoPである。 plCoPは、LeadCoP Prologの実装に基づいて構築されており、rlCoPシステムで実施された学習誘導のMonte-Carlo Tree Searchを追加している。 その他のコンポーネントには、plCoPとマシン学習者のPythonインターフェース、plCoP証明の有効性を検証する外部証明チェッカーなどがある。
  論文  参考訳（メタデータ） (2020-04-15T10:52:04Z)

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

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