下载PDF摘要：在这项工作中，我们的目标是可证明地计算表示为数据流图的两个程序之间的等价性。为此，我们将两个程序之间的等价问题形式化为找到一组从一个程序到另一个程序的保持语义的重写规则，使得在重写之后，两个程序在结构上是相同的，因此是基本等价的。然后，我们开发了第一个用于程序等价的图到序列神经网络系统，经过训练，可以从精心设计的自动示例生成算法中生成这样的重写序列。我们在一种丰富的多类型线性代数表达式语言上使用100多个图形重写等价公理的任意组合，对我们的系统进行了广泛的评估。对于隔离用于测试的10000个程序对中的96%(使用30个期限的程序)，Oursystem通过推理输出正确的重写序列。在所有情况下，生成的序列的有效性以及程序等价性的可证明断言都是可以计算的，时间可以忽略不计。