microsoft/FStarDataSet-V2

--- license: cdla-permissive-2.0 task_categories: - text-generation - text2text-generation - other tags: - code - fstar - popai pretty_name: PoPAI-FStarDataSet-V2 size_categories: - 10K<n<100K language: - code - fst --- This dataset is the Version 2.0 of [`microsoft/FStarDataSet`](https://huggingface.co/datasets/microsoft/FStarDataSet). ## Primary-Objective This dataset's primary objective is to train and evaluate Proof-oriented Programming with AI (PoPAI, in short). Given a specification of a program and proof in F*, the objective of a AI model is to synthesize the implemantation (see [below](#usage) for details about the usage of this dataset, including the input and output). ## Data Format Each of the examples in this dataset are organized as dictionaries with the following schema ```json { "file_name": <str: Name of the file>, "name": <str: name of the example, can be used to uniquely identify the example>, "original_source_type": <str: actual source type, to be used for type checking>, "source_type": <str: modified source type, to be used to formulate prompt>, "source_definition": <str: target definition>, "source": <dict: contains metadata about the source of this example, including project_name, git url, git sha, etc.>, "source_range": <dict: metadata containing start and end lines and columns of this definition in the source file>, "file_context": <str: extracted file context upto the point of current definition>, "dependencies": <dict: build dependencies for this file>, "opens_and_abbrevs": <list[dict]: List of opened modules and abbreviated modules in the file, necessary for evaluation.>, "vconfig": <dict: SMT solver flags for this definition>, "interleaved": <bool: whether this definition is interleaved from the interface file>, "verbose_type": <str: the verbose type of this definition as resolved by the type checker>, "effect": <str: effect>, "effect_flags": <list[str]: any effect flags>, "mutual_with": <list: if this definition is mutually recursive with another, list of those names>, "ideal_premises": <list[str]: Other definitions that are used in the ground truth definition>, "proof_features": <list[str]>, "is_simple_lemma": <bool/null>, "is_div": <bool: if this definition has the divergent effect>, "is_proof": <bool>, "is_simply_typed": <bool>, "is_type": <bool/null>, "partial_definition": <str>, "completed_definiton": <str>, "isa_cross_project_example": <bool: if this example belongs to the cross-project evaluation set> } ``` # Usage To use this dataset with [`datasets`](https://pypi.org/project/datasets/), ```python from datasets import load_dataset data = load_dataset("microsoft/FStarDataSet-V2") train_data = data["train"] eval_data = data["validation"] test_data = data["test"] intra_project_test = test_data.filter(lambda x: x["isa_cross_project_example"] == False) cross_project_test = test_data.filter(lambda x: x["isa_cross_project_example"] == True) ``` ## Input The primary input for generating F* definition is **`source_type`**. All other information in an example may be used directly or to derive an input except **`source_definition`**, **`ideal_premises`**, and **`completed_definiton`**. ## Output The primary output is **`source_definition`**, which is the ground truth definition, that can be evaluated with the [proof checker](#evaluation-on-this-dataset). The **`completed_definiton`** may be used as ground truth when a model is used as a text completion setting (though the evaluator does not support evaluation in this setting). In addition, **`ideal_premises`** may be used for evaluating premise selection models. # Evaluation on this dataset Generated F* definitions should be evaluated the proof checker tool from [https://github.com/FStarLang/fstar_dataset/releases/tag/eval-v2.0](https://github.com/FStarLang/fstar_dataset/releases/tag/eval-v2.0). Download the source code and the `helpers.zip` file from the release. ## Troubleshooting The attached binaries in the evaluator (i.e., `fstar.exe` and `z3`) are built on **`Ubuntu 20.04.6 LTS (GNU/Linux 5.4.0-189-generic x86_64)`**, **`gcc (Ubuntu 9.4.0-1ubuntu1~20.04.2)`**, **`OCaml 4.12.0`**. If any of the binaries do not work properly, build F* from [this commit (10183ea187da8e8c426b799df6c825e24c0767d3)](https://github.com/FStarLang/FStar/commit/10183ea187da8e8c426b799df6c825e24c0767d3) from the [F* repository](https://github.com/FStarLang/FStar), using the [installation guide](https://github.com/FStarLang/FStar/blob/master/INSTALL.md). # Data Source In addition to the eight projects in `microsoft/FStarDataSet`, data from four more projects are included in this version. 1. [Starmada](https://github.com/microsoft/Armada): a framework for doing proofs by stepwise refinement for concurrent programs in a weak memory model. Starmada is an experimental version of Armada implemented in F⋆, relying on various advanced features of F⋆’s dependent type system for more generic and abstract proofs. 2. [Zeta](https://github.com/project-everest/zeta): a high performance, concurrent monitor for stateful services proven correct in F⋆ and its Steel concurrent separation logic 3. [Dice-star](https://github.com/verified-HRoT/dice-star): a verified implementation of the DICE measured boot protocol for embedded devices 4. [Noise-star](https://github.com/Inria-Prosecco/noise-star): a verified compiler for implementations of Noise protocols, a family of key-exchange protocols # Limitations **TDB** # Citation ``` @inproceedings{chakraborty2024towards, title={Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming}, author={Chakraborty, Saikat and Ebner, Gabriel and Bhat, Siddharth and Fakhoury, Sarah and Fatima, Sakina and Lahiri, Shuvendu and Swamy, Nikhil}, booktitle={Proceedings of the IEEE/ACM 47th International Conference on Software Engineering (To Appear)}, pages={1--12}, year={2025} } ```许可证：CDLA许可2.0（CDLA-Permissive-2.0） 任务类别： - 文本生成 - 文本到文本生成 - 其他 标签： - 代码 - F*（FStar） - PoPAI 友好名称：PoPAI-FStar数据集V2 样本规模区间：10K < 样本数 < 100K 语言： - 代码 - FST 本数据集是 [`microsoft/FStarDataSet`](https://huggingface.co/datasets/microsoft/FStarDataSet) 的2.0版本。 ## 核心目标 本数据集的核心目标是训练与评估面向证明的人工智能编程（Proof-oriented Programming with AI，简称PoPAI）。给定F*语言中的程序规约与证明，人工智能模型的目标是合成对应的实现（关于本数据集的使用细节，包括输入与输出格式，请参见下文[使用方法]）。 ## 数据格式 本数据集的每个示例均采用如下schema组织的字典形式： json { "file_name": <字符串：文件名称>, "name": <字符串：示例名称，可用于唯一标识该示例>, "original_source_type": <字符串：实际源类型，用于类型检查>, "source_type": <字符串：修改后的源类型，用于构造提示词>, "source_definition": <字符串：目标定义>, "source": <字典：包含本示例来源的元数据，包括项目名称、Git地址、Git提交哈希等>, "source_range": <字典：包含本定义在源文件中的起止行与列的元数据>, "file_context": <字符串：提取至当前定义位置的文件上下文>, "dependencies": <字典：本文件的构建依赖项>, "opens_and_abbrevs": <列表[字典]：文件中打开的模块与缩写模块列表，用于评估所需>, "vconfig": <字典：本定义的SMT求解器（SMT solver）标志>, "interleaved": <布尔值：本定义是否来自接口文件的交错定义>, "verbose_type": <字符串：由类型检查器解析得到的本定义的详细类型>, "effect": <字符串：副作用>, "effect_flags": <列表[字符串]：所有副作用标志>, "mutual_with": <列表：若本定义与其他定义互为递归，则列出这些定义的名称>, "ideal_premises": <列表[字符串]：基准真值定义中使用的其他定义>, "proof_features": <列表[字符串]>, "is_simple_lemma": <布尔值/空值>, "is_div": <布尔值：若本定义包含发散副作用则为真>, "is_proof": <布尔值>, "is_simply_typed": <布尔值>, "is_type": <布尔值/空值>, "partial_definition": <字符串>, "completed_definiton": <字符串>, "isa_cross_project_example": <布尔值：若本示例属于跨项目评估集则为真> } ## 使用方法 若要结合 [`datasets`](https://pypi.org/project/datasets/) 库使用本数据集，可参考如下代码： python from datasets import load_dataset data = load_dataset("microsoft/FStarDataSet-V2") train_data = data["train"] eval_data = data["validation"] test_data = data["test"] intra_project_test = test_data.filter(lambda x: x["isa_cross_project_example"] == False) cross_project_test = test_data.filter(lambda x: x["isa_cross_project_example"] == True) ## 输入 生成F*定义的主要输入为**`source_type`**字段。示例中的所有其他信息均可直接使用或用于推导输入，但**`source_definition`**、**`ideal_premises`**和**`completed_definiton`**除外。 ## 输出 主要输出为**`source_definition`**，即基准真值定义，可通过[证明检查器]进行验证。当将模型用于文本补全任务时，**`completed_definiton`**可作为基准真值（尽管评估器尚不支持该场景下的评估）。此外，**`ideal_premises`**可用于评估前提选择模型。 ## 本数据集上的评估 生成的F*定义应通过来自[https://github.com/FStarLang/fstar_dataset/releases/tag/eval-v2.0](https://github.com/FStarLang/fstar_dataset/releases/tag/eval-v2.0) 的证明检查工具进行评估。请从该发布页面下载源代码与`helpers.zip`文件。 ## 故障排查 评估器附带的二进制文件（即`fstar.exe`与`z3`）基于**`Ubuntu 20.04.6 LTS (GNU/Linux 5.4.0-189-generic x86_64)`**、**`gcc (Ubuntu 9.4.0-1ubuntu1~20.04.2)`**与**`OCaml 4.12.0`**构建。若二进制文件无法正常运行，请从[F*仓库](https://github.com/FStarLang/FStar)的[指定提交（10183ea187da8e8c426b799df6c825e24c0767d3）](https://github.com/FStarLang/FStar/commit/10183ea187da8e8c426b799df6c825e24c0767d3)处拉取代码，并按照[安装指南](https://github.com/FStarLang/FStar/blob/master/INSTALL.md)自行编译F*。 ## 数据来源 除`microsoft/FStarDataSet`原有的8个项目外，本版本还新增了4个项目的数据： 1. [Starmada](https://github.com/microsoft/Armada)：一个用于在弱内存模型下对并发程序进行逐步精化证明的框架。Starmada是Armada的实验性F*实现，依托F*依赖类型系统（Dependent Type System）的各类高级特性，以实现更具通用性与抽象性的证明。 2. [Zeta](https://github.com/project-everest/zeta)：一款高性能、并发的有状态服务监视器，已在F*中完成正确性证明，并配套其Steel并发分离逻辑。 3. [Dice-star](https://github.com/verified-HRoT/dice-star)：面向嵌入式设备的DICE度量启动协议的经过验证的实现。 4. [Noise-star](https://github.com/Inria-Prosecco/noise-star)：Noise协议（一类密钥交换协议）实现的经过验证的编译器。 ## 局限性 **待补充（TDB）** ## 引用 @inproceedings{chakraborty2024towards, title={面向SMT辅助的面向证明编程的神经合成}, author={Chakraborty, Saikat and Ebner, Gabriel and Bhat, Siddharth and Fakhoury, Sarah and Fatima, Sakina and Lahiri, Shuvendu and Swamy, Nikhil}, booktitle={IEEE/ACM第47届国际软件工程会议论文集（待出版）}, pages={1--12}, year={2025} }