論文の概要: Verified Lifting of Deep learning Operators

• arxiv url: http://arxiv.org/abs/2412.20992v1
• Date: Mon, 30 Dec 2024 14:57:32 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-12-31 16:02:17.830979
• Title: Verified Lifting of Deep learning Operators
• Title（参考訳）: ディープラーニング演算子の検証リフティング
• Authors: Qi Zhan, Xing Hu, Xin Xia, Shanping Li,
• Abstract要約: 本研究は,ディープラーニング演算子の精度向上のための新しいフレームワークを導入する。 低レベルの実装から高レベルの数学的公式を合成する。 このフレームワークは低レベルの実装と高レベルの抽象化のギャップを埋めます。
• 参考スコア（独自算出の注目度）: 9.48599997951339
• License:
• 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.
• Abstract（参考訳）: ディープラーニングオペレータは、現代のディープラーニングフレームワークの基本コンポーネントである。 カスタマイズされたオペレータの需要が高まり、開発者が独自に開発することがますます一般的になっている。 しかし、ハードウェア固有の最適化と数値安定性の必要性のため、演算子の設計と実装は複雑でエラーを起こしやすい。 既存の演算子とユーザ定義演算子の両方の機能を要約できるツールが必要である。 このギャップに対処するために、この研究は、低レベル実装から高レベルな数学的公式を合成するディープラーニング演算子の正当性向上のための新しいフレームワークを導入する。 本手法は, シンボリックな実行, 構文誘導合成, SMTに基づく検証と組み合わせて, 可読性, 形式的に検証された数式を生成する。 検証では、不変な合成パターンを設計し、SMTソルバを用いて、抽出した要約の正しさを検証する。 実世界からトリトンで実装されたディープラーニング演算子のデータセットを用いて,既存の手法と比較して,合成と検証の有効性を実証する。 このフレームワークは、低レベルの実装と高レベルの抽象化のギャップを埋め、ディープラーニングオペレータ開発における理解と信頼性を改善します。

関連論文リスト

• HPT++: Hierarchically Prompting Vision-Language Models with Multi-Granularity Knowledge Generation and Improved Structure Modeling [39.14392943549792]
  本稿では,階層型プロンプトチューニング(HPT)と呼ばれる新しい手法を提案し,構造化知識と従来の言語知識の同時モデリングを可能にする。 低レベルの即時学習のためのエンティティと属性間のペアワイズ関連をキャプチャする、関係誘導型アテンションモジュールを導入する。 全体意味論をモデル化する高レベルかつグローバルレベルのプロンプトを取り入れることで、提案された階層構造は、クロスレベルな相互リンクを偽造し、より複雑で長期的な関係を扱うようにモデルに権限を与える。
  論文  参考訳（メタデータ） (2024-08-27T06:50:28Z)
• Adapting LLMs for Efficient Context Processing through Soft Prompt Compression [1.1550486371582305]
  本稿では,大規模言語モデルを合理化された文脈処理のために戦略的に調整する,革新的なフレームワークを提案する。 我々の手法はSoftPromptCompと呼ばれ、動的に生成されたソフトプロンプトで自然言語をアマルガメイトし、簡潔でセマンティックに頑健な文脈の描写をフォージする。 我々は,我々のフレームワークが計算オーバーヘッドを著しく減らし,LLMの有効性を様々なベンチマークで向上させることを実証した。
  論文  参考訳（メタデータ） (2024-04-07T15:44:20Z)
• When Do Program-of-Thoughts Work for Reasoning? [51.2699797837818]
  本稿では,コードと推論能力の相関性を測定するために,複雑性に富んだ推論スコア(CIRS)を提案する。 具体的には、抽象構文木を用いて構造情報をエンコードし、論理的複雑性を計算する。 コードはhttps://github.com/zjunlp/EasyInstructのEasyInstructフレームワークに統合される。
  論文  参考訳（メタデータ） (2023-08-29T17:22:39Z)
• ExeDec: Execution Decomposition for Compositional Generalization in Neural Program Synthesis [54.18659323181771]
  プログラム合成において望ましいいくつかの異なる構成一般化形式を特徴付ける。 本稿では,ExeDecを提案する。ExeDecは,実行サブゴールを予測し,各ステップでプログラム実行によって段階的に通知される問題を解くための,新しい分解ベースの戦略である。
  論文  参考訳（メタデータ） (2023-07-26T01:07:52Z)
• On Conditional and Compositional Language Model Differentiable Prompting [75.76546041094436]
  プロンプトは、下流タスクでうまく機能するために、凍結した事前訓練言語モデル(PLM)を適応するための効果的な方法であることが示されている。 タスク命令や入力メタデータを連続的なプロンプトに変換することを学習する新しいモデル Prompt Production System (PRopS) を提案する。
  論文  参考訳（メタデータ） (2023-07-04T02:47:42Z)
• Complex-valued Adaptive System Identification via Low-Rank Tensor Decomposition [3.268878947476012]
  本研究では、複素数値信号の処理を可能にする2つの新しいアーキテクチャを導出する。 これらの拡張は、パフォーマンスの観点から、オリジナルのアーキテクチャの自明で複雑な拡張を超えることができることを示す。
  論文  参考訳（メタデータ） (2023-06-28T07:01:08Z)
• Mastering Symbolic Operations: Augmenting Language Models with Compiled Neural Networks [48.14324895100478]
  ニューラルアーキテクチャ」は、コンパイルされたニューラルネットワーク(CoNN)を標準変換器に統合する。 CoNNは、人工的に生成された注意重みを通してルールを明示的にエンコードするように設計されたニューラルネットワークモジュールである。 実験は,シンボル操作における長さ一般化,効率,解釈可能性の観点から,既存の手法よりも優れていることを示す。
  論文  参考訳（メタデータ） (2023-04-04T09:50:07Z)
• Compositional Generalization and Decomposition in Neural Program Synthesis [59.356261137313275]
  本稿では,学習プログラムシンセサイザーの合成一般化能力の測定に焦点をあてる。 まず、プログラム合成法が一般化されるであろういくつかの異なる軸を特徴付ける。 2つの一般的な既存のデータセットに基づいて、これらの能力を評価するためのタスクのベンチマークスイートを導入する。
  論文  参考訳（メタデータ） (2022-04-07T22:16:05Z)
• BUSTLE: Bottom-Up Program Synthesis Through Learning-Guided Exploration [72.88493072196094]
  プログラムのボトムアップ検索に学習を活用する新しい合成手法を提案する。 特に、入力出力例のセットに基づいて、探索条件中の中間値の合成を優先順位付けするようにモデルを訓練する。 単純な教師付き学習アプローチであっても,学習とボトムアップ検索の組み合わせは極めて効果的であることを示す。
  論文  参考訳（メタデータ） (2020-07-28T17:46:18Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。