juwel07/formai-v2-full

--- dataset_info: features: - name: category dtype: string - name: file_name dtype: string - name: verification_finished dtype: string - name: vulnerable_line dtype: int64 - name: column dtype: int64 - name: function dtype: string - name: violated_property dtype: string - name: error_type dtype: string - name: code_snippet dtype: string - name: source_code dtype: string - name: num_lines dtype: int64 - name: cyclomatic_complexity dtype: float32 splits: - name: train num_bytes: 960684901 num_examples: 331000 download_size: 133615536 dataset_size: 960684901 configs: - config_name: default data_files: - split: train path: data/train-* --- # Dataset Card for Dataset Name <!-- Provide a quick summary of the dataset. --> Lanuage model generated c code with security vulnerabilities From ### Dataset Sources [optional] <!-- Provide the basic links for the dataset. --> - **Repository:** https://github.com/FormAI-Dataset/FormAI-dataset/?tab=readme-ov-file - **Paper:** https://dl.acm.org/doi/10.1145/3617555.3617874 ## Citation [optional] <!-- If there is a paper or blog post introducing the dataset, the APA and Bibtex information for that should go in this section. --> **BibTeX:** @inproceedings{10.1145/3617555.3617874, author = {Tihanyi, Norbert and Bisztray, Tamas and Jain, Ridhi and Ferrag, Mohamed Amine and Cordeiro, Lucas C. and Mavroeidis, Vasileios}, title = {The FormAI Dataset: Generative AI in Software Security through the Lens of Formal Verification}, year = {2023}, isbn = {9798400703751}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, url = {https://doi.org/10.1145/3617555.3617874}, doi = {10.1145/3617555.3617874}, booktitle = {Proceedings of the 19th International Conference on Predictive Models and Data Analytics in Software Engineering}, pages = {33–43}, numpages = {11}, keywords = {Artificial Intelligence, Dataset, Formal Verification, Large Language Models, Software Security, Vulnerability Classification}, location = {<conf-loc>, <city>San Francisco</city>, <state>CA</state>, <country>USA</country>, </conf-loc>}, series = {PROMISE 2023} }The FormAI dataset consists of C code generated by language models with security vulnerabilities, analyzed through formal verification methods. It is designed to explore the application of generative AI in software security, particularly from the perspective of formal verification. The dataset includes multiple feature fields such as category, file name, verification finished status, vulnerable line number, column, function, violated property, error type, code snippet, source code, number of lines, and cyclomatic complexity, which detail the security vulnerability attributes of each code sample. It can be used for tasks like vulnerability classification, software security analysis, and machine learning model training.

搜集汇总

数据集介绍

构建方式

伴随大语言模型在代码生成场景中的迅速普及，程序安全属性的可验证性成为软件工程与形式化方法交汇的重要议题。formai-v2-full 的构建依托生成式模型产出的C语言程序，并将形式验证机制嵌入数据生成与标注流程，对样本的安全属性进行自动化核查。数据集将验证结果细化为漏洞行、列、函数名、违反属性与错误类型等结构化字段，同时保留代码片段、源文件、类别、验证完成状态、行数及圈复杂度等元信息，从而形成由模型生成、形式化验证与缺陷定位共同支撑的漏洞语料。

特点

该数据集体现出生成式人工智能与软件安全分析深度融合的语料特征。其训练集包含331,000条样本，规模约960MB，覆盖语言模型生成的C代码及其安全缺陷标注。字段体系兼顾代码文本与验证语义，既有 code_snippet、source_code 等代码内容，也有 violated_property、error_type 等安全属性标签，并辅以 vulnerable_line、column、function 实现细粒度定位。num_lines 与 cyclomatic_complexity 进一步刻画代码规模与复杂度，为漏洞成因分析、模型安全性评估和程序理解研究提供多维信息。

使用方法

在软件安全与代码智能研究中，formai-v2-full 可通过 HuggingFace Datasets 接口便捷加载，默认配置下读取 train 数据分片即可获得完整训练语料。研究者可依据 verification_finished 筛选已完成形式验证的样本，围绕 error_type、violated_property 开展漏洞分类与属性违背分析，或利用 vulnerable_line、column、function 进行缺陷定位任务。结合 source_code 与 code_snippet，该数据集亦适用于大语言模型生成代码的安全评估、静态分析器基准测试及漏洞检测模型微调，圈复杂度与行数可作为辅助协变量纳入建模。

背景与挑战

背景概述

在生成式人工智能深度介入软件开发的浪潮中，formai-v2-full 作为 The FormAI Dataset 的扩展版本，由 Norbert Tihanyi、Tamas Bisztray、Ridhi Jain、Mohamed Amine Ferrag、Lucas C. Cordeiro 与 Vasileios Mavroeidis 等研究者于 2023 年提出并发表于 PROMISE 2023。其核心研究问题在于借助形式验证方法审视大语言模型生成 C 代码的安全漏洞，构建包含三十三万一千条训练样本的大规模标注资源，字段覆盖类别、函数、违反属性、错误类型、漏洞行、代码片段、圈复杂度等。该数据集为 AI 生成代码的安全性评估、漏洞分类与形式验证研究提供了重要基准，推动软件安全分析从经验判断走向可验证证据。

当前挑战

面向大语言模型生成 C 代码的安全审计，该数据集所应对的领域难题在于自动识别缓冲区溢出、空指针解引用、整数溢出、资源泄露与未定义行为等安全隐患，并在形式验证中缓解状态空间爆炸、验证超时与误报漏报的权衡。构建过程中的挑战涉及海量生成代码的可编译性与可验证性筛选，验证工具返回未知结果时的标注处理，漏洞行与违反属性的精确定位，不同生成模型与提示策略造成的分布异质性，以及安全类别不平衡对训练与评测的潜在偏置。这些因素共同构成数据质量与泛化能力的关键约束。

常用场景

经典使用场景

在生成式人工智能日益渗透源代码创作的背景下，formai-v2-full为C语言程序的安全漏洞研究提供了大规模、经过形式化验证的标注资源。其经典用途在于构建生成代码安全基准：研究者利用category、violated_property、error_type与code_snippet等字段，对语言模型生成的C代码进行漏洞检测、分类与定位，评估静态分析器、神经漏洞预测模型及混合验证工具在同分布与跨分布样本上的表现。该数据集亦支持剖析循环复杂度、代码行数与漏洞出现之间的统计关联，并可作为形式化验证流程的回归测试床，推动生成式编程安全评估从经验判断走向可计量、可复现的实证范式。

衍生相关工作

formai-v2-full延续了形式化验证与生成式AI安全交叉领域的研究脉络，并催生了一系列围绕漏洞检测、分类与安全对齐的经典工作。相关研究或以该数据集训练神经符号漏洞预测器，或将其作为评测基准检验大语言模型生成C代码的安全缺陷分布，亦有工作将其与静态分析、模糊测试及程序修复方法结合，探索多阶段验证管线。该数据集还推动安全标注规范、漏洞属性本体与跨模型泛化能力的讨论，进而影响后续多语言、多漏洞类型数据集的构建思路。这些衍生工作共同强化了以可验证证据评估AI生成代码安全性的研究传统。

数据集最近研究

最新研究方向

在生成式人工智能深度渗透软件工程全链条的背景下，formai-v2-full以形式化验证标注的三十余万条语言模型生成C代码样本，为AI代码安全研究构筑了可复现的实证基座。近期研究聚焦于借助其漏洞行、违反属性与错误类型标签，开展大模型生成代码的细粒度漏洞定位、缺陷分类、自动修复与安全约束学习，并探索复杂度特征同漏洞模式的关联。伴随AI编程助手大规模应用及供应链安全事件频发，该数据集推动形式验证与机器学习融合，支撑可信代码生成评测与安全对齐，对构建可审计、可验证的智能软件生态具有基准意义。