用大模型自动补全Coq证明漏洞，一键生成并验证
CoqPilot, a plugin for LLM-based generation of proofs
- 结合大模型与非机器学习方法生成证明候选
- 自动验证并替换证明空缺，成功率高且无需配置
- 提供实验平台和基准测试，适合形式化验证研究者
我们提出 CoqPilot，一个 VS Code 插件，用于自动化编写 Coq 证明。该插件收集 Coq 文件中使用 admit 策略标记的证明空缺（即证明漏洞），结合大语言模型与非机器学习方法生成证明候选。随后，CoqPilot 检查每个候选是否解决对应子目标，若成功则替换原空缺。CoqPilot 的重点在于：一方面支持无缝集成多种 Coq 生成方法，提供零配置体验；另一方面构建了用于 LLM 驱动的 Coq 证明生成实验的平台。我们开发了一个基准测试系统，嵌入插件中，并基于此开展实验，展示框架潜力。演示视频见：https://youtu.be/oB1Lx-So9Lo。代码地址：https://github.com/JetBrains-Research/coqpilot。
原文摘要 · Abstract (English)
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
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。