fm-universe/FM-alpaca

FM-Alpaca数据集是一个用于训练的数据集，它服务于一篇研究论文，该论文探讨将非正式的自然语言要求转化为可验证的正式证明。数据集包括六个形式验证相关的任务，如需求分析、证明/模型生成、证明片段生成、证明完成、证明填充以及代码到证明的转换。该数据集支持五种形式化规范语言：ACSL、TLA、Cog、Dafny和Lean4。数据集的准备工作包括从开源仓库收集形式化证明和相关配置，提取证明并进行数据质量检查，最后将证明分割成片段。

The FM-Alpaca dataset is a training dataset for a research paper that explores transforming informal natural language requirements into verifiable formal proofs. The dataset includes six formal verification-related tasks such as requirement analysis, proof/model generation, proof segment generation, proof completion, proof infilling, and code-to-proof transformation. The dataset supports five formal specification languages: ACSL, TLA, Cog, Dafny, and Lean4. The data preparation involves collecting formal proofs and related configurations from open-source repositories, extracting proofs, performing data quality checks, and finally segmenting the proofs into chunks.