2026-10-24 10:17:12 网络安全文章来源：ZONE.CI 全球网 0 阅读模式

G.O.S.S.I.P 阅读推荐 2026-10-20 PV-BENCH

QCP团队
QCP团队

安全研究GoSSIP

2026年10月20日 20:40
上海

去阅读

AI 正在让程序编写和修改变得更加高效，但生成的代码是否真正满足需求，仍然需要可靠的检查。测试能够发现错误，形式化验证则进一步通过精确的规约和数学证明，论证程序对所有满足前置条件的输入都能满足要求。

让 AI 自动完成这样的验证，仍面临不小的困难。规约如何准确表达需求、循环不变式如何选取、算法与内存操作如何一同证明，都依赖专业经验。高质量训练数据的不足是其中一项制约：现有公开代码很多，配有完整规约、标注和证明的验证实例却相对稀缺。

完整实例能够具体展示从算法概念到规约和证明的过程。以排序为例，“结果有序”只是功能要求的一部分，规约还必须保证原有元素及其出现次数不变。对于采用不同数据结构或加入性能优化的 C 程序，还要考虑如何描述内存、如何建立数学对象与具体存储之间的对应，以及如何组织证明。这些具体的设计选择和证明方法，正是模型需要学习、研究者希望复用的经验。

为此，上海算法创新研究院QCP（Qualified C Programming Verifier，C语言程序验证工具）团队（网址：https://www.qua.codes）于近日发布了程序验证基准 PV-BENCH，收录 233 个 C 程序实例。团队将积累的规约设计与证明经验融入 AI 智能体的工作流程，在专家指导和审核下，通过智能体自动执行或人机协作，使用 QCP 完成了这些程序的规约编写和验证。

PV-BENCH 将程序、规约、标注和证明一并发布，既提供可以研究和复用的验证实例，也为后续的全自动程序验证研究提供评测依据，支持探索效率更高、成本更低的自动验证方法。其突出特点是纳入较多具有实际编程复杂度的C 程序，并重点验证程序的功能正确性，而不止是内存安全性。与部分只包含数组基本操作、算术运算，或简化、略去关键实现细节的已有数据集不同，PV-BENCH 还覆盖实际编程中常用的高效、紧凑实现方式。

一、从经典算法到竞赛级程序

本次发布的 PV-BENCH 版本主要来自两部分：

86 个算法、数据结构和工程实例：包括 41 个经典算法实现、13 个 LeetCode 实例、19 个洛谷实例、5 个数据结构模块，以及 8 个工程例程，涵盖 C 字符串与内存操作函数、MiniSat 中的动态向量等。
147 个 Codeforces 实例：题目评分覆盖 800–2800，其中 26 个不低于 2000。这些 C 实现由语言模型根据题目描述生成，并通过相应在线评测的时间与内存限制，随后作为固定程序用于验证评测。

程序涉及排序、贪心、动态规划、图算法、数论和计算几何等领域。同一算法也保留了不同实现，用于考察规约与证明如何适应具体的控制流程和数据布局：

快速排序：涵盖从数组两端向中间扫描的 Hoare 分区、从一端单向扫描的 Lomuto 分区两种方案，共五种实现；其中 Hoare 方案包含交换式、填坑式及不同递归边界处理的版本。
Prim 最小生成树：包括邻接矩阵上返回最小生成树总权重、返回树的邻接矩阵，以及采用链式前向星和支持减小键值操作的堆、返回树的边数组等实现。
深度优先搜索（DFS）：分别使用一维数组展开的邻接矩阵、二维邻接矩阵，以及链式邻接表存图。

每个实例均配有题目描述、固定的 C 源码、经专家审核的参考规约，以及参考标注和完整的验证材料。QCP 自动处理一部分验证条件，其余由补充的 Rocq 证明完成。

根据基准数据统计，233 个实例共包含 12,599 行 C 代码。结合参考规约与标注，QCP 共生成 16,724 项验证条件，其中 4,638 项需要进一步完成证明。

QCP 是基于定理证明技术的 C 程序验证工具，支持 Rocq 和 Lean 两种后端。AI 可以与 QCP 交互配合，完成 C 程序的规约编写与验证。

二、分别评测规约、标注与证明

PV-BENCH 设置三项独立任务，分别考察验证过程中的关键能力：

规约生成：根据题目描述和固定代码，编写输入条件、输出要求及相应的数学定义。
程序标注：给定代码和参考规约，添加循环不变式、中间断言等验证所需的标注。
证明补全：给定参考规约与标注，在 Rocq 中证明 QCP 未能自动求解的验证条件。

三项任务独立评测，所需的前序材料均采用参考版本。例如，证明补全直接使用参考规约与标注，使规约或标注生成中的错误不会传递到证明任务，便于判断困难究竟出在哪个环节。

评测不仅检查生成的材料能否通过验证工具，还要求生成的规约与参考规约表达相同的要求，避免通过降低要求来获得“验证成功”。

图 1：规约生成与程序标注的评测流程。评审模型寻找证明或反驳证据，再交由验证工具检查。

三、代表性程序实例

这些任务要求证明程序的功能正确性，而不止是内存安全性。 以下三个例子展示不同程序的验证重点。

1. 图的多种存法：不同内存表示，相同可达性要求

同一张图可以存为一维邻接矩阵、二维邻接矩阵，也可以存为链式邻接表。下面对照链式邻接表和二维邻接矩阵两版 DFS。两者都用 vertex 指定搜索起点，用 visited 数组记录访问结果。

1.1. 链式邻接表。adjacency[u] 指向顶点 u 的邻居链表，每个节点保存一个邻居编号和指向下一节点的指针。

void dfs_adjacency_list(struct list **adjacency, int vertex_count,
                        int *visited, int vertex);

1.2. 二维邻接矩阵。matrix[u][v] 为 1 表示从 u 到 v 有边，为 0 表示无边。

void dfs_adjacency_matrix_2Darray(int **matrix, int vertex_count,
                                  int *visited, int vertex);

两个实现的共同点是都需要验证DFS能够遍历每一个从起点出发可达的节点。但是两者需要基于不同的图的存储方式完成证明细节：前者使用了邻接表，后者使用了邻接矩阵。

2. 数据结构vector：扩容后，元素序列如何变化

PV-BENCH 从公开代码库中收录了动态向量（vector）的一种定义与实现，下面以其中的整数向量为例：

struct veci_t {
    int    size;
    int    cap;
    int*   ptr;
};
typedef struct veci_t veci;

size 是已经存入的元素个数，cap 是缓冲区能容纳的元素个数，ptr 指向缓冲区。只有前 size 个位置属于当前向量的内容，其余位置是预留空间。

动态向量（vector）中追加元素函数 veci_push(v, e) 的声明如下：

void   veci_push   (veci* v, int e);

这个函数的实现中会在向量末尾加入 e；如果缓冲区已满，则先扩容。例如，下面图中把 50 追加到 [10, 20, 30, 40] 后得到 [10, 20, 30, 40, 50]。空间充足时，缓冲区地址和容量保持不变；空间已满时，需要扩容，缓冲区地址也可能改变。无论走哪条执行路径，元素顺序和内容都必须符合追加操作的要求。

图 2：缓冲区已满时追加元素：四个原有元素保留，末尾加入 50，容量由 4 增至 9。预留空间不属于当前元素序列。

不过在这个C函数的规约中，这些底层实现细节会被隐藏起来，整个规约很简明：veci\_push(v, e)会完整保留原有元素，并且只在末尾追加一个 e。

这个例子说明，一次简单的“追加元素”操作，背后可能包含扩容、内存迁移和结构体字段更新。验证需要证明这些操作共同实现了序列末尾追加的效果，并保持长度、容量与缓冲区内容一致，但是最后的规约是一个简单的功能描述，并不暴露具体底层存储的细节。在程序验证的过程中，底层存储的细节会被隐藏在证明中，但是这个函数的对外承诺会被简洁地封装起来。

3. Inconvenient Pairs：从绕路条件到点对计数

Codeforces 1569D Inconvenient Pairs 是一道编程题目：给定若干贯穿城市的横街、竖街，以及街道上的人。若两人之间沿街道行走的最短距离，严格大于两点的曼哈顿距离，就称他们构成一个“坏的点对”。任务是统计这样的无序点对，每对只计一次。

例如，下图中灰色实线表示的是仅有的两条横街和两条竖街。横街位于 y = 0 和 y = 4，两个人分别站在竖街上的 (0, 1) 和 (2, 2)。他们的曼哈顿距离是 3，但必须先走到横街才能转向，最短路程为 5，因此构成坏点对。

图 3：同一水平条带内、不同竖街上的两人必须绕行。蓝色实线为最短街道路径；橙色虚线仅用于说明曼哈顿距离。图为城市局部示意。

这道题目的求解程序会通过划分条带、排序和分组来计数。要证明这种计数方法符合题意，必须先建立几何上的等价关系：坏点对恰好来自两类情况——两人严格位于同一对相邻横街之间、分属不同竖街，或者严格位于同一对相邻竖街之间、分属不同横街。交叉口上的人不会与其他人构成坏点对。于是，每个条带的贡献可以写成“带内所有点对数，减去同一条街上的点对数”。

这个例子说明，程序验证不仅要论证程序的实现将计算出何种结果，还要论证这种计算方法背后的数学原理。

总结

PV-BENCH 将过去形式化专家在规约设计和程序验证中的经验在AI的辅助下整理为公开、可检查的参考材料，并通过规约生成、程序标注和证明补全三项独立任务，帮助研究者分析 AI 在自动验证中的能力与不足。我们希望这批实例能够支持后续模型与方法的研究，成为检验进展的共同依据，推动更高效、低成本的全自动程序验证。

项目公开地址：

数据集（Hugging Face）：https://huggingface.co/datasets/PV-SJTU/PV-Bench

代码仓库（GitHub）：https://github.com/QinxiangCao/PV-bench

QCP官网与下载：