为什么需要新的基准测试
神经网络编写的代码越多，就越需要回答一个尖锐的问题：如何确保这些代码确实做了它该做的事？常规测试能发现一部分错误，但无法提供正确性的形式化保证。为此需要验证——将程序转化为严格的数学命题语言，并证明其性质。这项工作昂贵且复杂，因此研究人员希望将其交给人工智能。
问题在于，在工整的教学示例上训练的模型，面对真实代码时常常迷失方向。真实项目中充满了隐式约定、语言特性和未文档化的行为。要检验人工智能能否应对这些条件，需要一个建立在真实程序而非合成练习题上的大规模试验场。
FVSpec：将真实测试作为人工智能的任务
一组研究人员——Quinn Dougherty、Max von Hippel、Simon Henniger、Hazel Shackleton和Mike Dodds——提出了基准测试 FVSpec。该工作以编号2606.01008发表在arXiv上，作者于2026年8月发布了更新版本。
核心思路是提取真实Python仓库中的基于属性的测试，并将其转化为Lean 4语言的形式化规范。这类测试检验的不是具体示例，而是函数的性质：“对于任何合法输入，都满足某个特定条件”。这使它们成为通往数学形式化的天然桥梁。
作者从开源Python项目中收集了11,039个基于属性的测试。其中只有2,772个能够自动翻译为Lean 4——约占四分之一。而输出端得到了9,415条规范：每个成功翻译的测试对应约三种形式化变体。之所以需要冗余，是因为同一性质可以用不同方式表述，事先并不总能判断哪种变体更便于后续证明。
为什么这很困难
将测试改写为Lean并非机械的语法替换。Python和Lean处于不同的范式：前者是动态类型、可变对象和命令式结构，后者则是带有依赖类型的严格类型系统。要使规范符合代码的真实行为，必须仔细建模Python的语义。
另一个难点在于，基于属性的测试通常以命令式脚本的形式编写：包含循环、异常和状态操作。从中提炼出“对于任何x，P(x)成立”这样的纯粹命题，本身就是一项研究任务。
最后，Lean 4仍然是一门类型系统复杂的语言，即使在专业开发中也很少见。这对语言模型来说是严峻的挑战：它们需要同时掌握罕见的语法、适应依赖类型并生成正确的定义。
流水线与评估的构成
为了实现自动翻译，作者构建了一个由三个LLM代理组成的流水线。从描述来看，代理之间分工协作：一个解析原始测试，一个构建规范，另一个检查并改进结果。流水线的全部代码以及收集的数据均已公开。
翻译质量从多个维度进行评估。覆盖率反映真实测试中能够形式化的比例。独立的质量指标评估所得规范在多大程度上反映了代码的原始行为。此外，研究人员还记录了证明生成的基线：他们运行了多种自动化和模型驱动的方法，并统计这些方法成功证明所表述命题的频率。这些测量为后续工作提供了比较的参照点。
这对实践意味着什么
FVSpec瞄准的是一个研究较少的领域——真实软件的人工智能辅助形式化验证。能够证明教学示例的性质并不能保证在真实代码上取得成功，因此建立在真实测试之上的基准测试有助于公平比较各种方法并跟踪进展。
这种方法的重要性随着神经网络生成的代码量增长而日益凸显。如果人工智能越来越多地编写程序，那么自动化的正确性检查工具就不再是奢侈品，而是必需品。
结论
FVSpec是朝着让形式化验证不再局限于少数专家、转而成为实用工具迈出的重要一步。该基准测试将真实的基于属性的测试、Lean 4语言和开放的LLM流水线结合在一起。得益于公开的数据和代码，任何研究者都可以复现实验或提出自己的方法，这意味着社区拥有了一个共同的前进起点。
