Proving Equivalence Between Complex Expressions Using Graph-to-Sequence Neural Models

TL;DR

This paper introduces a graph-to-sequence neural model that automatically generates proof sequences to verify the equivalence of complex algebraic expressions, ensuring correctness and efficiency.

Contribution

It presents a novel neural approach for program equivalence using rewrite rules, with a system that guarantees correctness and achieves high accuracy on complex expressions.

Findings

93% accuracy on 10,000 test pairs

Guarantees correctness for all true negatives

Zero false positives by design

Abstract

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.