論文の概要: 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ソルバを用いて、抽出した要約の正しさを検証する。 実世界からトリトンで実装されたディープラーニング演算子のデータセットを用いて,既存の手法と比較して,合成と検証の有効性を実証する。 このフレームワークは、低レベルの実装と高レベルの抽象化のギャップを埋め、ディープラーニングオペレータ開発における理解と信頼性を改善します。

関連論文リスト

• A Text-Based Knowledge-Embedded Soft Sensing Modeling Approach for General Industrial Process Tasks Based on Large Language Model [16.842988666530204]
  データ駆動型ソフトセンサー(DDSS)は、プロセス産業において重要なパフォーマンス指標を予測する主要な手法となっている。 開発には、モデリングプロセス中に様々なタスクに合わせてカスタマイズされた複雑でコストがかかる設計が必要である。 本稿では,LLM-TKESS(テキストベース知識埋め込み型ソフトセンシングのための大規模言語モデル)というフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-01-09T08:59:14Z)
• EpiCoder: Encompassing Diversity and Complexity in Code Generation [49.170195362149386]
  抽象構文木(AST)にヒントを得た新しい特徴木ベース合成フレームワークを提案する。 コードの構文構造をキャプチャするASTとは異なり、私たちのフレームワークはコード要素間のセマンティックな関係をモデル化します。 広く使われているベースモデルを微調整してEpiCoderシリーズを作成し、関数レベルとファイルレベルの両方で最先端のパフォーマンスを実現しました。
  論文  参考訳（メタデータ） (2025-01-08T18:58:15Z)
• Think Beyond Size: Adaptive Prompting for More Effective Reasoning [0.0]
  本稿では,動的かつ反復的なフレームワークであるAdaptive Promptingを紹介する。 その結果、Adaptive Promptingは、算術的推論(GSM8K、MultiArithm)、論理的推論、コモンセンスタスクなど、様々な推論ベンチマークのパフォーマンスを著しく向上させることを示した。 提案手法は,計算効率を維持しつつ,GPT-4などの大規模モデルと競合する性能を実現する。
  論文  参考訳（メタデータ） (2024-10-10T17:14:36Z)
• 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)
• 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)

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

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