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.