论文标题
使用图形到序列神经模型通过重写规则的数据流图等效性
Equivalence of Dataflow Graphs via Rewrite Rules Using a Graph-to-Sequence Neural Model
论文作者
论文摘要
在这项工作中，我们针对的是，可以证明计算两个表示为数据流图的程序之间的等价性。为此，我们将两个程序之间的等效问题形式化为将一组传播语义的改写规则从一个程序中找到一个，以便在重写两个程序之后，这两个程序在结构上是相同的，因此在同等上相同。然后，我们开发了第一个用于程序等效性的图形到序列神经网络系统，该系统经过培训，可以从精心制作的自动示例生成算法中产生此类序列。我们使用100多个等效的图形练习公理的任意组合，在丰富的多类线性代数表达语言上广泛评估我们的系统。我们的系统通过推断输出正确的重写序列，用于使用30年程序隔离进行测试的10,000个程序对中的96％。在所有情况下，产生的序列的有效性，因此在可忽略的时间内可以计算程序等效性的可证明的主张。
In this work we target the problem of provably computing the equivalence between two programs represented as dataflow graphs. To this end, we formalize the problem of equivalence between two 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 the first 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 system outputs via inference a correct rewrite sequence for 96% of the 10,000 program pairs isolated for testing, using 30-term programs. And in all cases, the validity of the sequence produced and therefore the provable assertion of program equivalence is computable, in negligible time.
