Synthesizing Mathematical Identities with E-Graphs

TL;DR

This paper introduces an automated method for discovering mathematical identities using e-graphs, significantly reducing manual effort and enabling faster, more accurate function implementations.

Contribution

It presents a novel two-phase pipeline combining synthesis with e-graphs and deduplication via integer linear programming to automatically find core mathematical identities.

Findings

Generated 7215 candidate identities from 61 benchmarks

Reduced candidates to 125 core identities through deduplication

Demonstrated effectiveness in automating identity discovery

Abstract

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.