CoqPyt: Proof Navigation in Python in the Era of LLMs
<|reference_start|>CoqPyt: Proof Navigation in Python in the Era of LLMs: 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.<|reference_end|>
@article{carrott2024coqpyt:,
    title={CoqPyt: Proof Navigation in Python in the Era of LLMs},
    author={Pedro Carrott, Nuno Saavedra, Kyle Thompson, Sorin Lerner, Jo~ao F.
  Ferreira, Emily First},
    journal={arXiv preprint arXiv:2405.04282},
    year={2024},
    doi={10.1145/3663529.3663814},
    archivePrefix={arXiv},
    eprint={2405.04282},
    primaryClass={cs.SE}
}