VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean
This addresses the need for realistic benchmarks in software verification for researchers and developers, though it is incremental as it builds on existing formal verification and LLM evaluation efforts.
The authors tackled the problem of evaluating large language models and specialized provers in formal verification by introducing VeriSoftBench, a benchmark of 500 Lean 4 proof obligations from open-source formal-methods developments, and found that existing provers tuned for mathematics transfer poorly, with success rates strongly correlated to dependency complexity.
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.