Benchmarking LLMs for Invariant Generation | Anjiang Wei (Stanford)

Anjiang Wei from Stanford will be presenting his paper titled "InvBench: Can LLMs Accelerate Program Verification with Invariant Synthesis?”

https://arxiv.org/abs/2509.21629.
Abstract: Program verification relies on loop invariants, yet automatically discovering strong invariants remains a long-standing challenge. This work introduces InvBench, a framework for evaluating LLMs on invariant synthesis. Unlike previous methods, this approach uses a verifier-based decision procedure with a formal soundness guarantee and assesses not only the correctness of invariants but also the speedup they provide in the verification process.