Proving Equivalence Between Complex Expressions Using Graph-to-Sequence Neural Models
This addresses the challenge of automated program verification for complex expressions, offering a reliable method for domains like linear algebra, though it is incremental as it builds on existing graph-to-sequence models and rewrite rule frameworks.
The paper tackles the problem of proving equivalence between complex expression trees by developing a graph-to-sequence neural network system that generates semantics-preserving rewrite sequences, achieving 93% success on 10,000 equivalent pairs with zero false positives and guaranteed correctness for true negatives.
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.