Verified Lifting of Deep learning Operators

TL;DR

This work tackles the challenge of deriving formal, human-readable mathematical summaries of deep learning operators from low-level implementations. It introduces a three-phase framework—synthesis, verification, and simplification—driven by symbolic evaluation, syntax-guided synthesis (combining top-down and bottom-up search), SMT-based verification, and e-graph-based simplification. Empirical evaluation on 33 real-world Triton/FlagGems operators shows substantial improvements over the baseline in both synthesis and verification success (28/33 vs 13/33) and in speed, with ablation studies highlighting the value of top-down synthesis, search pruning, and invariant-patterning-based verification. The approach yields readable, formally verified operator summaries and demonstrates potential for improving reliability and comprehension in custom DL kernel development, with practical impact for developers and tooling in high-performance DL frameworks.

Abstract

Deep learning operators are fundamental components of modern deep learning frameworks. With the growing demand for customized operators, it has become increasingly common for developers to create their own. However, designing and implementing operators is complex and error-prone, due to hardware-specific optimizations and the need for numerical stability. There is a pressing need for tools that can summarize the functionality of both existing and user-defined operators. To address this gap, this work introduces a novel framework for the verified lifting of deep learning operators, which synthesizes high-level mathematical formulas from low-level implementations. Our approach combines symbolic execution, syntax-guided synthesis, and SMT-based verification to produce readable and formally verified mathematical formulas. In synthesis, we employ a combination of top-down and bottom-up strategies to explore the vast search space efficiently; In verification, we design invariant synthesis patterns and leverage SMT solvers to validate the correctness of the derived summaries; In simplification, we use egraph-based techniques with custom rules to restore complex formulas to their natural, intuitive forms. Evaluated on a dataset of deep learning operators implemented in Triton from the real world, our method demonstrates the effectiveness of synthesis and verification compared to existing techniques. This framework bridges the gap between low-level implementations and high-level abstractions, improving understanding and reliability in deep learning operator development.

Figures (2)

• Figure 1: Overview of our approach
• Figure 2: Language Syntax