AI 正在让程序编写和修改变得更加高效，但生成的代码是否真正满足需求，仍然需要可靠的检查。测试能够发现错误，形式化验证则进一步通过精确的规约和数学证明，论证程序对所有满足前置条件的输入都能满足要求。
让 AI 自动完成这样的验证，仍面临不小的困难。规约如何准确表达需求、循环不变式如何选取、算法与内存操作如何一同证明，都依赖专业经验。高质量训练数据的不足是其中一项制约：现有公开代码很多，配有完整规约、标注和证明的验证实例却相对稀缺。
完整实例能够具体展示从算法概念到规约和证明的过程。以排序为例，“结果有序”只是功能要求的一部分，规约还必须保证原有元素及其出现次数不变。对于采用不同数据结构或加入性能优化的 C 程序，还要考虑如何描述内存、如何建立数学对象与具体存储之间的对应，以及如何组织证明。这些具体的设计选择和证明方法，正是模型需要学习、研究者希望复用的经验。
为此，QCP 团队发布了程序验证基准 PV-BENCH，收录 233 个 C 程序实例。团队将积累的规约设计与证明经验融入 AI 智能体的工作流程，在专家指导和审核下，通过智能体自动执行或人机协作，使用 QCP 完成了这些程序的规约编写和验证。
PV-BENCH 将程序、规约、标注和证明一并发布，既提供可以研究和复用的验证实例，也为后续的全自动程序验证研究提供评测依据，支持探索效率更高、成本更低的自动验证方法。
访问 PV-BENCH：Hugging Face 数据集 · GitHub 仓库
从经典算法到竞赛级程序
本次发布的 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 证明完成。
分别评测规约、标注与证明
PV-BENCH 设置三项独立任务，分别考察验证过程中的关键能力：
- 规约生成：根据题目描述和固定代码，编写输入条件、输出要求及相应的数学定义。
- 程序标注：给定代码和参考规约，添加循环不变式、中间断言等验证所需的标注。
- 证明补全：给定参考规约与标注，在 Rocq 中证明 QCP 未能自动求解的验证条件。
三项任务独立评测，所需的前序材料均采用参考版本。例如，证明补全直接使用参考规约与标注，使规约或标注生成中的错误不会传递到证明任务，便于判断困难究竟出在哪个环节。
评测不仅检查生成的材料能否通过验证工具，还要求生成的规约与参考规约表达相同的要求，避免通过降低要求来获得“验证成功”。
代表性实例：从程序行为到数学原理
这些任务要求证明程序的功能正确性，而不止是内存安全性。 以下三个例子展示不同程序的验证重点。
图的多种存法：不同内存表示，相同可达性要求
同一张图可以存为一维邻接矩阵、二维邻接矩阵，也可以存为链式邻接表。下面对照链式邻接表和二维邻接矩阵两版 DFS。两者都用 vertex 指定搜索起点，用 visited 数组记录访问结果。
链式邻接表。 adjacency[u] 指向顶点 u 的邻居链表，每个节点保存一个邻居编号和指向下一节点的指针。
void dfs_adjacency_list(struct list **adjacency, int vertex_count,
int *visited, int vertex);
二维邻接矩阵。 matrix[u][v] 为 1 表示从 u 到 v 有边，为 0 表示无边。
void dfs_adjacency_matrix_2Darray(int **matrix, int vertex_count,
int *visited, int vertex);
两个实现的共同点是都需要验证DFS能够遍历每一个从起点出发可达的节点。但是两者需要基于不同的图的存储方式完成证明细节：前者使用了邻接表，后者使用了邻接矩阵。
这个例子说明，同一算法的不同实现，可以共享数学上的功能要求描述，同时需要各自的内存描述。程序验证需要把抽象的功能要求，落实到具体的数据表示上。
MiniSat 中的动态向量：扩容后，元素序列如何变化
MiniSat 是一款小巧的开源布尔可满足性（SAT）求解器，用于判断一个布尔公式是否存在使其为真的变量赋值。PV-BENCH 收录了 MiniSat 中动态向量（vector）的定义与实现，下面以其中的整数向量为例：
struct veci_t {
int size;
int cap;
int* ptr;
};
typedef struct veci_t veci;
size 是已经存入的元素个数，cap 是缓冲区能容纳的元素个数，ptr 指向缓冲区。只有前 size 个位置属于当前向量的内容，其余位置是预留空间。下图展示缓冲区已满时追加一个元素的情况：
下面是追加元素函数 veci_push(v, e) 的声明。它在向量末尾加入 e；如果缓冲区已满，则先扩容。
void veci_push (veci* v, int e)
/*@ With (xs : list Z) (buf : Z) (cap : Z)
Require
... && veci_raw(v, buf, cap, xs)
Ensure
exists buf2 cap2, ... &&
veci_raw(v, buf2, cap2, app(xs, cons(e, nil)))
*/;
验证要保证原有元素完整保留，并且只在末尾追加一个 e。例如，图中把 50 追加到 [10, 20, 30, 40] 后得到 [10, 20, 30, 40, 50]。空间充足时，缓冲区地址和容量保持不变；空间已满时，需要扩容，缓冲区地址也可能改变。无论走哪条执行路径，元素顺序和内容都必须符合追加操作的要求。
这个例子说明，一次简单的“追加元素”操作，背后可能包含扩容、内存迁移和结构体字段更新。验证需要证明这些操作共同实现了序列末尾追加的效果，并保持长度、容量与缓冲区内容一致，但是最后的规约是一个简单的功能描述，并不包含具体的底层存储的细节。底层存储的细节隐藏在证明中，对外承诺的行为需要简洁。
Inconvenient Pairs：从绕路条件到点对计数
Codeforces 1569D Inconvenient Pairs 给定若干贯穿城市的横街、竖街，以及街道上的人。若两人之间沿街道行走的最短距离，严格大于两点的曼哈顿距离，就称他们构成一个“坏的点对”。任务是统计这样的无序点对，每对只计一次。
例如，相邻横街位于 y = 0 和 y = 4，两个人分别站在竖街上的 (0, 1) 和 (2, 2)。他们的曼哈顿距离是 3，但必须先走到横街才能转向，最短路程为 5，因此构成坏点对。
下面是求解函数 solver 的声明，它返回坏点对的数量。xs 保存竖街的横坐标，ys 保存横街的纵坐标，px、py 分别保存每个人的横、纵坐标；后四个数组是分组和排序使用的工作空间。
static long long solver(const int *xs, int n, const int *ys, int m,
const int *px, const int *py, int k,
int *va_grp, int *va_key,
int *ha_grp, int *ha_key);
程序实际通过划分条带、排序和分组来计数。要证明这种计数方法符合题意，必须先建立几何上的等价关系：坏点对恰好来自两类情况——两人严格位于同一对相邻横街之间、分属不同竖街，或者严格位于同一对相邻竖街之间、分属不同横街。交叉口上的人不会与其他人构成坏点对。于是，每个条带的贡献可以写成“带内所有点对数，减去同一条街上的点对数”。
这个例子说明，验证不仅要论证程序完成了分组、排序和计数，还要证明这种计数方法为何等价于题目中的最短路条件。问题背后的数学原理，也是程序正确性证明的一部分。
PV-BENCH 将这些规约设计和证明经验整理为公开、可检查的参考材料，并通过规约生成、程序标注和证明补全三项独立任务，帮助研究者分析 AI 在自动验证中的能力与不足。我们希望这批实例能够支持后续模型与方法的研究，成为检验进展的共同依据，推动更高效、低成本的全自动程序验证。