# Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 32 of its 103 references that are in the map.
- First posted on arXiv 22 Sep 2021.

## Builds on (most cited first, 30 of 32)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Scaling Laws for Neural Language Models](https://mlsanity.com/paper/2001.08361/) (2020)
- [Sequence to Sequence Learning with Neural Networks](https://mlsanity.com/paper/1409.3215/) (2014)
- [Decision Transformer: Reinforcement Learning via Sequence Modeling](https://mlsanity.com/paper/2106.01345/) (2021)
- [Google's Neural Machine Translation System: Bridging the Gap between Human and Machine Translation](https://mlsanity.com/paper/1609.08144/) (2016)
- [Hindsight Experience Replay](https://mlsanity.com/paper/1707.01495/) (2017)
- [Abstractive Text Summarization Using Sequence-to-Sequence RNNs and Beyond](https://mlsanity.com/paper/1602.06023/) (2016)
- [An Empirical Investigation of Catastrophic Forgetting in Gradient-Based Neural Networks](https://mlsanity.com/paper/1312.6211/) (2013)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [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)
- [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)
- [Self-Supervised Bug Detection and Repair](https://mlsanity.com/paper/2105.12787/) (2021)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)
- [Neural Program Repair with Execution-based Backpropagation](https://mlsanity.com/paper/2105.04123/) (2021)
- [Self-Supervised Contrastive Learning for Code Retrieval and Summarization via Semantic-Preserving Transformations](https://mlsanity.com/paper/2009.02731/) (2020)
- [On the Generalizability of Neural Program Models with respect to Semantic-Preserving Program Transformations](https://mlsanity.com/paper/2008.01566/) (2020)
- [DIRE: A Neural Approach to Decompiled Identifier Naming](https://mlsanity.com/paper/1909.09029/) (2019)
- [Neural Transfer Learning for Repairing Security Vulnerabilities in C Code](https://mlsanity.com/paper/2104.08308/) (2021)
- [An Empirical Evaluation of Rule Extraction from Recurrent Neural Networks](https://mlsanity.com/paper/1709.10380/) (2017)
- [Generating Bug-Fixes Using Pretrained Transformers](https://mlsanity.com/paper/2104.07896/) (2021)
- [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)
- [Recognizing and Verifying Mathematical Equations using Multiplicative Differential Neural Units](https://mlsanity.com/paper/2104.02899/) (2021)
- [Incremental Unsupervised Domain-Adversarial Training of Neural Networks](https://mlsanity.com/paper/2001.04129/) (2020)
- [Equivalence of Dataflow Graphs via Rewrite Rules Using a Graph-to-Sequence Neural Model](https://mlsanity.com/paper/2002.06799/) (2020)

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

- [NExT: Teaching Large Language Models to Reason about Code Execution](https://mlsanity.com/paper/2404.14662/) (2024)
- [Disproving Program Equivalence with LLMs](https://mlsanity.com/paper/2502.18473/) (2025)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)

## Abstract (arXiv)

We target the problem of automatically synthesizing proofs of semantic equivalence between two programs made of sequences of statements. We represent programs using abstract syntax trees (AST), where a given set of semantics-preserving rewrite rules can be applied on a specific AST pattern to generate a transformed and semantically equivalent program. In our system, two programs are equivalent if there exists a sequence of application of these rewrite rules that leads to rewriting one program into the other. We propose a neural network architecture based on a transformer model to generate proofs of equivalence between program pairs. The system outputs a sequence of rewrites, and the validity of the sequence is simply checked by verifying it can be applied. If no valid sequence is produced by the neural network, the system reports the programs as non-equivalent, ensuring by design no programs may be incorrectly reported as equivalent. Our system is fully implemented for one single grammar which can represent straight-line programs with function calls and multiple types. To efficiently train the system to generate such sequences, we develop an original incremental training technique, named self-supervised sample selection. We extensively study the effectiveness of this novel training approach on proofs of increasing complexity and length. Our system, S4Eq, achieves 97% proof success on a curated dataset of 10,000 pairs of equivalent programs.