{"ID":2866238,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2509.21629","arxiv_id":"2509.21629","title":"Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis","abstract":"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","short_abstract":"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-b...","url_abs":"https://arxiv.org/abs/2509.21629","url_pdf":"https://arxiv.org/pdf/2509.21629v3","authors":"[\"Anjiang Wei\",\"Tianran Sun\",\"Tarun Suresh\",\"Haoze Wu\",\"Ke Wang\",\"Alex Aiken\"]","published":"2025-09-25T21:47:02Z","proceeding":"cs.PL","tasks":"[\"cs.PL\",\"cs.AI\",\"cs.CL\",\"cs.LG\"]","methods":"[\"Large Language Model\",\"Language Model\"]","has_code":false,"code_links":[{"ID":609352,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_id":2866238,"paper_url":"https://arxiv.org/abs/2509.21629","paper_title":"Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis","repo_url":"https://github.com/Anjiang-Wei/Quokka","is_official":false,"mentioned_in_paper":false,"mentioned_in_github":true,"github_stars":0}]}