LLM-generated code specs still struggle with formal verification
Large language models fail to reliably generate formal program specifications despite advances in theorem proving.
A new Rocq-based framework called Coins evaluates how well LLMs generate formal program specifications by instantiating them on trusted test cases and generating concrete proof obligations. In a large-scale study on HumanEval using a curated set of human-written Rocq specifications, specification generation proves to be a formidable challenge, and verification complexity can obscure genuine differences in specification quality. The findings suggest that accurate specification evaluation—not model scaling alone—is central to understanding LLM power for specification synthesis, and that test-case-based formal reasoning offers a more faithful and discriminative measure of progress.
- Coins is a new Rocq-based evaluation framework designed to assess specification quality by instantiating specifications on trusted test cases.
- Researchers tested 164 HumanEval problems and found LLMs struggle to generate reliable formal specifications.
- The study emphasizes that evaluation methodology—not just model size—is critical to advancing LLM capabilities in formal verification.
Why It Matters
Formal program specifications are vital for software correctness, but current LLMs cannot reliably generate them—limiting adoption in critical systems.