Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code

TL;DR

This paper introduces a large, comprehensive Coq dataset to improve AI models' ability to generate correct and meaningful Coq code, advancing automated theorem proving.

Contribution

The creation of a detailed Coq dataset from over 10,000 files to enhance LLM training for formal theorem proving tasks.

Findings

Models trained on the dataset showed improved Coq code generation accuracy.

A fine-tuned LLM generated 141 valid proofs for a basic lemma.

The dataset facilitates the discovery of diverse proof strategies.

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