CoqPyt: Proof Navigation in Python in the Era of LLMs
Pedro Carrott, Nuno Saavedra, Kyle Thompson, Sorin Lerner, João F. Ferreira, Emily First
TL;DR
The paper tackles the high cost of formal verification by enabling data-rich interaction with Coq for neural theorem proving. It introduces CoqPyt, a Python tool built on Coq LSP that collects per-step context and supports arbitrary file and proof modifications to assist proof search and repair. The authors demonstrate CoqPyt's capabilities on contemporary Coq versions and validate its utility for data collection and evaluation in neural approaches, including a CompCert case study. The work provides an open-source platform to seed retrieval-augmented LLMs and other learning-based proof tools with richer Coq-context data, potentially accelerating Coq-based verification research.
Abstract
Proof assistants enable users to develop machine-checked proofs regarding software-related properties. Unfortunately, the interactive nature of these proof assistants imposes most of the proof burden on the user, making formal verification a complex, and time-consuming endeavor. Recent automation techniques based on neural methods address this issue, but require good programmatic support for collecting data and interacting with proof assistants. This paper presents CoqPyt, a Python tool for interacting with the Coq proof assistant. CoqPyt improves on other Coq-related tools by providing novel features, such as the extraction of rich premise data. We expect our work to aid development of tools and techniques, especially LLM-based, designed for proof synthesis and repair. A video describing and demonstrating CoqPyt is available at: https://youtu.be/fk74o0rePM8.