FVSpec: 真实世界基于属性的测试作为 Lean 挑战

TL;DR FVSpec 将真实 Python 仓库中的基于属性的测试（PBT）自动转换为 Lean 4 规范与证明目标，构建了一个 AI 辅助形式验证的基准，并通过多智能体 LLM 流水线系统评估证明生成能力。

问题

问题背景

AI 生成的代码正大量进入现实软件系统，如何确保其正确性与安全性成为关键挑战。形式验证（Formal Verification）通过数学证明来保证软件行为符合规约，被视为未来 AI 安全（如 Safeguarded AI）的核心技术支柱。然而，将真实代码从日常开发语言转换为交互式定理证明器（ITP）的可验证规范，至今仍缺乏系统化的方法与基准。

现有方法局限

目前的 AI 辅助形式验证工作大多停留在玩具级或合成数据集上，例如使用启发式规则、领域特定语言或人工设计的定理。主要局限有三：

• 缺乏真实世界语义覆盖：现有基准很少涉及 Python 生态中流行的 property-based testing（PBT），无法反映实际工程中混杂效应、副作用和复杂数据结构的挑战。
• 翻译自动化缺失：将 PBT 转为 Lean 等依赖类型语言，需要同时理解 PBT 的隐含逻辑契约、建模 Python 运行时语义，并处理强类型系统中常见的证明义务，现有 rule-based 或单模型方法几乎无法处理这种多阶段推理。
• 复现性差：缺少开放、可重复的评估流程，导致不同方法间难以公平对比。

技术挑战与业界关注度

该问题的难度源于 "三重鸿沟"：

1. 语义鸿沟：命令式 Python 代码（如可变状态、异常、生成器）必须被形式化地抽象为 Lean 的纯函数式规范，这要求交叉领域知识。
2. 逻辑鸿沟：PBT 中的随机测试逻辑（如 forall + assume）在 Lean 中需转化为全称量化定理，且必须兼容 SMT 或策略式证明。
3. 工程鸿沟：Lean 是一门尚未被广泛使用的依赖类型语言，模型训练数据稀疏，经典代码翻译范式（如 seq2seq）在此几乎失效。

业界对此高度关注：OpenAI、DeepMind 等均已投入 AI 辅助定理证明，而 ARIA 的 Safeguarded AI 等项目明确将真实代码的形式验证列为优先级。

行业类比

这就像当前 AI 编译器（如 Triton）需要理解高层张量运算与底层硬件指令的鸿沟一样，将 PBT 翻译成 Lean 规范本质上是搭建一座从动态软件工程到静态数学证明的桥梁，是实现 AI 自举安全的关键一步。

核心洞察

• **从真实 Python 代码库中挖掘 PBT 并大规模转换为 Lean 规范**：该工作摒弃了主流 benchmark 中常用的合成定理或人工编写的问题，直接从 11,039 个真实世界的 property-based tests 出发，自动翻译成 9,415 个 Lean 4 命题。这使评估更贴近“AI 生成代码需要形式验证”的实际场景，而非常见的玩具定理，强迫模型处理 Python 语义建模、命令式逻辑翻译和依赖类型编程的三重挑战。
• **保留多个非支配性翻译版本以反映真实自动转换的模糊性**：与追求单一“正确”形式化的思路不同，FVSpec 在每个 PBT 上保留约 3 个质量各异的 Lean 尝试，因为缺乏单一质量指标能明确选出最优。这模拟了实际自动验证工具链中规范生成的不确定性，要求证明器或 agent 具备在多个候选规范中辨别或利用最有利版本的能力，相比仅提供确定规范的基准更具难度。
• **将 Lean 4 的类型检查作为近乎完美的自动评分器**：FVSpec 利用依赖类型语言 Lean 的编译器作为 oracle，通过“sorry”占位符将证明义务标注为待完成，使任何生成的证明都能被严格自动判定正确性。这避免了传统评测中人类标注证明正确性带来的主观性和成本，同时 Lean 的丰富类型系统能编码任意高深的数学性质，为 AI 形式验证研究提供了可无限扩展的自动化基准框架。

方法

输入：真实世界属性测试语料

首先从 GitHub 开源 Python 仓库中自动抓取大量属性测试（property-based tests, PBTs），获得 11,039 个原始 PBT 样例，覆盖不同项目、领域及编码风格。这一步骤确保了基准的来源真实性和任务多样性，避免传统形式验证基准中人工构造示例的分布偏移。

关键模块：三代理 LLM 转译管道

将 Python PBT 自动转换为 Lean 4 形式规格的管道由三个 LLM 代理协作完成：

1. 语义解析代理：解析命令式 Python 测试代码，推断其中蕴含的逻辑属性（如“对所有输入，排序后输出有序且长度不变”），并识别需要公理化的副作用（如外部 API、随机数等）。
2. 形式化建模代理：将解析出的属性映射为 Lean 4 中的类型驱动声明。该代理需要处理 Python 动态类型到 Lean 依赖类型（dependently-typed）的语义鸿沟，为 Python 数据构造 Lean 等价模型，并将副作用封装为公理接口（axiomatized interfaces）。
3. 规格合成代理：生成包含 sorry 占位符的定理声明（即“证明义务”），形成无证明的规格说明。当多个尝试（平均约 3 次/PBT）在质量指标上没有显著优势时，保留所有尝试以增加问题多样性。

输出：FVSpec 形式验证基准

最终产出 9,415 个 Lean 4 定理声明（来自 2,772 个原始 PBT，覆盖率达 25%），每个声明均带有难度评分、公理化边界等元信息。这些定理是对真实软件属性的形式刻画，是 AI 模型进行证明生成的挑战目标。论文同时提供了多种自动化达标器和基于模型的证明基线，以推动 AI 辅助形式验证的研究。

与同类方法的差异

不同于以往大多来自竞赛、教科书或手工构造的形式验证基准，FVSpec 直接从真实代码库中自动化提取，使任务更贴近工业级软件质量保障需求；同时，其**面向证明生成（而非仅仅规格推断）**的设定，以及依赖类型语言 Lean 4 的高门槛，构成了独特的挑战。

实验

实验设计

构造 FVSpec 基准分两步：首先自动抓取 GitHub 上真实 Python 仓库中的 11,039 个属性基测试 (PBT)，构成 FVSpec:PBT 数据集；然后设计三代理 LLM 管道（翻译、验证、精炼）将其中的 2,772 个（25%）转换为 9,415 条 Lean 4 规范，保留多个翻译尝试以捕捉质量波动，形成 FVSpec:FV。评估管线通过覆盖率、语法正确率和类型检查通过率等多维质量指标自动筛选，并对样本做难度分级。为建立参照，同时运行多种自动定理证明器与模型驱动的证明生成基线。

关键发现

• 翻译成功率仅 25%：多数 PBT 在建模 Python 语义、推断隐含逻辑属性或应对依赖类型编程时失败，说明现实代码形式化极富挑战。
• 多版本保留策略：平均每个 PBT 产生约 3.4 个 Lean 规范，覆盖不同抽象级别与质量，为后续证明生成提供多样性。
• 现状基线薄弱：当前自动化证明方法在多数任务上成功率很低，验证了整个基准对 AI 模型具有足够的难度和区分度。

与基线对比的解读

FVSpec 区别于现有形式验证基准（如 MiniF2F、CoqGym）的关键在于直接从生产代码的 PBT 出发，而非依赖手工编写的数学定理或玩具示例。这一设计让任务更贴近工业场景，但同时也将验证难度从纯逻辑推理扩展到程序语义建模、语言间的语义鸿沟等工程问题。多代理管道尝试用 LLM 弥合这种鸿沟，但基线证明生成的低成功率揭示出当前模型在掌握依赖类型与复杂不变式上的明显短板。该基准旨在推动 AI 辅助形式验证从“可控的数学问题”向“真实软件保障”迈进，为后续的方法发展和评估提供统一标尺。

行业影响

工业界影响分析

落地场景

形式化验证（FV） 在安全关键领域（如自动驾驶感知模块、金融交易引擎、医疗设备固件）一直有强需求，但手工编写证明成本极高。FVSpec 提供了一条 AI 辅助生成 Lean 4 规范与证明 的新路径，可将已有的 property-based tests (PBTs) 自动转换为形式化定理。这直接赋能以下产品与业务：

• 代码审查与合规平台（如代码质量门禁自动生成形式化证据）
• 智能合约审计工具（自动将合约的 PBTs 转为 Lean 证明，减少人工审计）
• API 测试服务（从客户提供的测试用例自动升维为机器可检验的数学证明）

商业价值

传统 FV 项目的人力成本可达代码开发的 10 倍以上，仅少数大型项目（如 CompCert、seL4）能负担。FVSpec 的 三代理 LLM 翻译管线 将大量样板工作自动化，使形式化验证下沉到普通开发团队。核心价值体现为：

• 降本：减少对专业定理证明工程师的依赖，将 FV 成本降低一个数量级
• 增收：为测试工具厂商提供差异化的“证明生成”增值模块，提升产品 ARPU
• 风险管控：在金融、自动驾驶等领域，形式化证明可以压缩保险费率或降低合规失败导致的罚金

与现有工作流集成

FVSpec 以 Lean 4 作为统一后端，验证结果可机器检查，完美融入现代 DevOps 工具链：

• CI/CD 集成：将 sorry 占位的 Lean 定理作为待证目标放入流水线，由模型自动尝试证明，失败则阻断高风险部署
• IDE 插件：在 VS Code 等环境中利用 Lean 的 Language Server 实时反馈，开发者在编写 PBT 时可一键尝试生成证明
• 测试框架对接：直接与 Python 的 Hypothesis 等 PBT 库关联，形成“测试→规范→证明→回归”的闭环

具体 Use Case

1. 自动驾驶感知算法测试
   感知输出（如 3D 目标检测框）需满足几何与物理一致性约束。用 Hypothesis 编写 PBTs 后，FVSpec 将其转化为关于坐标变换和时序逻辑的 Lean 定理，AI 代理自动证明这些安全约束永成立，替代数千小时的场景仿真回归。

2. 金融交易系统的订单簿一致性验证
   订单匹配引擎的 PBTs（如“成交后总资产守恒”）经自动翻译为 Lean 规范后，AI 辅助完成关键不变性的证明。这为数字资产交易所的合规审计提供不可篡改的数学证据，加速监管审批流程。

局限

• **翻译覆盖率和质量有限**：当前三代理 LLM 流水线仅将 25% 的 PBT 转换为 Lean 规范，且为同一测试保留多个候选正式化，表明模型在建模 Python 语义、推断逻辑属性时仍面临显著挑战。这限制了基准的规模与代表性，可能偏向简单、无副作用的测试，使得生成的正式规范在覆盖真实世界复杂性上存在偏差。
• **公理化接口的脆弱性**：为处理效应ful 代码与外部库，流水线依赖公理化包装（如列表、IO 等）。当这些公理与实际行为不一致或不够完备时，翻译出的规范会变得无意义或极为脆弱。论文在“有效性威胁”中承认了该问题，它直接削弱了形式化规范的可靠性，可能导致下游证明无法成立或与原始 Python 代码脱节。
• **证明生成基线的深度不足**：基准提供的证明生成基线仅覆盖几种自动化和模型方法，缺乏与交互式定理证明（ITP）工具链的深度整合，也未给出证明复杂度的细粒度分类。对比其他形式验证基准（如 miniF2F、CompCert），FVSpec 更侧重于规范翻译，但未能充分展示如何驱动证明自动化技术的实质性进步，对“AI 辅助形式验证”的推动作用目前还停留在数据资源层面。