Tensor Algebraic Property Skeletons: Amplifying Property-Based Testing for AI Compilers

• URL: http://arxiv.org/abs/2606.06747v1
• Date: Thu, 04 Jun 2026 22:01:30 GMT
• Title: Tensor Algebraic Property Skeletons: Amplifying Property-Based Testing for AI Compilers
• Abstract summary: Propilot is an agentic property-based testing framework for deep learning (DL) compilers with GPT 5.5.<n>It represents tensor algebra knowledge as reusable property skeletons, each coupled with operator constraints, shape and value rules, and oracle templates.<n>We evaluate Propilot on TVM with 212 operators and 20 property skeletons, generating 4,579 PBTs.
• Score: 7.684444178725619
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Deep learning (DL) compilers such as TVM and ONNX-MLIR lower tensor computation graphs into optimized executables for target backends. Testing these AI compilers has made substantial progress in generating well-formed inputs in the context of fuzzing; however, such generation alone does not catch semantic drifts from algebraic invariants that graph transformations and optimizations are expected to preserve. While tensor algebra has been studied for decades, it has not been transformed into executable property-based tests (PBTs) for DL compilers because doing so requires jointly constructing operators, inputs, and test oracles. The central challenge is no longer generating well-formed inputs for fuzzing DL compilers, but bootstrapping executable PBTs with such inputs and oracles based on tensor algebra. We realize this vision in Propilot, an LLM-driven agentic property-based testing framework for DL compilers with GPT 5.5. First, Propilot represents tensor algebra knowledge as reusable property skeletons, each coupled with operator constraints, shape and value rules, and oracle templates. Second, given a target compiler, Propilot instantiates these skeletons into executable PBTs by generating paired tensor computation graphs, concrete tensor inputs, and expected semantic relations as oracles. Next, to prevent generated tests from degenerating into invalid or uninformative PBTs, Propilot validates each PBT candidate before execution for applicability and safety. Validation feedback, execution results, and coverage signals guide subsequent generation. We evaluate Propilot on TVM with 212 operators and 20 property skeletons, generating 4,579 PBTs. Compared with direct LLM-based PBT generation, Propilot reduces redundancy by 49% and eliminates invalid tests through explicit property skeletons. This effectiveness translates into finding semantic errors and numerical discrepancies.

Related papers

• Agentic Proof and Property-Based Testing via Property-Templates in Data-Intensive Computing [6.28395649374318]
  This paper investigates recurring property patterns in Apache Spark computation.<n>We design an agentic, dual-track validation framework that uses property templates to formally verify correctness in the Lean 4 theorem prover.<n>Our evaluation shows that property templates increase agentic proof engineering success by up to 2.6x (1.6x on average) and reduce proof hallucinations by 59%.
  arXiv  Detail & Related papers  (2026-07-10T03:33:47Z)
• VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
  We introduce VASO, a framework for verification-guided self-evolution of robot skill contracts.<n>VASO verifies logically inconsistent skill contracts, then verifies plans induced by the skill against global and local temporal specifications.<n>On Clearpath Jackal and PX4 quadcopter tasks, VASO reaches 97.2% formal-specification compliance using fewer than 100 optimization samples.
  arXiv  Detail & Related papers  (2026-06-03T20:02:35Z)
• Leveraging BART to Assess CS1 C++ Programming Assignments using Rubric-based Criteria [2.1843439591862333]
  This paper investigates rubric-aware, multitask fine-tuning of transformer models for automated grading of C++ programming assignments.<n>Using multi-semester CS1 data, student submissions are paired with numeric scores, letter-grade buckets, and assignment rubrics, then preprocessed into unified sequences for transformer input.<n>A BART encoder-decoder with LoRA adaptation is trained to jointly predict numeric grades and grade buckets, augmented with a distribution-matching term to align predicted and empirical grade distributions.
  arXiv  Detail & Related papers  (2026-06-02T15:57:14Z)
• From Patches to Trajectories: Privileged Process Supervision for Software-Engineering Agents [56.31499185764872]
  Supervised fine-tuning (SFT) on long teacher trajectories is the dominant way to instill investigation and reasoning in open software-engineering (SWE) agents.<n>We propose Patches-to-Trajectories (P2T), which uses $pstar$ as privileged information during curation and formulates trajectory construction as bi-objective optimization over per-step effectiveness and trajectory length.
  arXiv  Detail & Related papers  (2026-05-21T04:54:55Z)
• Controllable and Verifiable Tool-Use Data Synthesis for Agentic Reinforcement Learning [82.89535601592739]
  We propose a two-stage pipeline that generates reliable base tool-use trajectories through self-evolving synthesis with multi-level validation.<n>These augmentations introduce distractor tools, indirect or ambiguous user queries, and noisy, multi-format, or erroneous tool outputs.<n>This design enables automatic reward computation via reference matching for standard cases and lightweight judge-assisted verification for special behaviors such as error detection.
  arXiv  Detail & Related papers  (2026-04-10T18:38:52Z)
• Dynamic analysis enhances issue resolution [53.50448142467294]
  DAIRA (Dynamic Analysis-enhanced Issue Resolution Agent) is an automated repair framework that embeds dynamic analysis into the agent's reasoning cycle.<n> Driven by a Test Tracing-Driven methodology, DAIRA utilizes lightweight monitors to extract critical runtime data.<n>When powered by Gemini 3 Flash Preview, DAIRA establishes a new state-of-the-art (SOTA) performance, achieving a 79.4% resolution rate on the SWE-bench Verified dataset.
  arXiv  Detail & Related papers  (2026-03-23T14:48:54Z)
• TENSURE: Fuzzing Sparse Tensor Compilers (Registered Report) [9.083996936429465]
  We present TENSURE, the first black-box fuzzing framework specifically designed for the testing of sparse Compilers.<n>We propose a novel constraint-based generation algorithm that guarantees 100% semantic validity of synthesized kernels.<n>Our evaluation on two state-of-the-art systems, TACO and Finch, reveals widespread fragility, particularly in TACO, where TENSURE exposed crashes or silent miscompilations.
  arXiv  Detail & Related papers  (2026-03-19T00:13:14Z)
• SecureCodeRL: Security-Aware Reinforcement Learning for Code Generation with Partial-Credit Rewards [1.5377279217726239]
  This paper presents SecureCodeRL, a reinforcement learning pipeline for security-aware code generation.<n>The key idea is a partial-credit functional reward that assigns intermediate scores for validity, successful execution, and producing output.<n>Although Bandit findings were absent in this small evaluation, the security term is integrated into training to discourage insecure shortcuts when they appear.
  arXiv  Detail & Related papers  (2026-01-03T13:36:36Z)
• Test time training enhances in-context learning of nonlinear functions [51.56484100374058]
  Test-time training (TTT) enhances model performance by explicitly updating designated parameters prior to each prediction.<n>We investigate the combination of TTT with in-context learning (ICL), where the model is given a few examples from the target distribution at inference time.
  arXiv  Detail & Related papers  (2025-09-30T03:56:44Z)
• Generating Highly Structured Test Inputs Leveraging Constraint-Guided Graph Refinement [4.121384394709256]
  This study investigates whether test inputs for structured domains can be unified through a graph-based representation.<n>We will evaluate the effectiveness of this approach in enhancing input validity and semantic preservation across eight AI systems.
  arXiv  Detail & Related papers  (2025-07-28T18:54:04Z)
• Test-Time Adaptation with Binary Feedback [50.20923012663613]
  BiTTA is a novel dual-path optimization framework that balances binary feedback-guided adaptation on uncertain samples with agreement-based self-adaptation on confident predictions.<n> Experiments show BiTTA achieves 13.3%p accuracy improvements over state-of-the-art baselines.
  arXiv  Detail & Related papers  (2025-05-24T05:24:10Z)
• Constraining Representations Yields Models That Know What They Don't Know [2.729898906885749]
  A well-known failure mode of neural networks is that they may confidently return erroneous predictions. This work presents a novel direction to address these issues in a broad, general manner. We assign to each class a unique, fixed, randomly-generated binary vector - hereafter called class code. We train the model so that its cross-depths activation patterns predict the appropriate class code according to the input sample's class.
  arXiv  Detail & Related papers  (2022-08-30T18:28:00Z)

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.