  We target the problem of provably computing the equivalence between two
complex expression trees. To this end, we formalize the problem of equivalence
between two such programs as finding a set of semantics-preserving rewrite
rules from one into the other, such that after the rewrite the two programs are
structurally identical, and therefore trivially equivalent.We then develop a
graph-to-sequence neural network system for program equivalence, trained to
produce such rewrite sequences from a carefully crafted automatic example
generation algorithm. We extensively evaluate our system on a rich multi-type
linear algebra expression language, using arbitrary combinations of 100+
graph-rewriting axioms of equivalence. Our machine learning system guarantees
correctness for all true negatives, and ensures 0 false positive by design. It
outputs via inference a valid proof of equivalence for 93% of the 10,000
equivalent expression pairs isolated for testing, using up to 50-term
expressions. In all cases, the validity of the sequence produced and therefore
the provable assertion of program equivalence is always computable, in
negligible time.
