Verified Lifting of Deep learning Operators

TL;DR

This paper presents a framework that automatically synthesizes and verifies high-level mathematical descriptions of deep learning operators from low-level code, enhancing correctness and interpretability.

Contribution

It introduces a novel combination of symbolic execution, synthesis, and SMT verification to produce verified, human-readable formulas for deep learning operators.

Findings

Effective synthesis and verification on real-world Triton operators

Improved understanding and reliability of deep learning operator implementations

Bridging low-level code and high-level mathematical abstractions

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.