VeriSoftBench: 仓库级形式验证基准测试用于Lean
VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean
AI总结：
VeriSoftBench通过500个Lean 4证明义务评估LLM和证明器在仓库级形式验证中的表现，揭示了依赖闭包对证明成功率的影响。
摘要：
大型语言模型在交互式定理证明中取得了显著成果，尤其是在Lean中。然而，大多数基于LLM的证明自动化基准测试大多来自Mathlib生态系统中的数学，而软件验证中的证明是在具有大量项目特定库的定义丰富的代码库中开发的。我们引入了VeriSoftBench，这是一个包含500个Lean 4证明义务的基准测试，这些证明义务来自开源的形式化方法开发，并打包以保持现实的仓库上下文和跨文件依赖关系。我们对前沿LLM和专用证明器的评估得出三个观察结果。第一，针对Mathlib风格数学优化的证明器在这种仓库中心设置中表现不佳。第二，成功与转置仓库依赖性密切相关：那些证明依赖于大型、多跳依赖闭包的任务更不可能被解决。第三，提供经过筛选的上下文，仅限于证明的依赖闭包，可以提高性能，相对于暴露完整的仓库，但仍然有相当大的改进空间。我们的基准测试和评估套件已发布在https://github.com/utopia-group/VeriSoftBench。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
