CoqPilot：基于 LLM 的证明生成插件

Andrei Kozyrev; Gleb Solovev; Nikita Khramov; Anton Podkopaev

doi:10.1145/3691620.3695357

CoqPilot：基于 LLM 的证明生成插件

软件工程 2024-10-28 v1 人工智能计算机科学中的逻辑

作者: Andrei Kozyrev , Gleb Solovev , Nikita Khramov , Anton Podkopaev

在 arXiv 上查看 ↗ PDF ↗ DOI ↗

摘要

我们提出了 CoqPilot，一个旨在帮助自动化编写 Coq 证明的 VS Code 扩展。该插件收集 Coq 文件中使用 admit 策略标记的证明部分，即证明空洞，并结合 LLM 与非机器学习方法为这些空洞生成证明候选。随后，CoqPilot 检查每个证明候选是否能解决给定的子目标，若成功，则用其替换该空洞。CoqPilot 的重点有两方面。首先，我们希望允许用户无缝结合多种 Coq 生成方法，并为我们的工具提供零配置体验。其次，我们希望提供一个基于 LLM 的 Coq 证明生成实验平台。我们开发了一个用于 Coq 生成方法的基准测试系统，可在该插件中使用，并利用其进行了一项实验，展示了该框架的潜力。CoqPilot 的演示参见：https://youtu.be/oB1Lx-So9Lo。代码参见：https://github.com/JetBrains-Research/coqpilot

关键词

Coq 证明生成大型语言模型 VS Code 扩展自动定理证明证明空洞

引用

@article{arxiv.2410.19605,
  title  = {CoqPilot, a plugin for LLM-based generation of proofs},
  author = {Andrei Kozyrev and Gleb Solovev and Nikita Khramov and Anton Podkopaev},
  journal= {arXiv preprint arXiv:2410.19605},
  year   = {2024}
}

备注

Published in the proceedings of the ASE'24 Tool Demonstrations Track

CoqPilot：基于 LLM 的证明生成插件

摘要

关键词

引用

备注

相关论文