当我们审视当前机器学习辅助程序验证器的发展现状时，会发现一个显著的结构性失衡：关于模型训练配方（超参数配置、损失函数设计、提示工程技巧）的技术文章俯拾皆是，而关于基准数据集本身的构建方法与 SMT 求解器集成工程的深度解析却极为稀缺。这种失衡直接导致研究者在复现工作时往往只能获得 “如何训练” 的零散信息，却难以系统掌握 “基准数据从何而来”“验证条件如何可靠地转化为 SMT 查询” 等底层工程问题。本文以 DafnyBench 为核心案例，系统梳理程序验证基准数据集从数据采集、去重、验证到与 SMT 求解器对接的完整技术链路，为研究者提供一份可操作的工程实践指南。
大规模基准数据集的构建方法论
构建高质量的程序验证基准数据集并非简单的代码收集过程，而是需要在数据多样性、验证可靠性和可扩展性之间寻求平衡。DafnyBench 作为目前规模最大的机器学习程序验证基准数据集，其构建流程为这一领域提供了极具参考价值的工程实践范式。该数据集最终包含 782 个经验证的独立 Dafny 程序，总代码量约 53,000 行，涵盖了从基础算法到中等复杂度软件系统的广泛场景。
数据采集阶段的核心挑战在于如何在海量公开代码中筛选出真正适合形式化验证的程序。DafnyBench 团队采用了 GitHub API 的语言过滤功能（language:Dafny），在 2023 年年底前抓取了所有公开可访问的 Dafny 源代码文件，初步获得了约 15,000 个原始文件。然而，这些文件存在大量重复内容，直接使用会导致基准数据集出现严重的数据倾斜问题。为此，团队引入了 MinHash 去重算法，通过计算文件之间的 Jaccard 相似度来识别重复变体。具体而言，算法将每个文件转换为 n-gram（通常是字符级三元组）的集合，然后使用多个哈希函数生成最小哈希签名，最后通过局部敏感哈希（LSH）技术将相似文件映射到相同的哈希桶中。在阈值为 0.5 的相似度条件下，该流程将原始文件数量从约 15,000 个有效压缩至约 5,000 个，剔除比例超过 60%，显著提升了数据集的多样性。
去重后的文件必须经过严格的自动化验证筛选才能进入基准数据集。团队使用 Dafny 4.3.0 版本的 dafny verify 命令对每个文件进行编译时验证，移除了所有无法通过验证的源代码。这一步骤的重要性在于：只有经过验证的代码才能作为可靠的 “地面真值”（ground truth），为后续的提示填充任务提供可信赖的评估基准。值得注意的是，团队在筛选过程中还移除了缺乏必要规范声明（requires/ensures 语句）的文件，以及完全缺少断言（assert）和循环不变式（invariant）的代码，因为这类程序无法为 “提示填充” 任务提供有意义的挑战。最终，556 个来自 GitHub 抓取的文件通过了全部筛选条件，加上从 Clover 数据集引入的 62 个教材级程序和从 dafny-synthesis 基准转换来的 164 个 MBPP 问题，总计形成了 782 个高质量基准程序。
验证条件生成与 SMT 求解器的集成架构
程序验证基准数据集的核心价值不仅在于提供待验证的源代码，更在于确保每一道验证题目都对应着可计算、可判定的验证条件（Verification Conditions, VC）。Dafny 作为一个内置形式化验证支持的编程语言，其后端采用了 Boogie 中间表示层来生成验证条件，随后将 VC 翻译为 SMT-LIB 格式的查询，委托给 Z3 等 SMT 求解器进行可满足性判定。这一架构为理解 SMT 求解器在程序验证中的角色提供了典型案例。
当 Dafny 编译器处理一个包含前置条件（requires）、后置条件（ensures）和循环不变式的程序时，它会执行以下转换流程：首先将源代码提升为 Boogie 中间语言表示，在这一阶段循环被展开为带有显式不变式约束的求守护前缀形式，函数调用被展开为带调用约定的程序图；随后，Boogie 生成一组逻辑公式，每个公式对应程序中需要验证的一个逻辑路径或循环入口；最后，这些公式被编码为 SMT-LIB 格式的求解请求，声明所需的理论（如线性整数算术、数组理论、位向量等），并设置适当的求解选项。
在工程实践中，SMT 求解器的集成远非简单的命令调用那么简单。一个健壮的验证流水线需要处理求解超时（通常设置 30 秒至 5 分钟的时限）、内存限制（通常为 1-4 GB）、以及结果不稳定等现实问题。研究者发现，验证条件生成过程中的微小变化 —— 例如变量命名顺序的改变、公式重写策略的调整 —— 都可能导致 SMT 求解器的运行时间出现数量级的波动。这种现象在学术文献中被称为 “验证不稳定性”，它对基准数据集的可复现性构成潜在威胁。为缓解这一问题，基准构建者通常会固定求解器版本、记录完整的求解日志，并在可能的情况下使用多个求解器进行交叉验证。
求解器选择与多策略集成
在更高级的验证场景中，单一 SMT 求解器往往难以应对所有类型的验证条件，因此引入求解器选择机制成为提升验证效率的关键策略。Where4 项目在这方面进行了开创性探索：它从 Why3 证明义务中提取结构化特征（如语法节点数量、各类运算符的计数、理论混合度等），然后训练机器学习模型来预测不同 SMT 求解器在特定验证条件上的性能表现。在实践中，这种方法能够将平均求解时间缩短 30%-50%，因为它避免了让 Z3 或 CVC4 在其不擅长的理论域上徒劳消耗计算资源。
MachSMT 则采用了更通用的算法选择框架，它在大量 SMT-LIB 基准实例上评测不同求解器配置的性能，构建起一个包含实例特征、求解器运行时间和最终结果的数据集。基于这个数据集，研究者可以训练排序模型或分类模型，来为每个新到来的验证条件推荐最优的求解器或求解策略。这些技术在形式化验证竞赛（如 SV-COMP）中已被广泛采用，其工程实现通常包含一个 “求解器驱动层”，它屏蔽了不同求解器的接口差异，为上层验证器提供统一的 API。
基准数据集的使用与评估
DafnyBench 的核心评估任务被设计为 “提示填充”（fill-hints）：给定一个移除了所有 assert 和 invariant 语句的验证程序，要求模型在正确位置插入恰当的验证提示，使程序能够通过 Dafny 验证器的检查。这一任务的评估标准非常严格：程序必须成功验证、必须保留原有的 requires 和 ensures 声明、且不得使用 {:verify false} 或 assume false 等 “作弊” 手段来绕过验证。
实验结果揭示了当前大语言模型在形式化验证辅助方面的能力边界。在 782 个基准程序上，Claude 3 Opus 取得了约 68% 的成功率，GPT-4 Turbo 紧随其后达到约 60%，而 CodeLlama-7B 等开源模型仅比 “无需模型” 基线（26.9%，即部分程序即使不添加任何提示也能自动验证）略有提升。值得注意的是，模型的表现在程序规模增大和所需提示数量增加时显著下降：当程序代码超过 200 行或提示文本超过 2000 字符时，成功率往往跌至 30% 以下。这一发现表明，当前模型在处理长程依赖和复杂验证条件时仍面临根本性挑战。
实践启示与工程参数
综合上述分析，构建可靠的程序验证基准数据集需要在以下工程参数上做出审慎决策。在数据采集层面，建议使用 GitHub API 的语言过滤结合 MinHash 去重，相似度阈值可设为 0.5，去重后的文件数量通常为原始数量的 30%-40%。在验证筛选层面，应固定验证器版本（如 Dafny 4.3.0），设置合理的超时参数（建议 60 秒），并同时保留 “有提示” 和 “无提示” 两个版本来评估基准的固有难度。在 SMT 求解器集成层面，推荐使用驱动架构来抽象求解器差异，设置超时（30-120 秒）和内存限制（1-4 GB），并记录完整的求解日志以支持后续的不稳定性分析。对于有兴趣构建自定义基准的研究者，建议从已有的公开数据集（如 SV-COMP、Why3 标准库）出发，通过结构化特征提取和地面真值交叉验证来确保质量。
资料来源
- DafnyBench 论文（arXiv:2406.08467）：https://arxiv.org/html/2406.08467v1
- Where4：预测软件验证中 SMT 求解器性能（arXiv:1701.08466）
- MachSMT：基于机器学习的 SMT 算法选择器