一句话：用神经网络表示 ranking function，并经符号验证为程序提供终止性证书。
本文研究程序的自动终止性分析，核心是寻找并验证 ranking function（排名函数）：它将程序状态映射为有下界的值，并随程序执行递减，从而证明终止。作者提出用神经网络表示候选 ranking function，先从程序采样执行轨迹进行训练，使网络输出沿轨迹递减；随后利用符号推理形式化验证该网络对所有可能执行都满足递减条件。验证成功即可得到程序的终止性证书，称为神经 ranking function。实验表明，得益于神经网络表达非线性函数的能力，该方法能处理现有最先进工具难以覆盖的程序，例如循环条件含析取以及包含非线性表达式的程序。
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.