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
• Abstract summary: This work introduces a novel framework for the verified lifting of deep learning operators.<n>It synthesizes high-level mathematical formulas from low-level implementations.<n>This framework bridges the gap between low-level implementations and high-level abstractions.
• Score: 9.48599997951339
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• 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

• The Imitation Game: When LLMs Learn to Reason Like Programs via Code-Centric Reasoning Data Synthesis [50.473217152006875]
  MIMIC is a framework that leverages executable code as a rigorous medium for reasoning data synthesis.<n>MIMIC transforms algorithms into verifiable reasoning trajectories through narrative fusion, code-guided test synthesis, and dynamic code instrumentation.<n>Our method significantly elevates accuracy across general reasoning, complex mathematical benchmarks, and fine-grained deterministic tasks.
  arXiv  Detail & Related papers  (2026-09-13T17:04:16Z)
• Knowledge-Centric Agents for Workflow Generation [73.4340391112949]
  We propose a knowledge-centric framework that learns to invert, inject, and infer with knowledge across multiple abstraction levels.<n>Our method produces with richer node diversity, more coherent structures, and higher execution success rates than existing systems.
  arXiv  Detail & Related papers  (2026-07-17T11:03:01Z)
• An Operator-Based Approach to STL [10.103844123344057]
  We propose a novel approach to Signal Temporal Logic (STL) based on an operator acting on reachability value functions.<n>This constitutes a new theoretical framework for handling complex multi-nested formulae.<n>In contrast to focusing on the design of STL-based reachability functions, we develop operator-based nesting rules.
  arXiv  Detail & Related papers  (2026-05-27T07:47:45Z)
• Understanding by Reconstruction: Reversing the Software Development Process for LLM Pretraining [66.89012795621349]
  Large Language Models (LLMs) often struggle with the deep, long-horizon reasoning required for complex software engineering.<n>We propose a novel paradigm: understanding via reconstruction.<n>We introduce a framework that synthesizes latent agentic trajectories using a multi-agent simulation.
  arXiv  Detail & Related papers  (2026-03-11T09:23:20Z)
• Deep Unfolding: Recent Developments, Theory, and Design Guidelines [99.63555420898554]
  This article provides a tutorial-style overview of deep unfolding, a framework that transforms optimization algorithms into structured, trainable ML architectures.<n>We review the foundations of optimization for inference and for learning, introduce four representative design paradigms for deep unfolding, and discuss the distinctive training schemes that arise from their iterative nature.
  arXiv  Detail & Related papers  (2025-12-03T13:16:35Z)
• Fourier Neural Operators Explained: A Practical Perspective [75.12291469255794]
  The Fourier Neural Operator (FNO) has become the most influential and widely adopted due to its elegant spectral formulation.<n>This guide aims to establish a clear and reliable framework for applying FNOs effectively across diverse scientific and engineering fields.
  arXiv  Detail & Related papers  (2025-12-01T08:56:21Z)
• LightKGG: Simple and Efficient Knowledge Graph Generation from Textual Data [0.0]
  LightKGG is a novel framework that enables efficient KG extraction from textual data using small-scale language models.<n> Context-integrated Graph extraction integrates contextual information with nodes and edges into a unified graph structure.<n>Topology-enhanced relationship inference leverages the inherent topology of the extracted graph to efficiently infer relationships.
  arXiv  Detail & Related papers  (2025-10-27T13:55:13Z)
• Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
  We propose an end-to-end deep learning (DL) framework with low inference complexity for symbol-level precoding.<n>We show that the proposed framework captures substantial performance gains of optimal SLP, while achieving an approximately 80-times speedup over conventional methods.
  arXiv  Detail & Related papers  (2025-10-02T15:15:50Z)
• Negative Matters: Multi-Granularity Hard-Negative Synthesis and Anchor-Token-Aware Pooling for Enhanced Text Embeddings [25.565372681837697]
  We introduce a Multi-Granularity Hard-negative (MGH) synthesis framework to generate diverse negative samples with varying levels of similarity with the query.<n>We also propose an Anchor Token Aware (ATA) pooling method to improve text embedding accuracy without increasing model complexity.
  arXiv  Detail & Related papers  (2025-08-31T13:24:48Z)
• Synthetic Data Generation Using Large Language Models: Advances in Text and Code [0.0]
  Large language models (LLMs) are transforming synthetic training data generation in both natural language and code domains.<n>We highlight key techniques such as prompt-based generation, retrieval-augmented pipelines, and iterative self-refinement.<n>We discuss the accompanying challenges, including factual inaccuracies in generated text, insufficient stylistic or distributional realism, and risks of bias amplification.
  arXiv  Detail & Related papers  (2025-03-18T08:34:03Z)
• VeriMind: Agentic LLM for Automated Verilog Generation with a Novel Evaluation Metric [4.590930025882158]
  We propose VeriMind, an agentic LLM framework for Verilog code generation. We introduce a novel evaluation metric-pass@ARC-which combines the conventional pass@k measure with Average Refinement Cycles (ARC) to capture both success rate and the efficiency of iterative refinement. Experimental results on diverse hardware design tasks demonstrated that our approach achieved up to $8.3%$ improvement on pass@k metric and $8.1%$ on pass@ARC metric.
  arXiv  Detail & Related papers  (2025-03-15T23:43:06Z)
• 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.<n>Results demonstrate that Adaptive Prompting significantly improves performance on diverse reasoning benchmarks, including arithmetic reasoning (GSM8K, MultiArithm), logical reasoning and commonsense tasks.<n>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)
• A Neural Rewriting System to Solve Algorithmic Problems [47.129504708849446]
  We propose a modular architecture designed to learn a general procedure for solving nested mathematical formulas. Inspired by rewriting systems, a classic framework in symbolic artificial intelligence, we include in the architecture three specialized and interacting modules. We benchmark our system against the Neural Data Router, a recent model specialized for systematic generalization, and a state-of-the-art large language model (GPT-4) probed with advanced prompting strategies.
  arXiv  Detail & Related papers  (2024-02-27T10:57:07Z)
• 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)
• Complex-valued Adaptive System Identification via Low-Rank Tensor Decomposition [3.268878947476012]
  In this work we derive two new architectures to allow the processing of complex-valued signals. We show that these extensions are able to surpass the trivial, complex-valued extension of the original architecture in terms of performance.
  arXiv  Detail & Related papers  (2023-06-28T07:01:08Z)
• 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)
• BUSTLE: Bottom-Up Program Synthesis Through Learning-Guided Exploration [72.88493072196094]
  We present a new synthesis approach that leverages learning to guide a bottom-up search over programs. In particular, we train a model to prioritize compositions of intermediate values during search conditioned on a set of input-output examples. We show that the combination of learning and bottom-up search is remarkably effective, even with simple supervised learning approaches.
  arXiv  Detail & Related papers  (2020-07-28T17:46:18Z)

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.