FVSpec：把真实世界的基于性质的测试转化为 Lean 形式化验证挑战

从 11039 个真实 Python 性质测试提炼 9415 个 Lean 4 验证任务。

前置知识

形式化验证 (Formal Verification, FV)

用数学证明的方法验证程序是否满足规约的技术，依赖交互式定理证明器（ITP）如 Lean、Coq 或自动化定理证明器（ATP）。与测试相比能给出几乎完美的信心，但需要专家写证明，工程代价极高。

论文核心是给 AI 模型出'写 Lean 证明'的题目，读者必须知道 ITP/ATP 的区别，以及为什么 FV 在工业界几乎不可用——这正是论文要解决的问题动机。

基于性质的测试 (Property-Based Testing, PBT)

不写具体输入例子，而是描述'输入应满足什么性质'，由框架（Hypothesis / QuickCheck）自动生成大量随机输入验证。在 ACL2s 等 ITP 中，未证明的定理语句会被自动当作 PBT 运行。

FVSpec 的素材全部来自 Python 的 Hypothesis PBT，理解 PBT 才能明白为何选取它作为'轻量级形式方法'桥梁——PBT 在工业界有真实采用，比纯 FV 更贴近普通工程实践。

Lean 4 依赖类型编程

Lean 4 是微软研究院维护的交互式定理证明器，语法类似函数式编程语言但支持依赖类型（值的类型可以依赖于其他值）。论文中大量定义形如 `def isort : List Int → List Int`，并用 `sorry` 占位符代替未写证明。

翻译 PBT 到 Lean 时会遇到'用未广泛使用的依赖类型语言建模 Python 语义'的难题；sorry 占位符机制是评测 AI 模型能否补全证明的关键。

结构忠实度 (Structural Faithfulness)

论文自定义的复合质量指标，五个子分数加权平均：$S = 0.25 S_{param} + 0.25 S_{type} + 0.20 S_{strat} + 0.20 S_{assert} + 0.10 S_{dep}$，衡量参数覆盖、类型对应、策略覆盖、断言覆盖、依赖覆盖，各项取值 $[0,1]$。

这是论文用来给同一 PBT 的多个形式化结果排序、挑选 canonical 的核心度量；理解它才能看懂为何中位忠实度只有 0.65（参数和依赖覆盖拉低）。

树解析与 LSP 修复循环 (tree-sitter & Language Server Protocol repair loop)

tree-sitter 是增量语法解析器，用来从 Python 源码中抽取函数定义和调用关系；LSP 是编辑器与编译器通信的标准协议。论文中形式化智能体每写完一轮 Lean 代码就触发 `lake build`，把编译器诊断信息通过 LSP/MCP 回传智能体修正，最多 16 轮迭代。

读者需要知道这不是一次性翻译，而是带自修复的多轮智能体调用——这是与 FVAPPS 等前作的主要工程差异，也是 25% 通过率的来源。

研究动机

AI 安全领域多个提案（如 ARIA Safeguarded AI、Guaranteed Safe AI、Scalable Formal Oversight）都假设未来 AI 生成的代码会被自主形式化验证智能体监督，但当前没有公开证据表明这种能力可行。现有 ITP 基准存在三类不足：规模太小（如 DafnyBench 782 题）、聚焦高级数学而非工程（如 FrontierMath、PutnamBench、Lean Workbook 共计数万题但全是数奥/高校数学），或源自专家驱动的验证项目（如 Vericoding 12,504 题、LEAN-GitHub 28,597 题、CoqStoq 10,396 题），这些题目本身就是写给 ITP 的代码，分布与 AI 训练数据高度重叠。FVAPPS（17,931 题）虽然方法最接近本文，但来源是 APPS 编程竞赛题，仍是合成数据而非'普通工程师随手写的工程代码'。结果就是：模型在数学竞赛题上能拿 60%+，但放到真实软件项目里就抓瞎——而真实软件恰恰有前端、后端、数据库、黑盒 API 和巨型依赖树，更难验证。

本文的目标是构建一个规模上千、来源真实软件工程、由非形式化背景的工程师所写、且未在 AI 训练数据中出现的 Lean 4 形式验证基准。具体三个目标：(1) 用爬虫抓取 GitHub 上 333 个开源仓库的 11,039 条真实 Python Hypothesis PBT（FVSpec:PBT）；(2) 通过智能体流水线把其中能编译的 2,772 条转成 9,415 道 Lean 验证题（FVSpec:FV），每题含 Python 实现 + Python PBT + Lean 实现 + 带 sorry 占位的 Lean 定理；(3) 用三个前沿模型（Claude Sonnet 4.6、Opus 4.7、GPT-5.4）跑基线，量化当下能力差距。

与已有工作不同的是，切入点是把 PBT 当作'真实工程师写的、合法但未证明的猜想'——这是从'用户视角'出发的形式验证任务，与 Vericoding/LEAN-GitHub 的'作者视角'（写代码时就知道要形式化）截然不同。技术上引入三个差异化设计：(1) 用树解析 + LSP 修复循环代替一次性翻译，容忍 Python→Lean 的高损耗；(2) 对效果性代码（Redis、文件系统、定时器）采用公理化接口策略，把副作用世界变成未解释的 `axiom`，使定理仍能约束核心状态转移；(3) 同一 PBT 平均保留 3.4 个形式化结果并用 `is_canonical` 标记最佳，承认翻译本质上是有损的。论文明确不追求与原 PBT 严格等价，只要'等价地有趣'，这一定位把基准从'测代码正确性'转变为'测 AI 在工程级形式化任务上的能力'。

核心方法

FVSpec 流水线分两条独立主线：上半段抓 PBT（FVSpec:PBT），下半段翻译成 Lean 验证题（FVSpec:FV）。直觉上是想把'工业界写了一半、没力气继续形式化下去的工程师'的遗产捞起来，让 AI 模型代替他们把 sorry 填上。具体技术路线分三个阶段：函数发现阶段用 tree-sitter 从 Python 源码里把被测函数（FUT）及其本地定义依赖的传递闭包挖出来；智能体转译阶段让一个 LLM 智能体同时产出 `Impl.lean`（纯定义，无 sorry）和 `Spec.lean`（每条 Hypothesis 断言对应一条带 sorry 的定理），每轮都跑 `lake build` 校验，失败就把编译器诊断信息回传给智能体重写，最多 16 轮；后处理阶段合并多轮结果、按结构忠实度打分挑 canonical、重跑 lake build 丢弃失败的、用 AST 分析器统计 sorry/axiom 行数、最后让 Claude Haiku 4.5 当判官打 easy/hard 二元标签并附带置信度。整套设计继承自 FVAPPS 但起点从编程竞赛题换成了真实 PBT，并补上了 LSP 自修复回路这一关键工程改进。

核心创新有三个层面。第一，**素材层面的范式切换**：把'验证基准'的来源从专家驱动的 ITP 代码池切到工程师随手写的 PBT，让题目天然 out-of-distribution。第二，**翻译策略层面的公理化封装**：当 Python 代码涉及 Redis、文件系统、定时器等副作用时，不试图在 Lean 里重建整个世界，而是把这些接口声明成 `axiom Redis : Type` 这种未解释符号，定理只约束纯函数部分的状态转移，从而既保证定理类型干净、又让题目仍然反映真实系统的契约——典型例子是给 scality/runner-manager 那个 GitHub Actions runner 控制器形式化时引入了 17 个公理。第三，**评测层面的非严格等价立场**：明确声明翻译是 lossy 的，同一 PBT 平均生成 3.4 个候选形式化结果全部保留、用 `is_canonical` 字段标记最佳、用 structural faithfulness 公式做 tie-break——这与之前所有'一个题目一个标准答案'的 ITP 基准假设根本不同。

方法步骤详情

具体可拆为 6 步。**Step 1 仓库发现**：用 PyGitHub 沿 Hypothesis 依赖图爬取，得到 19,808 个唯一 owner/repo 对并静态快照。**Step 2 许可证过滤**：剔除 AGPL/GPL/LGPL/MPL 等 copyleft 协议仓库，记录许可证字符串。**Step 3 PBT 抽取**：浅克隆每个仓库，用 ripgrep 找 `@given` 装饰器定位 PBT，用 Python AST 解析提取测试函数及调用到的本地定义闭包，24 小时产出 54,345 条原始 PBT。**Step 4 去重**：按仓库 base name 分组保留星标最多的 canonical fork，再按空白归一化 SHA-256 二次去重，剩下 11,039 条跨 333 仓库、281 用户、303 上游项目名。**Step 5 函数发现与智能体转译**：tree-sitter 提取 FUT 和本地依赖传递闭包（失败时生成带泛型的 stub FUT），然后一个形式化智能体（运行在 Inspect AI 框架里）生成 `Impl.lean` + `Spec.lean`，每轮通过 MCP 上的 Lean LSP 跑 `lake build`，失败诊断回传智能体继续重试，最多 16 轮迭代。**Step 6 后处理**：从 `.eval` 归档里抽 LLM 轮数 → JSONL 合并去重（tie-break 用 $S = 0.25 S_{param} + 0.25 S_{type} + 0.20 S_{strat} + 0.20 S_{assert} + 0.10 S_{dep}$ 五维加权结构忠实度）→ 重跑 lake build 过滤编译失败（分为超时/非良基递归/未知标识符/综合失败/类型不匹配/语法错误/缺失函数/应用错误/声明错误 9 类）→ AST 分析器统计 theorem/def/sorry/axiom 行数 → 让 Claude Haiku 4.5 当裁判打 easy/hard 标签及置信度（用 Sonnet 4.6 + GPT-5.4 表现做后验校准，得到约 70% 校准度）。最终入库 9,415 个样本，对应 2,772 个 PBT，命中率 25%，平均每题 8 个定理（中位 6、最大 66）、结构忠实度中位 0.65、59% 完整实现、41% 用 stub。

技术新颖性

技术新颖性主要体现在工程流水线层面而非新算法。论文没有发明新的定理证明技术或新的 LLM 训练方法，而是把现有组件（tree-sitter + Lean LSP/MCP + Inspect AI + 结构忠实度公式 + LLM-as-judge）组合成一个端到端的、可扩展的真实工程基准生产链。新颖性的核心在于：(1) 流水线能在 19,808 仓库规模下保持 25% 端到端成功率且全自动运行；(2) 公理化封装策略使效果性 PBT 也能产出有意义的 Lean 定理，扩展了可形式化任务的覆盖面；(3) 平均每 PBT 保留 3.4 个候选 + `is_canonical` 标记的多解设计，承认翻译损耗并把不确定性显式编码进数据集。相对前作 FVAPPS 的关键改进是增加了 LSP 自修复循环（最多 16 轮）以及把 Axiom 化方案落地——前者让端到端通过率从 FVAPPS 的近零提升到 25%，后者让题目从纯函数扩展到包含 Redis/Queue/State 等真实系统组件的工业级代码。

**Figure 1**: 单个 FVSpec 题目的四个 artifact（isort 示例）

实验结果

实验分三块。**翻译质量（图 4）**：9,415 个样本的结构忠实度中位数为 0.65、均值 0.67；五个子分数分布极度不均——类型对应 1.00、断言覆盖 0.97 已近饱和，策略覆盖 0.61 中等，而参数覆盖仅 0.24、依赖覆盖 0.48 是明显短板。这说明智能体在保留类型签名和断言语义上很强，但漏掉参数细节和本地辅助函数。**难度分布与实现完整度**：Claude Haiku 4.5 裁判把数据集打成 62% 难 / 38% 易；59% 样本含完整 `Impl.lean`，41% 用 stub 实现（但两组忠实度均值相当，0.67 vs 0.68），说明规约质量与实现是否完整基本独立。**基线模型（图 6、图 7）**：在 100 易 + 100 难的随机抽样上、Sonnet 4.6 / Opus 4.7 / GPT-5.4 均跑 best-of-5。Proved-ever 率在 Easy 上分别约 80% / 73% / 67%，在 Hard 上约 59% / 55% / 57%，整体均值 Easy 70%、Hard 49%——证明基准远未饱和，尤其是 Hard 维度。Refusal 率（模型声称题目不可解而跳过）在 Easy 上 3-5%、在 Hard 上 8-25%，其中 GPT-5.4 整体最高（15%），显示前沿模型在面对陌生 ITP 任务时的能力边界清晰可量化。**计算成本（图 8）**：GPT-5.4 在 k=5 时 wall-clock 中位约 1000 秒、token 中位约 2000k，远高于 Sonnet/Opus 的水平；Sonnet 4.6 是三者中最快的，但成功率也最低，呈现明显的'速度-能力'权衡。

**Table 2**: FVSpec:PBT 仓库多样性统计（描述性，文中未单列表号，源自第 3.1.1 节文字）

查看结构化数据

任务	指标	本文	基线	提升
Lean 4 定理证明（Easy 子集，best-of-5）	Proved-ever 率（零 sorry 且 lake build 通过）	Claude Sonnet 4.6 ≈ 80%、Opus 4.7 ≈ 73%、GPT-5.4 ≈ 67%	无（首次在此基准上报告）	基准本身首次定义，无历史可比；Easy 子集均值 70%
Lean 4 定理证明（Hard 子集，best-of-5）	Proved-ever 率	Claude Sonnet 4.6 ≈ 59%、Opus 4.7 ≈ 55%、GPT-5.4 ≈ 57%	无	Hard 子集均值 49%；Easy→Hard 平均掉 21 个百分点，体现难度分层有效
Refusal 率（声称题目无解）	模型主动跳过的样本比例	Easy 3-5%、Hard 8-25%、Overall 4-15%	无	GPT-5.4 在 Hard 上 25%，明显高于 Opus 4.7（8%），反映模型对自身能力边界感知差异
翻译质量（结构忠实度）	五维加权分 $S$ 在 $[0,1]$	中位 0.65、均值 0.67；子分数 Type 1.00 / Assert 0.97 / Strat 0.61 / Dep 0.48 / Param 0.24	无直接对照	首次定义该指标；Type+Assert 饱和证明转译在结构层面可行，Param+Dep 是下个改进点
难度分级校准	Haiku 4.5 标签预测模型表现的准确率	≈ 70% 校准度（基于 Sonnet 4.6 + GPT-5.4 后验表现）	无	首次在形式验证基准中引入 LLM-as-judge 校准机制，置信度随样本公开

局限与改进

作者在第 5 节坦承六类有效性质疑，最严重的是**效果性接口的公理化是否真有意义**——`axiom Redis : Type` 抓不住真实 Redis 的一致性、顺序、失败模式，所以基于它证的定理不一定能迁移到生产环境。其次是**翻译忠实度本身是启发式**：高忠实度不保证语义等价，低忠实度也不意味着题目无用。第三是**LLM 裁判可能失准**：Haiku 4.5 的 easy/hard 标签未对人类专家做校准，论文承认无法回答'这套题需要多少人类努力'。第四是**41% 样本只有 stub 实现**：定理良类型但被约束的函数体是空的，证明义务被弱化。第五是**许可证检测有边界情况**：当 GitHub 检测不到 license 时默认放行，可能引入版权不清的样本。第六是**没有人类基线**：无法把模型表现换算成人类专家工时。我自己额外观察两点：(1) 评测样本只 100 易 + 100 难，规模偏小，置信区间宽；(2) Refusal 率被作者纳入分析但不计入'Proved-ever'分母，这意味着如果模型大量拒绝则成功率的解读会被乐观偏置——应该用'意图证明过的样本中证明成功比例'作为更鲁棒的指标。

独立分析的弱点

从独立分析角度，至少有四个可改进的弱点。**弱点 1：翻译成功率的瓶颈在依赖闭包抽取而非定理生成本身**——结构忠实度里参数覆盖 0.24、依赖覆盖 0.48 是双重低位，建议在函数发现阶段先用 LLM 自动补充被外部库遮蔽的辅助函数（如 isort 例子里的 `insort`），甚至对每个 PBT 同时产出多种 stub 策略（保留 `bisect` 的纯函数版本与 stub 版本），让形式化智能体有更多选择空间。**弱点 2：LSP 修复循环 16 轮上限过死板**——长尾样本可能正好卡在第 17 轮突破，建议改为基于编译错误种类的自适应迭代（如类型错误 5 轮、未知标识符 10 轮、声明错误 16 轮分层），并把'差 1 个 sorry 就完成'的样本单独标记做冷启动续跑。**弱点 3：公理化接口粒度过粗**——给 runner-manager 引入了 17 个公理但没记录它们之间应有的约束（如 Redis key 唯一性、Queue FIFO），建议在后续版本里把'axiom + 不变式'升级为 'structure + 不变式'，让定理仍然只约束核心但公理间约束被显式编码。**弱点 4：评测指标单一**——目前只看 proved/partial credit/axiom 引入情况，建议加入'证明长度'、'是否复用 Mathlib 引理'、'修改原 Impl.lean 的程度'三个维度，前两者衡量 AI 是否真的理解 Lean 标准库而非硬编码、后者衡量是否在偷换题目。

未来方向

作者在结论里点明四个方向。**方向 1：跨语言/跨 ITP 扩展**——把 Hypothesis PBT 推广到 Haskell/QuickCheck、C++/RapidCheck、TypeScript/fast-check，并把 Lean 4 推广到 Coq、Isabelle、F*、Verus，因为不同 ITP 的语法风格和证明难度差异本身就是评测维度。**方向 2：与 HC-2026 语料融合**——补全当前基准缺失的运行时上下文（trace、crash dump、profile），让形式验证题不再只看规约，还能在端到端调试循环里被使用。**方向 3：被证伪的性质 → 程序修复任务**——用 Lean 反例或 Hypothesis 缩小的失败用例作为自动 program-repair 的种子，把'开发者自己的测试都没抓到'的 bug 用 Lean 精确定位出来。**方向 4：AI 安全场景下的实证**——把 FVSpec 用作'AI 生成代码的守门员'的实测平台，量化自动验证管线在多大吞吐量下能跟上 AI 代码生产速度。基于成果还可延伸的方向：(a) 把 9,415 个验证题拆成'证明能力'和'理解能力'两个子基准，前者只给 Spec.lean 让 AI 写证明、后者只给 Spec.lean 让 AI 反推 Python 测试用例；(b) 引入人类专家小样本标注，构造人机混合校准的难度标签，替代当前的 Haiku 4.5 单裁判。

复现评估

**完全开源**，这是论文值得称赞的一点。所有构件在 GitHub `github.com/GaloisInc/fvspec` 下以 MIT/Apache 双协议发布，包括 scraper、依赖抽取器、形式化智能体、后处理脚本；两个数据集分别托管在 `huggingface.co/datasets/GaloisInc/fvspec-pbt`（FVSpec:PBT，11,039 条）和 `huggingface.co/datasets/GaloisInc/fvspec-fv`（FVSpec:FV，9,415 个样本）。**算力门槛**：复现全流水线需要跑两次大规模智能体转译（feb03 用 Sonnet 4.5 产出 5,979 题，apr08 用 Sonnet 4.6 产出 3,436 题），按图 8 的 token 中位数 1000-2000k/样本、wall-clock 1000-3000 秒/样本估算，单卡完整复现需消耗数百万美元级 LLM 费用，普通研究者基本只能复现评测环节。**复现难度**：评测环节门槛相对低——准备好 Lean 4 + lake 工具链、Clone 评测代码即可跑三个 baseline 模型，模型推理本身走 API 即可；但样本筛选（100 易 + 100 难的随机抽样）和指标计算逻辑需要严格对齐基线脚本，避免 Refusal 处理方式不一致带来结果偏差。**许可可商用**：双协议允许二次使用和商业化分发，但要注意 41% 的 stub 实现样本需要被下游用户过滤以避免误用。

FVSpec：把真实世界的基于性质的测试转化为 Lean 形式化验证挑战 FVSpec: Real-World Property-Based Tests as Lean Challenges