Verified Lifting of Deep learning Operators

• URL: http://arxiv.org/abs/2412.20992v1
• Date: Mon, 30 Dec 2024 14:57:32 GMT
• Title: Verified Lifting of Deep learning Operators
• Authors: Qi Zhan, Xing Hu, Xin Xia, Shanping Li,
• Abstract summary: This work introduces a novel framework for the verified lifting of deep learning operators. It synthesizes high-level mathematical formulas from low-level implementations. This framework bridges the gap between low-level implementations and high-level abstractions.
• Score: 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.

Related papers

• A Text-Based Knowledge-Embedded Soft Sensing Modeling Approach for General Industrial Process Tasks Based on Large Language Model [16.842988666530204]
  Data-driven soft sensors (DDSS) have become mainstream methods for predicting key performance indicators in process industries. Development requires complex and costly customized designs tailored to various tasks during the modeling process. We propose a general framework named LLM-TKESS (large language model for text-based knowledge-embedded soft sensing) for enhanced soft sensing modeling.
  arXiv  Detail & Related papers  (2025-01-09T08:59:14Z)
• EpiCoder: Encompassing Diversity and Complexity in Code Generation [49.170195362149386]
  We introduce a novel feature tree-based synthesis framework inspired by Abstract Syntax Trees (AST) Unlike AST, which captures syntactic structure of code, our framework models semantic relationships between code elements. We fine-tuned widely-used base models to create the EpiCoder series, achieving state-of-the-art performance at both the function and file levels.
  arXiv  Detail & Related papers  (2025-01-08T18:58:15Z)
• Think Beyond Size: Adaptive Prompting for More Effective Reasoning [0.0]
  We introduce Adaptive Prompting, a dynamic and iterative framework designed to enhance reasoning by incorporating real-time adjustments to prompt structures and validation mechanisms. Results demonstrate that Adaptive Prompting significantly improves performance on diverse reasoning benchmarks, including arithmetic reasoning (GSM8K, MultiArithm), logical reasoning and commonsense tasks. Our approach enables smaller models to achieve competitive performance with larger counterparts, such as GPT-4, while maintaining computational efficiency.
  arXiv  Detail & Related papers  (2024-10-10T17:14:36Z)
• When Do Program-of-Thoughts Work for Reasoning? [51.2699797837818]
  We propose complexity-impacted reasoning score (CIRS) to measure correlation between code and reasoning abilities. Specifically, we use the abstract syntax tree to encode the structural information and calculate logical complexity. Code will be integrated into the EasyInstruct framework at https://github.com/zjunlp/EasyInstruct.
  arXiv  Detail & Related papers  (2023-08-29T17:22:39Z)
• ExeDec: Execution Decomposition for Compositional Generalization in Neural Program Synthesis [54.18659323181771]
  We characterize several different forms of compositional generalization that are desirable in program synthesis. We propose ExeDec, a novel decomposition-based strategy that predicts execution subgoals to solve problems step-by-step informed by program execution at each step.
  arXiv  Detail & Related papers  (2023-07-26T01:07:52Z)
• On Conditional and Compositional Language Model Differentiable Prompting [75.76546041094436]
  Prompts have been shown to be an effective method to adapt a frozen Pretrained Language Model (PLM) to perform well on downstream tasks. We propose a new model, Prompt Production System (PRopS), which learns to transform task instructions or input metadata, into continuous prompts.
  arXiv  Detail & Related papers  (2023-07-04T02:47:42Z)
• Mastering Symbolic Operations: Augmenting Language Models with Compiled Neural Networks [48.14324895100478]
  "Neural architecture" integrates compiled neural networks (CoNNs) into a standard transformer. CoNNs are neural modules designed to explicitly encode rules through artificially generated attention weights. Experiments demonstrate superiority of our approach over existing techniques in terms of length generalization, efficiency, and interpretability for symbolic operations.
  arXiv  Detail & Related papers  (2023-04-04T09:50:07Z)
• Compositional Generalization and Decomposition in Neural Program Synthesis [59.356261137313275]
  In this paper, we focus on measuring the ability of learned program synthesizers to compositionally generalize. We first characterize several different axes along which program synthesis methods would be desired to generalize. We introduce a benchmark suite of tasks to assess these abilities based on two popular existing datasets.
  arXiv  Detail & Related papers  (2022-04-07T22:16:05Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.