Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914438507921408 |
|---|---|
| author | Wei, Anjiang Sun, Tianran Suresh, Tarun Wu, Haoze Wang, Ke Aiken, Alex |
| author_facet | Wei, Anjiang Sun, Tianran Suresh, Tarun Wu, Haoze Wang, Ke Aiken, Alex |
| contents | Program verification relies on loop invariants, yet automatically discovering strong invariants remains a long-standing challenge. We investigate whether large language models (LLMs) can accelerate program verification by generating useful loop invariants. We introduce Quokka, an evaluation-oriented framework for LLM-based invariant synthesis that provides sound evaluation and achieves state-of-the-art performance. Unlike prior work that treats LLM outputs as noisy symbolic material requiring substantial post-processing, Quokka adopts a simpler and evaluation-centric design that directly validates whether each LLM-generated invariant helps prove the target assertion. We construct a benchmark of 866 instances derived from SV-COMP and evaluate 9 state-of-the-art LLMs across multiple model families. We demonstrate that supervised fine-tuning and Best-of-N sampling yield measurable improvements, and we show that Quokka consistently outperforms prior LLM-based verifiers. Our code and data are publicly available at https://github.com/Anjiang-Wei/Quokka |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_21629 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis Wei, Anjiang Sun, Tianran Suresh, Tarun Wu, Haoze Wang, Ke Aiken, Alex Programming Languages Artificial Intelligence Computation and Language Machine Learning Program verification relies on loop invariants, yet automatically discovering strong invariants remains a long-standing challenge. We investigate whether large language models (LLMs) can accelerate program verification by generating useful loop invariants. We introduce Quokka, an evaluation-oriented framework for LLM-based invariant synthesis that provides sound evaluation and achieves state-of-the-art performance. Unlike prior work that treats LLM outputs as noisy symbolic material requiring substantial post-processing, Quokka adopts a simpler and evaluation-centric design that directly validates whether each LLM-generated invariant helps prove the target assertion. We construct a benchmark of 866 instances derived from SV-COMP and evaluate 9 state-of-the-art LLMs across multiple model families. We demonstrate that supervised fine-tuning and Best-of-N sampling yield measurable improvements, and we show that Quokka consistently outperforms prior LLM-based verifiers. Our code and data are publicly available at https://github.com/Anjiang-Wei/Quokka |
| title | Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis |
| topic | Programming Languages Artificial Intelligence Computation and Language Machine Learning |
| url | https://arxiv.org/abs/2509.21629 |