构建首个面向代码库级形式化验证的Lean 4基准测试
VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean
- 从真实开源项目中提取500个带上下文依赖的证明任务
- 发现数学类模型在代码库场景下表现显著下降，依赖链越长越难解
- 限定依赖闭包可提升性能，但仍有巨大优化空间
大型语言模型在交互式定理证明（尤其是Lean）中已取得显著进展，但现有基准大多基于Mathlib数学库，而软件形式化验证通常依赖定义丰富的代码库和大量项目专属库。本文提出VeriSoftBench，一个包含500个来自开源形式化项目的真实Lean 4证明目标的基准，保留了完整的代码库上下文与跨文件依赖关系。对前沿LLM与专用证明器的评估发现：首先，针对Mathlib优化的证明器在代码库场景下迁移能力差；其次，成功率与传递依赖深度强相关，多跳依赖任务更难解决；第三，仅提供证明所需依赖闭包可提升性能，但仍远低于理想水平。该基准及评估套件已开源。
原文摘要 · Abstract (English)
Large language models have achieved striking results in interactive theorem proving, particularly in Lean. However, most benchmarks for LLM-based proof automation are drawn from mathematics in the Mathlib ecosystem, whereas proofs in software verification are developed inside definition-rich codebases with substantial project-specific libraries. We introduce VeriSoftBench, a benchmark of 500 Lean 4 proof obligations drawn from open-source formal-methods developments and packaged to preserve realistic repository context and cross-file dependencies. Our evaluation of frontier LLMs and specialized provers yields three observations. First, provers tuned for Mathlib-style mathematics transfer poorly to this repository-centric setting. Second, success is strongly correlated with transitive repository dependence: tasks whose proofs draw on large, multi-hop dependency closures are less likely to be solved. Third, providing curated context restricted to a proof's dependency closure improves performance relative to exposing the full repository, but nevertheless leaves substantial room for improvement. Our benchmark and evaluation suite are released at https://github.com/utopia-group/VeriSoftBench.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。