论文标题
用电子支柱综合数学身份
Synthesizing Mathematical Identities with E-Graphs
论文作者
论文摘要
身份紧凑地描述了数学表达的属性，并可以将其利用为更快，更准确的功能实现。但是，目前必须手动发现身份，这需要很多专业知识。我们提出了一个两相合成和重复数据删除管道，该管道自动发现这些身份。在综合步骤中，使用电子图表来发现候选身份。但是，这些候选人中的大多数都是重复的，该重复是使用整数线性编程和另一个电子图表的次要重复数据删除。该合成阶段应用于一组61个基准，生成了7215个候选身份，然后将其重复数据删除阶段降低至125个核心身份。
Identities compactly describe properties of a mathematical expression and can be leveraged into faster and more accurate function implementations. However, identities must currently be discovered manually, which requires a lot of expertise. We propose a two-phase synthesis and deduplication pipeline that discovers these identities automatically. In the synthesis step, a set of rewrite rules is composed, using an e-graph, to discover candidate identities. However, most of these candidates are duplicates, which a secondary deduplication step discards using integer linear programming and another e-graph. Applied to a set of 61 benchmarks, the synthesis phase generates 7215 candidate identities which the deduplication phase then reduces down to 125 core identities.
