Reproduce “ClassInvGen: Class Invariant Synthesis using Large Language Models” on OpenResearch

About this paper

Chuyue Sun, Viraj Agashe, Saikat Chakraborty, Jubi Taneja, Clark Barrett, David Dill, Xiaokang Qiu, Shuvendu K. Lahiri

ClassInvGen, developed by researchers from Stanford, Microsoft Research, and Purdue, automates the synthesis of executable class invariants for C++ by combining Large Language Models with static analysis and dynamic testing. The system generates high-quality invariants, achieving 100% correctness and detecting an average of 11.2% more mutants than unit tests alone on a benchmark of C++ data structures and Z3 SMT solver classes.

Key insights

• A neuro-symbolic approach, combining LLM generation with static analysis for context and dynamic testing for validation, effectively mitigates the limitations of purely neural or symbolic methods for invariant synthesis.
• The co-generation of invariant candidates and filtering test suites, coupled with a feedback-driven refinement loop, significantly improves the correctness and robustness of generated invariants.
• Large Language Models, leveraging broad contextual understanding and code semantics, can generate more expressive and less trivial class invariants than template-based dynamic inference tools like Daikon.

Summary by alphaXiv.