Next Steps in LLM-Supported Java Verification
This work addresses the challenge of ensuring correctness in LLM-generated code specifications for software verification, though it appears incremental as it builds on recent methods.
The paper tackles the problem of generating correct specification annotations for Java verification using unreliable Large Language Models, showing early results that a rigorous verification toolset can reliably elicit correct annotations from LLMs.
Recent work has shown that Large Language Models (LLMs) are not only a suitable tool for code generation but also capable of generating annotation-based code specifications. Scaling these methodologies may allow us to deduce provable correctness guarantees for large-scale software systems. In comparison to other LLM tasks, the application field of deductive verification has the notable advantage of providing a rigorous toolset to check LLM-generated solutions. This short paper provides early results on how this rigorous toolset can be used to reliably elicit correct specification annotations from an unreliable LLM oracle.