CoqPyt: Proof Navigation in Python in the Era of LLMs

Pedro Carrott, Nuno Saavedra, Robert Thompson, Sorin Lerner, João F. Ferreira, Emily First
April 2024
Code

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/x4fGkZDxOxo.

Type
Conference paper
Publication
In International Conference on the Foundations of Software Engineering, 2024, Demonstrations Track
Ranking
CORE A* conference
Avatar
Computer Scientist

My research interests include software reliability, software verification, and formal methods applied to software engineering. I am also interested in interactive storytelling. For more details, see some of my projects or my selected (or recent) publications. More posts are available in my blog. Follow me on Twitter or add me on LinkedIn.