Pattern Matching in AI Compilers and its Formalization (Extended Version)
Joseph W. Cutler, Alex Collins, Bin Fan, Mahesh Ravishankar, Vinod, Grover

TL;DR
This paper introduces PyPM, a Python-based DSL for graph optimization in machine learning, and formalizes its complex pattern matching language through a core calculus with proven semantics equivalence, mechanized in Coq.
Contribution
It formalizes the complex pattern language of PyPM into a mathematical core and proves the equivalence of its semantics using Coq.
Findings
Formal core calculus for PyPM patterns developed
Declarative and algorithmic semantics proven equivalent
Mechanized proof in Coq confirms correctness
Abstract
PyPM is a Python-based domain specific language (DSL) for building rewrite-based optimization passes on machine learning computation graphs. Users define individual optimizations by writing (a) patterns that match subgraphs of a computation graph and (b) corresponding rules which replace a matched subgraph with an optimized kernel. PyPM is distinguished from the many other DSLs for defining rewriting passes by its complex and novel pattern language which borrows concepts from logic programming. PyPM patterns can be recursive, nondeterminstic, and can require checking domain-specific constraints such as the shapes of tensors. The PyPM implementation is thus similarly complicated, consisting of thousands of lines of C++ code. In this paper, we present our work on building PyPM, as well as formalizing and distilling and this complexity to an understandable mathematical core. We have…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFuzzy Logic and Control Systems · Software Testing and Debugging Techniques · Algorithms and Data Compression
