# CLN2INV: Learning Loop Invariants with Continuous Logic Networks

arXiv: https://arxiv.org/abs/1909.11542 · HTML: https://mlsanity.com/paper/1909.11542/

## Key facts

- Cited by 20 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 25 Sep 2019.

## Built on by (most cited first, 20 of 20)

- [InCoder: A Generative Model for Code Infilling and Synthesis](https://mlsanity.com/paper/2204.05999/) (2022)
- [Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?](https://mlsanity.com/paper/2310.01831/) (2023)
- [Finding Inductive Loop Invariants using Large Language Models](https://mlsanity.com/paper/2311.07948/) (2023)
- [Ranking LLM-Generated Loop Invariants for Program Verification](https://mlsanity.com/paper/2310.09342/) (2023)
- [Goal-Aware Neural SAT Solver](https://mlsanity.com/paper/2106.07162/) (2021)
- [FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving](https://mlsanity.com/paper/2406.14408/) (2024)
- [Neural Termination Analysis](https://mlsanity.com/paper/2102.03824/) (2021)
- [Learning Security Classifiers with Verified Global Robustness Properties](https://mlsanity.com/paper/2105.11363/) (2021)
- [Leveraging Large Language Models for Automated Proof Synthesis in Rust](https://mlsanity.com/paper/2311.03739/) (2023)
- [Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models](https://mlsanity.com/paper/2412.10483/) (2024)
- [Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?](https://mlsanity.com/paper/2510.12702/) (2025)
- [Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis](https://mlsanity.com/paper/2205.14229/) (2022)
- [Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis](https://mlsanity.com/paper/2509.21629/) (2025)
- [NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis](https://mlsanity.com/paper/2401.12131/) (2024)
- [Toward Neural-Network-Guided Program Synthesis and Verification](https://mlsanity.com/paper/2103.09414/) (2021)
- [Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes](https://mlsanity.com/paper/2205.14943/) (2022)
- [Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning](https://mlsanity.com/paper/2107.09766/) (2021)
- [Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems](https://mlsanity.com/paper/2312.10842/) (2023)
- [AutoICE: Automatically Synthesizing Verifiable C Code via LLM-driven Evolution](https://mlsanity.com/paper/2512.07501/) (2025)
- [Privilege and confidentiality in generative AI workflows](https://mlsanity.com/paper/2607.05479/) (2026)

## Abstract (arXiv)

Program verification offers a framework for ensuring program correctness and therefore systematically eliminating different classes of bugs. Inferring loop invariants is one of the main challenges behind automated verification of real-world programs which often contain many loops. In this paper, we present Continuous Logic Network (CLN), a novel neural architecture for automatically learning loop invariants directly from program execution traces. Unlike existing neural networks, CLNs can learn precise and explicit representations of formulas in Satisfiability Modulo Theories (SMT) for loop invariants from program execution traces. We develop a new sound and complete semantic mapping for assigning SMT formulas to continuous truth values that allows CLNs to be trained efficiently. We use CLNs to implement a new inference system for loop invariants, CLN2INV, that significantly outperforms existing approaches on the popular Code2Inv dataset. CLN2INV is the first tool to solve all 124 theoretically solvable problems in the Code2Inv dataset. Moreover, CLN2INV takes only 1.1 seconds on average for each problem, which is 40 times faster than existing approaches. We further demonstrate that CLN2INV can even learn 12 significantly more complex loop invariants than the ones required for the Code2Inv dataset.