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

要約

形式的定理証明の領域では、Coq 証明アシスタントは、数学的主張とソフトウェアの正しさを検証するための厳密なアプローチで際立っています。
人工知能と機械学習の進歩にもかかわらず、Coq 構文とセマンティクスの特殊な性質は、大規模言語モデル (LLM) に特有の課題を引き起こします。
このギャップに対処するために、我々は、Coq コードの解釈と生成における LLM の習熟度を高めるために特別に設計された包括的なデータセットを提示します。
このデータセットは、10,000 を超える Coq ソース ファイルのコレクションから派生しており、ソース参照やライセンス情報などのメタデータで強化された、幅広い命題、証明、定義を網羅しています。
私たちの主な目的は、構文的に正しく、意味的に意味のある Coq 構造を生成できる LLM の開発を促進し、それによって自動化された定理証明の最前線を前進させることです。
このデータセットを使用した初期実験では、その重要な可能性が実証されました。
このデータでトレーニングされたモデルは、Coq コード生成の精度が向上しました。
特に、特定の実験では、微調整された LLM が基本的な補題に対して 141 の有効な証明を生成できることが明らかになり、多様で有効な証明戦略の発見を容易にするデータセットの有用性が強調されました。
このペーパーでは、データセットの構成、その作成の背後にある方法論、形式検証における機械学習の将来に対する我々の発見の意味について説明します。
データセットは、さらなる研究と探索のためにアクセスできます: https://huggingface.co/datasets/florath/coq-facts-props-proofs-gen0-v1

要約(オリジナル)

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

arxiv情報

提供元, 利用サービス

arxiv.jp, Google