[Paper] VeriSoftBench：针对 Lean 的仓库规模形式化验证基准

Source: arXiv - 2602.18307v1

（请提供您希望翻译的具体文本内容，我将按照要求保留源链接、格式和技术术语，仅翻译正文部分。）

概述

本文介绍了 VeriSoftBench，一个由 500 条 Lean 4 证明义务组成的新基准套件，来源于真实的开源软件验证项目。不同于现有聚焦纯数学（例如 Mathlib）的 LLM 驱动的定理证明基准，该数据集保留了完整的仓库上下文——跨文件导入、自定义库以及深层依赖图——因此为基于语言模型的证明器和传统自动化证明器提供了更真实的测试平台。

关键贡献

• Repository‑scale benchmark：从多样的公开可用形式化方法代码库中抽取的 500 条 Lean 4 验证任务。
• Context‑preserving packaging：每个任务都随其完整的传递依赖闭包一起打包，能够进行可复现的实验，反映真实的开发环境。
• Comprehensive evaluation：对前沿的大语言模型（如 GPT‑4、Claude）和专用证明器进行基准测试，揭示了从 Mathlib‑style 数学到软件验证代码的迁移中存在的系统性差距。
• Empirical insights：关于可迁移性、依赖复杂性以及为证明自动化提供精心策划上下文价值的三大核心观察。
• Open‑source release：基准数据、评估脚本和基线结果已在 GitHub 上公开发布。

方法论

1. 数据收集 – 作者挖掘了流行的 Lean 4 验证仓库（例如编译器验证、操作系统内核以及安全关键库的验证）。他们提取了尚未自动证明的单个 theorem/lemma 声明。
2. 依赖提取 – 对每个证明义务进行静态分析，识别出所有导入的模块、定义和用于类型检查该声明的引理。完整的传递闭包被打包为一个自包含的 Lean 项目。
3. 基准设计 – 根据依赖闭包的大小（小型、中型、大型）将任务划分为三个难度层级。
4. 评估流程 –
   • 基于 LLM 的证明器：构造提示，将目标声明连同整个仓库、精选的依赖闭包或不提供额外上下文一起输入。LLM 生成证明脚本，随后由 Lean 进行类型检查。
   • 专用证明器：使用 leanprover-community/lean4 中的 simp、omega 以及外部 SAT/SMT 后端等工具，在相同的上下文设置下运行。
5. 度量指标 – 记录成功率（证明完整通过类型检查）、证明时间以及 LLM 提示的 token 使用量。

结果与发现

• 转移差距：在 Mathlib 证明上表现出色的工具在面对以仓库为中心的验证任务时成功率显著下降。
• 依赖深度重要：需要大量传递导入的证明其解决概率约为其他的三分之一。
• 精选上下文有帮助：仅提供最小依赖闭包相较于完整仓库可将 LLM 性能提升约 50 %，但绝对成功率仍然有限，表明在更智能的上下文选择或推理机制方面仍有很大提升空间。

实际意义

• 面向工业规模验证的工具链：构建形式化验证软件的公司（例如安全关键驱动、密码学库）不能再仅依赖 “Mathlib‑only” 基准来评估 LLM 辅助证明自动化的准备程度。VeriSoftBench 提供了一个更贴近实际的衡量标准。
• 上下文管理 API：研究结果表明，IDE 和 CI 流水线应当集成自动化的依赖裁剪工具，只向证明器提供必要的 Lean 文件，从而降低 LLM API 的 token 成本并提升响应延迟。
• 混合证明器架构：从精心挑选的上下文中获得的适度提升暗示，采用两阶段方法——首先使用快速的静态分析器计算最小闭包，然后交给 LLM 或 SMT 后端——可能会成为验证流水线的标准模式。
• 基于基准的研究：开发新提示策略、检索增强生成或领域特定微调的研究者，现在可以针对一个反映生产代码库复杂度的数据集进行评估，从而加速可用验证助理的研发进程。

限制与未来工作

• 领域覆盖：虽然 500 项任务跨越了多个验证项目，但基准仍偏向学术开源仓库；工业专有代码可能呈现出更为丰富的依赖图。
• 静态依赖提取：当前方法假设所有所需的 import 都能被静态发现；Lean 中的动态元编程模式可能隐藏额外的需求。
• LLM 提示范围：仅测试了少数领先的 LLM；未来工作可以探索链式思考提示、工具使用扩展（例如自动调用 Lean 的 simp），或在验证特定语料上进行微调。
• 度量广度：成功率是二元的；未衡量更丰富的指标，如证明长度、人类可读性或下游维护成本。

作者计划扩展 VeriSoftBench，加入更多项目，增加多语言支持（如 Coq、Isabelle），并提供排行榜以跟踪社区整体进展。

作者

• Yutong Xin
• Qiaochu Chen
• Greg Durrett
• Işil Dillig

论文信息

• arXiv ID: 2602.18307v1
• 分类: cs.SE, cs.CL, cs.LG, cs.PL
• 出版日期: 2026年2月20日
• PDF: 下载 PDF