AI RESEARCH
Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis
arXiv CS.LG
•
ArXi:2509.21629v3 Announce Type: replace-cross 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