Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code
Andreas Florath
TL;DR
The paper addresses the challenge of applying LLMs to Coq formal proofs by constructing a large, license-aware Coq-focused dataset drawn from 10,000+ sources. It details the dataset coq-facts-props-proofs, its preprocessing pipeline, and comprehensive statistics, demonstrating how fine-tuning a base LLM yields substantial gains in generating Coq-specified proofs, including 141 valid proofs for a basic lemma. The work highlights the potential for autonomous proof generation and the creation of diverse proof strategies, supported by careful licensing and provenance management. Overall, the dataset enables more reliable Coq code generation and paves the way for automated formal verification tools and Coq-based AI agents.
Abstract
In the realm of formal theorem proving, the Coq proof assistant stands out for its rigorous approach to verifying mathematical assertions and software correctness. Despite the advances in artificial intelligence and machine learning, the specialized nature of Coq syntax and semantics poses unique challenges for Large Language Models (LLMs). Addressing this gap, we present a comprehensive dataset specifically designed to enhance LLMs' proficiency in interpreting and generating Coq code. This dataset, derived from a collection of over 10,000 Coq source files, encompasses a wide array of propositions, proofs, and definitions, enriched with metadata including source references and licensing information. Our primary aim is to facilitate the development of LLMs capable of generating syntactically correct and semantically meaningful Coq constructs, thereby advancing the frontier of automated theorem proving. Initial experiments with this dataset have showcased its significant potential; models trained on this data exhibited enhanced accuracy in Coq code generation. Notably, a particular experiment revealed that a fine-tuned LLM was capable of generating 141 valid proofs for a basic lemma, highlighting the dataset's utility in facilitating the discovery of diverse and valid proof strategies. This paper discusses the dataset's composition, the methodology behind its creation, and the implications of our findings for the future of machine learning in formal verification. The dataset is accessible for further research and exploration: https://huggingface.co/datasets/florath/coq-facts-props-proofs-gen0-v1