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

arXiv: https://arxiv.org/abs/2106.02452 · HTML: https://mlsanity.com/paper/2106.02452/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 22 of its 66 references that are in the map.
- First posted on arXiv 1 Jun 2021.

## Builds on (most cited first, 22 of 22)

- [Neural Machine Translation by Jointly Learning to Align and Translate](https://mlsanity.com/paper/1409.0473/) (2014)
- [Distributed Representations of Words and Phrases and their Compositionality](https://mlsanity.com/paper/1310.4546/) (2013)
- [A Comprehensive Survey on Graph Neural Networks](https://mlsanity.com/paper/1901.00596/) (2019)
- [Hindsight Experience Replay](https://mlsanity.com/paper/1707.01495/) (2017)
- [Effective Approaches to Attention-based Neural Machine Translation](https://mlsanity.com/paper/1508.04025/) (2015)
- [Gated Graph Sequence Neural Networks](https://mlsanity.com/paper/1511.05493/) (2015)
- [Deep Learning for Symbolic Mathematics](https://mlsanity.com/paper/1912.01412/) (2019)
- [OpenNMT: Open-source Toolkit for Neural Machine Translation](https://mlsanity.com/paper/1709.03815/) (2017)
- [code2vec: Learning Distributed Representations of Code](https://mlsanity.com/paper/1803.09473/) (2018)
- [A Survey of Machine Learning for Big Code and Naturalness](https://mlsanity.com/paper/1709.06182/) (2017)
- [Learning to Represent Programs with Graphs](https://mlsanity.com/paper/1711.00740/) (2017)
- [Professor Forcing: A New Algorithm for Training Recurrent Networks](https://mlsanity.com/paper/1610.09038/) (2016)
- [SequenceR: Sequence-to-Sequence Learning for End-to-End Program Repair](https://mlsanity.com/paper/1901.01808/) (2018)
- [An Empirical Study on Learning Bug-Fixing Patches in the Wild via Neural Machine Translation](https://mlsanity.com/paper/1812.08693/) (2018)
- [Neural Network-based Graph Embedding for Cross-Platform Binary Code Similarity Detection](https://mlsanity.com/paper/1708.06525/) (2017)
- [Graph-to-Sequence Learning using Gated Graph Neural Networks](https://mlsanity.com/paper/1806.09835/) (2018)
- [INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving](https://mlsanity.com/paper/2007.02924/) (2020)
- [DIRE: A Neural Approach to Decompiled Identifier Naming](https://mlsanity.com/paper/1909.09029/) (2019)
- [An Empirical Evaluation of Rule Extraction from Recurrent Neural Networks](https://mlsanity.com/paper/1709.10380/) (2017)
- [Learning to Prove from Synthetic Theorems](https://mlsanity.com/paper/2006.11259/) (2020)
- [Context2Name: A Deep Learning-Based Approach to Infer Natural Variable Names from Usage Contexts](https://mlsanity.com/paper/1809.05193/) (2018)
- [Learning dynamic polynomial proofs](https://mlsanity.com/paper/1906.01681/) (2019)

## Built on by (most cited first, 2 of 2)

- [Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules](https://mlsanity.com/paper/2109.10476/) (2021)
- [Integrating Large Language Models and Reinforcement Learning for Non-Linear Reasoning](https://mlsanity.com/paper/2410.13501/) (2024)

## Abstract (arXiv)

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.