Daily Arxiv

This is a page that curates AI-related papers published worldwide.
All content here is summarized using Google Gemini and operated on a non-profit basis.
Copyright for each paper belongs to the authors and their institutions; please make sure to credit the source when sharing.

Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models

Created by
  • Haebom

Author

Ruibang Liu, Guoqiang Li, Minyu Chen, Ling-I Wu, Jingyu Ke

Outline

This paper proposes a novel tool, ACInv, to address the challenges of automated program verification, which is crucial for building reliable software, especially when analyzing real-world programs with complex data structures and control flow. ACInv generates loop invariants by combining static analysis with a large-scale language model (LLM). It extracts loop information through static analysis and embeds it in the LLM prompt. It then uses an LLM-based evaluator to verify the generated invariants and strengthen, weaken, or reject them to obtain optimal invariants. Experimental results show that ACInv outperforms existing tools on datasets containing data structures, while maintaining comparable performance to the state-of-the-art tool, AutoSpec, on numerical programs without data structures. ACInv solves 21% more examples than AutoSpec across the entire dataset and generates reference data structure templates.

Takeaways, Limitations

•
Takeaways:
◦
We present a novel method that effectively solves the problem of generating loop invariants for complex programs by combining static analysis and LLM.
◦
It outperforms existing tools in programs that include data structures.
◦
Provides the ability to create reference data structure templates.
◦
We verify and improve the accuracy of invariants using an LLM-based evaluator.
•
Limitations:
◦
Performance for numerical programs without data structures is comparable to state-of-the-art tools, but does not show overwhelming performance improvements.
◦
Since it depends on the performance of LLM, limitations of LLM may affect the performance of ACInv.
◦
Performance may vary depending on the scope and diversity of the experimental dataset. More extensive experiments may be required.
👍
Made with Slashpage