paperbot · PL 论文追踪

全部论文 待读 收藏

P0 CoqPilot, a plugin for LLM-based generation of proofs

CoqPilot：基于 LLM 生成证明的插件
ASE Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering2024匹配度 8/10 · 该论文利用 LLM 与传统方法结合来自动填充 Coq 证明空洞，属于“AI→PL：利用 LLM/Agent 改进形式化验证”的方向，与用户关注点直接相关；同时提供 VS Code 插件和基准测试平台，契合对工程实现与 benchmark 的关注。引用 2 inbox
Andrei Kozyrev, Gleb Solovev, Nikita Khramov, Anton Podkopaev
机器学习与程序语言编程环境与开发者工具
crossref: 2026-09-12

AI 速览

一句话：提出 CoqPilot：一个 VS Code 插件，结合 LLM 与传统方法自动填补 Coq 证明空洞，并提供基准测试平台。

CoqPilot 旨在自动化 Coq 证明写作。该插件收集 Coq 文件中由 admit 标记的证明空洞，结合 LLM 与非机器学习方法为每个空洞生成候选证明，并交由 Coq 检查；若候选证明成功求解子目标，则替换原有空洞。CoqPilot 强调无缝组合多种 Coq 证明生成方法、提供零配置使用体验，并作为 LLM 在 Coq 证明生成上的实验平台。作者还实现了内置的基准测试系统，并开展实验展示框架能力，同时提供演示视频与开源代码。

问题
如何帮助用户自动化地编写 Coq 证明，尤其是填补文件中以 admit 标记的证明空洞，并集成多种证明生成方法。
方法
CoqPilot 作为 VS Code 扩展收集证明空洞，联合 LLM 与非机器学习方法生成候选证明，由 Coq 验证成功则自动替换空洞；同时提供多方法组合、零配置体验与基准测试平台。
评估
作者实现 CoqPilot 插件及其内置基准测试系统，并开展实验展示该框架进行 Coq 证明生成实验的能力；工具提供演示视频和开源代码。
原文摘要（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

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot8393,
  title = {CoqPilot, a plugin for LLM-based generation of proofs},
  author = {Andrei Kozyrev and Gleb Solovev and Nikita Khramov and Anton Podkopaev},
  booktitle = {ASE},
  year = {2024},
  doi = {10.1145/3691620.3695357}
}