# Neural Termination Analysis

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

## Key facts

- Cited by 16 papers in the map (data through 14 Oct 2026).
- Builds on 32 of its 123 references that are in the map.
- First posted on arXiv 7 Feb 2021.

## Builds on (most cited first, 30 of 32)

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Neural Lyapunov Control](https://mlsanity.com/paper/2005.00611/) (2020)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Neuro-Symbolic Program Synthesis](https://mlsanity.com/paper/1611.01855/) (2016)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [Verifying Properties of Binarized Deep Neural Networks](https://mlsanity.com/paper/1709.06662/) (2017)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [Learning Safe Multi-Agent Control with Decentralized Neural Barrier Certificates](https://mlsanity.com/paper/2101.05436/) (2021)
- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)
- [Learning Certified Control using Contraction Metric](https://mlsanity.com/paper/2011.12569/) (2020)
- [An SMT-Based Approach for Verifying Binarized Neural Networks](https://mlsanity.com/paper/2011.02948/) (2020)
- [Reachable Polyhedral Marching (RPM): A Safety Verification Algorithm for Robotic Systems with Deep Neural Network Components](https://mlsanity.com/paper/2011.11609/) (2020)
- [Scalable Verification of Quantized Neural Networks (Technical Report)](https://mlsanity.com/paper/2012.08185/) (2020)
- [Learning Lyapunov Functions for Hybrid Systems](https://mlsanity.com/paper/2012.12015/) (2020)
- [Property Invariant Embedding for Automated Reasoning](https://mlsanity.com/paper/1911.12073/) (2019)
- [CLN2INV: Learning Loop Invariants with Continuous Logic Networks](https://mlsanity.com/paper/1909.11542/) (2019)
- [Termination Analysis by Learning Terminating Programs](https://mlsanity.com/paper/1405.4189/) (2014)
- [Termination Analysis Without the Tears](https://mlsanity.com/paper/2101.09783/) (2021)
- [Automated Verification of Neural Networks: Advances, Challenges and Perspectives](https://mlsanity.com/paper/1805.09938/) (2018)
- [Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models](https://mlsanity.com/paper/2007.03251/) (2020)
- [DynamiTe: Dynamic Termination and Non-termination Proofs](https://mlsanity.com/paper/2010.05747/) (2020)
- [Ranking Templates for Linear Loops](https://mlsanity.com/paper/1401.5338/) (2014)

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

- [Can ChatGPT support software verification?](https://mlsanity.com/paper/2311.02433/) (2023)
- [Neural Abstractions](https://mlsanity.com/paper/2301.11683/) (2023)
- [Neural Model Checking](https://mlsanity.com/paper/2410.23790/) (2024)
- [Bisimulation Learning](https://mlsanity.com/paper/2405.15723/) (2024)
- [NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis](https://mlsanity.com/paper/2401.12131/) (2024)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)
- [SINGA-Easy: An Easy-to-Use Framework for MultiModal Analysis](https://mlsanity.com/paper/2108.02572/) (2021)
- [VisualTextRank: Unsupervised Graph-based Content Extraction for Automating Ad Text to Image Search](https://mlsanity.com/paper/2108.02725/) (2021)
- [Text is NOT Enough: Integrating Visual Impressions into Open-domain Dialogue Generation](https://mlsanity.com/paper/2109.05778/) (2021)
- [Discovering Personalized Semantics for Soft Attributes in Recommender Systems using Concept Activation Vectors](https://mlsanity.com/paper/2202.02830/) (2022)
- [Reinforced MOOCs Concept Recommendation in Heterogeneous Information Networks](https://mlsanity.com/paper/2203.11011/) (2022)
- [Explanation-Guided Fairness Testing through Genetic Algorithm](https://mlsanity.com/paper/2205.08335/) (2022)
- [Using Graph Neural Networks for Program Termination](https://mlsanity.com/paper/2207.14648/) (2022)
- [Tribe or Not? Critical Inspection of Group Differences Using TribalGram](https://mlsanity.com/paper/2303.09664/) (2023)
- [Automated Strategy Invention for Confluence of Term Rewrite Systems](https://mlsanity.com/paper/2411.06409/) (2024)
- [VeRecycle: Reclaiming Guarantees from Probabilistic Certificates for Stochastic Dynamical Systems after Change](https://mlsanity.com/paper/2505.14001/) (2025)

## Abstract (arXiv)

We introduce a novel approach to the automated termination analysis of computer programs: we use neural networks to represent ranking functions. Ranking functions map program states to values that are bounded from below and decrease as a program runs; the existence of a ranking function proves that the program terminates. We train a neural network from sampled execution traces of a program so that the network's output decreases along the traces; then, we use symbolic reasoning to formally verify that it generalises to all possible executions. Upon the affirmative answer we obtain a formal certificate of termination for the program, which we call a neural ranking function. We demonstrate that thanks to the ability of neural networks to represent nonlinear functions our method succeeds over programs that are beyond the reach of state-of-the-art tools. This includes programs that use disjunctions in their loop conditions and programs that include nonlinear expressions.