Abstract: We introduce a novel approach to the automated termination analysis of
computer programs: we train neural networks to act as ranking functions.
Ranking functions map program states to values that are bounded from below and
decrease as the program runs. The existence of a valid ranking function proves
that the program terminates. While in the past ranking functions were usually
constructed using static analysis, our method learns them from sampled
executions. We train a neural network so that its output decreases along
execution traces as a ranking function would; then, we use formal reasoning to
verify whether it generalises to all possible executions. We present a custom
loss function for learning lexicographic ranking functions and use
satisfiability modulo theories for verification. Thanks to the ability of
neural networks to generalise well, our method succeeds over a wide variety of
programs. This includes programs that use data structures from standard
libraries. We built a prototype analyser for Java bytecode and show the
efficacy of our method over a standard dataset of benchmarks.