LLM-guided Predicate Discovery and Data Augmentation for Learning Likely Program Invariants

We present a framework that leverages large language models (LLMs) to automatically discover informative predicates and synthesize high-quality augmented data for learning likely program invariants. By integrating LLM-generated predicate suggestions with targeted trace sampling, our approach improves classifier accuracy and generalization while reducing manual feature-engineering effort. Extensive experiments on a suite of benchmark programs demonstrate that our method yields tighter invariants than state-of-the-art template-based and decision-tree learners, often with an order-of-magnitude reduction in training samples.

In ACM/SIGAPP Symposium on Applied Computing (SAC 2025)