# Horn-ICE Learning for Synthesizing Invariants and Contracts

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

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Dec 2017.

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

- [Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis](https://mlsanity.com/paper/2509.21629/) (2025)
- [Engineering an Efficient Boolean Functional Synthesis Engine](https://mlsanity.com/paper/2108.05717/) (2021)
- [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)
- [LLM For Loop Invariant Generation and Fixing: How Far Are We?](https://mlsanity.com/paper/2511.06552/) (2025)
- [Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning](https://mlsanity.com/paper/2107.09766/) (2021)
- [Data-driven Verification of Procedural Programs with Integer Arrays](https://mlsanity.com/paper/2505.15958/) (2025)
- [Not All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMs](https://mlsanity.com/paper/2603.15510/) (2026)
- [Verification Modulo Tested Library Contracts](https://mlsanity.com/paper/2604.15533/) (2026)
- [Privilege and confidentiality in generative AI workflows](https://mlsanity.com/paper/2607.05479/) (2026)
- [Towards Certificate-Driven Software Porting: A Self-Improving Agentic Harness for Scientific Program Optimization](https://mlsanity.com/paper/2609.34069/) (2026)

## Abstract (arXiv)

We design learning algorithms for synthesizing invariants using Horn implication counterexamples (Horn-ICE), extending the ICE-learning model. In particular, we describe a decision-tree learning algorithm that learns from Horn-ICE samples, works in polynomial time, and uses statistical heuristics to learn small trees that satisfy the samples. Since most verification proofs can be modeled using Horn clauses, Horn-ICE learning is a more robust technique to learn inductive annotations that prove programs correct. Our experiments show that an implementation of our algorithm is able to learn adequate inductive invariants and contracts efficiently for a variety of sequential and concurrent programs.