Verified Lifting of Deep learning Operators

要約

深層学習演算子は、最新の深層学習フレームワークの基本コンポーネントです。
カスタマイズされたオペレーターの需要が高まるにつれ、開発者が独自のオペレーターを作成することがますます一般的になってきています。
ただし、ハードウェア固有の最適化と数値安定性の必要性により、演算子の設計と実装は複雑でエラーが発生しやすくなります。
既存の演算子とユーザー定義の演算子の両方の機能を要約できるツールが急務となっています。
このギャップに対処するために、この研究では、低レベルの実装から高レベルの数式を合成する、深層学習演算子の検証済みリフティングのための新しいフレームワークを導入しています。
私たちのアプローチは、シンボリック実行、構文ガイド付き合成、および SMT ベースの検証を組み合わせて、読みやすく正式に検証された数式を生成します。
合成では、トップダウン戦略とボトムアップ戦略を組み合わせて、広大な検索空間を効率的に探索します。
検証では、不変合成パターンを設計し、SMT ソルバーを活用して、導出された要約の正確さを検証します。
簡素化では、カスタム ルールを備えた egraph ベースの手法を使用して、複雑な数式を自然で直感的な形式に復元します。
現実世界から Triton に実装された深層学習演算子のデータセットで評価された私たちの方法は、既存の技術と比較して合成と検証の有効性を示しています。
このフレームワークは、低レベルの実装と高レベルの抽象化の間のギャップを埋め、深層学習オペレーター開発における理解と信頼性を向上させます。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google