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

翻译：本文介绍CoqPilot，一款旨在辅助自动化编写Coq证明的VS Code扩展插件。该插件会收集Coq文件中使用admit策略标记的证明片段（即证明空缺），并综合运用大语言模型与非机器学习方法为这些空缺生成候选证明。随后，CoqPilot会验证每个候选证明是否能解决给定的子目标，若验证成功，则用该证明替换原空缺。CoqPilot的设计聚焦于两个核心目标：其一，使用户能够无缝整合多种Coq证明生成方法，并为工具提供零配置体验；其二，构建一个基于大语言模型的Coq证明生成实验平台。我们在插件中开发了针对Coq生成方法的基准测试系统，并利用该系统进行了实验，展示了该框架的应用潜力。CoqPilot演示视频见：https://youtu.be/oB1Lx-So9Lo，代码仓库见：https://github.com/JetBrains-Research/coqpilot。