CoqPilot, a plugin for LLM-based generation of proofs

要約

Coq 証明の作成を自動化するために設計された VS Code 拡張機能である CoqPilot を紹介します。
このプラグインは、Coq ファイル内のアドミット戦術でマークされた証明の部分、つまりプルーフ ホールを収集し、LLM と非機械学習手法を組み合わせて、ホールの証明候補を生成します。
次に、CoqPilot は、各証明候補が指定されたサブゴールを解決するかどうかを確認し、成功した場合はそのホールをそのサブゴールで置き換えます。
CoqPilot の焦点は 2 つあります。
まず、ユーザーが複数の Coq 生成アプローチをシームレスに組み合わせて、ツールにゼロセットアップ エクスペリエンスを提供できるようにしたいと考えています。
次に、Coq 証明生成に関する LLM ベースの実験のためのプラットフォームを提供したいと考えています。
私たちは、プラグインで利用可能な Coq 生成メソッドのベンチマーク システムを開発し、それを使用して実験を実施し、フレームワークの可能性を示しました。
CoqPilot のデモは https://youtu.be/oB1Lx-So9Lo でご覧いただけます。
コード: https://github.com/JetBrains-Research/coqpilot

要約(オリジナル)

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

arxiv情報

提供元, 利用サービス

arxiv.jp, Google