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

在形式定理证明领域，Coq证明助手以其严谨的方法验证数学断言和软件正确性而脱颖而出。尽管人工智能和机器学习取得了进展，但Coq语法和语义的专业性为大语言模型(LLMs)提出了独特的挑战。为了解决这个问题，我们提出了一个全面的数据集，专门设计用于提高LLMs在解释和生成Coq代码方面的熟练程度。这个数据集来源于超过10,000个Coq源文件的集合，包括各种命题、证明和定义，丰富的元数据包括源引用和许可信息。我们的主要目的是促进开发能够生成语法正确和语义有意义的Coq构造的LLMs，从而推进自动定理证明的前沿。对这个数据集的初步实验展示了它的巨大潜力；在这些数据上训练的模型在Coq代码生成方面表现出更高的准确性。值得注意的是，一个特定的实验揭示了一个经过精细调整的LLM能够为一个基本引理生成141个有效的证明，凸显了这个数据集在促进多样化和有效的证明策略发现方面的实用性。本文讨论了数据集的组成、创建背后的方法以及我们的发现对形式验证中机器学习未来的影响。该数据集可用于进一步的研究和探索：https://huggingface.co/datasets/florath/coq-facts-props-proofs-gen0-v1

如何提高大型语言模型在Coq代码生成方面的效率和准确性？

创建一个专门针对Coq代码的数据集，以提高大型语言模型在Coq代码生成方面的能力。

论文提出了一个基于Coq源代码的数据集，包含了广泛的命题、证明和定义，并且附加了元数据。实验结果表明，使用该数据集训练的模型在Coq代码生成方面表现出更高的准确性。该数据集已经开源并可供进一步研究和探索。

最近的相关研究包括：1）使用机器学习技术进行定理证明的研究；2）使用深度学习技术对数学公式进行分类和识别的研究。