使用图-序列神经模型证明复杂表达式之间的等价性
Proving Equivalence Between Complex Expressions Using Graph-to-Sequence Neural Models
摘要：
我们的目标是可证明计算两个复杂的表达式树之间的等价性的问题。为此，我们形式化的问题，两个这样的程序之间的等价性，找到一组语义保持重写规则从一个到另一个，这样，重写后的两个程序在结构上是相同的，因此平凡equivalent. Then，我们开发了一个图形序列神经网络系统的程序等价性，训练产生这样的重写序列从一个精心制作的自动示例生成算法。我们广泛评估我们的系统上丰富的多类型线性代数表达式语言，使用任意组合的100+图形重写公理的等价。我们的机器学习系统保证所有真阴性的正确性，并通过设计确保零误报。它通过推理为10，000个隔离测试的等价表达式对中的93%输出有效的等价性证明，使用多达50个术语表达式。在所有情况下，序列的有效性产生，因此程序等价性的可证明断言总是可计算的，在可忽略的时间。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
