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 a given 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

翻译：我们针对自动合成两个由语句序列构成的程序间语义等价性证明的问题展开研究。采用抽象语法树（AST）表示程序，其中一组保持语义的重写规则可应用于特定AST模式，从而生成转换后的语义等价程序。在本系统中，若存在一系列重写规则的应用能将一个程序改写为另一个程序，则这两个程序被视为等价。我们提出一种基于Transformer模型的神经网络架构，用于生成程序对间的等价性证明。该系统输出一系列重写操作，通过验证其可应用性即可简单检查序列的有效性。若神经网络未生成有效序列，系统将报告程序非等价，从而从根本上杜绝错误报告等价的情况。我们的系统针对可表示包含函数调用与多类型直线程序的特定语法规则进行了完整实现。为高效训练系统生成此类序列，我们提出一种名为"自监督样本选择"的原创渐进式训练技术。我们深入研究了这种新型训练方法在证明复杂度与长度递增情况下的有效性。我们的系统S4Eq在包含10,000对等价程序的数据集上实现了97%的证明成功率。