# Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 24 of its 52 references that are in the map.
- First posted on arXiv 16 Jul 2021.

## Builds on (most cited first, 24 of 24)

- [code2vec: Learning Distributed Representations of Code](https://mlsanity.com/paper/1803.09473/) (2018)
- [Learning to Represent Programs with Graphs](https://mlsanity.com/paper/1711.00740/) (2017)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Leveraging Grammar and Reinforcement Learning for Neural Program Synthesis](https://mlsanity.com/paper/1805.04276/) (2018)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)
- [Deep Network Guided Proof Search](https://mlsanity.com/paper/1701.06972/) (2017)
- [Premise Selection for Theorem Proving by Deep Graph Embedding](https://mlsanity.com/paper/1709.09994/) (2017)
- [Neural-Guided Deductive Search for Real-Time Program Synthesis from Examples](https://mlsanity.com/paper/1804.01186/) (2018)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving](https://mlsanity.com/paper/1703.00426/) (2017)
- [Can Neural Networks Understand Logical Entailment?](https://mlsanity.com/paper/1802.08535/) (2018)
- [CLN2INV: Learning Loop Invariants with Continuous Logic Networks](https://mlsanity.com/paper/1909.11542/) (2019)
- [SMT-based Model Checking for Recursive Programs](https://mlsanity.com/paper/1405.4028/) (2014)
- [Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning](https://mlsanity.com/paper/1807.08058/) (2018)
- [Horn-ICE Learning for Synthesizing Invariants and Contracts](https://mlsanity.com/paper/1712.09418/) (2017)
- [Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning](https://mlsanity.com/paper/1811.00796/) (2018)
- [Overfitting in Synthesis: Theory and Practice (Extended Version)](https://mlsanity.com/paper/1905.07457/) (2019)
- [Learning Invariants using Decision Trees](https://mlsanity.com/paper/1501.04725/) (2015)
- [Program Verification via Predicate Constraint Satisfiability Modulo Theories](https://mlsanity.com/paper/2007.03656/) (2020)
- [Decision Tree Learning in CEGIS-Based Termination Analysis](https://mlsanity.com/paper/2104.11463/) (2021)
- [Constraint-based Relational Verification](https://mlsanity.com/paper/2106.02628/) (2021)

## Abstract (arXiv)

Loop-invariant synthesis is the basis of program verification. Due to the undecidability of the problem in general, a tool for invariant synthesis necessarily uses heuristics. Despite the common belief that the design of heuristics is vital for the performance of a synthesizer, heuristics are often engineered by their developers based on experience and intuition, sometimes in an ad-hoc manner. In this work, we propose an approach to systematically learning heuristics for template-based CounterExample-Guided Inductive Synthesis (CEGIS) with reinforcement learning. As a concrete example, we implement the approach on top of PCSat, which is an invariant synthesizer based on template-based CEGIS. Experiments show that PCSat guided by the heuristics learned by our framework not only outperforms existing state-of-the-art CEGIS-based solvers such as HoICE and the neural solver Code2Inv, but also has slight advantages over non-CEGIS-based solvers such as Eldarica and Spacer in linear Constrained Horn Clause (CHC) solving.