2026-06-08
Tensor Algebraic Property Skeletons: Amplifying Property-Based Testing for AI Compilers Yuxin Qiu1 , Ben Limpanukorn2 , Seongmin Lee2 , Jiyuan Wang3 , Qian Zhang1 , Miryung Kim2 1 UC Riverside 2 UCLA 3 Tulane University
arXiv:2606.06747v1 [cs.SE] 4 Jun 2026
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 correct oracles based on tensor algebra. We realize this vision in P ROPILOT, an LLM-driven agentic property-based testing framework for DL compilers with GPT 5.5. First, P ROPILOT 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, P ROPILOT 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, P ROPILOT validates each PBT candidate before execution for applicability and safety. Validation feedback, execution results, and coverage signals guide subsequent generation. We evaluate P ROPILOT on TVM with 212 operators and 20 property skeletons, generating 4,579 PBTs. Compared with direct LLM-based PBT generation, P ROPILOT reduces redundancy by 49% and eliminates invalid tests through explicit property skeletons. This effectiveness translates into finding semantic errors and numerical discrepancies.
1
Introduction
Deep learning (DL) compilers, such as TVM Chen et al. (2018) and ONNX-MLIR Jin et al. (2020), are now part of the critical deployment path for trained models. They lower tensor computation graphs, containing tensor operators such as matmul and add, into executable code through graph rewrites, operator legalization, fusion, layout changes, and backend-specific code generation. These transformations are necessary for performance, but they also create a correctness risk: an optimized program may compile and run while computing values that no longer match the source tensor computation Shen et al. (2021); Liu et al. (2023a); Zhou et al. (2024). Testing DL compilers inherently requires solving a constrained input-generation problem. A model graph with tensors is not a free-form input: tensor shapes must be consistent across dataflow edges, operator attributes must satisfy frontend requirements, and the generated graph must stay within the compiler’s supported operator space. Existing work has therefore made substantial progress on this well-formedness problem Liu et al. (2023a;b); Wang et al. (2023); Deng et al. (2022); Ma et al. (2023); Mu et al. (2025); Limpanukorn et al. (2025). These techniques extract, infer, or encode operator and graph constraints to generate models that compiler frontends can accept in the context of fuzzing . For example, NeuRI Liu et al. (2023b) infers operator constraints from execution traces and applies concolic solving to generate models that satisfy inferred relations. Well-formed inputs can check whether a compiler frontend accepts a model correctly; however, acceptance does not show whether compiler transformations preserve the intended tensor computation. Silent semantic drifts can change model outputs without triggering frontend validation errors or compilation failures Shen et al. (2021); Zhou et al. (2024); Ma et al. (2023). For example, generating valid input tensors for add can exercise the operator, but it does not check whether optimized executions preserve algebraic relations such as associativity. Exposing these behaviors requires an executable property: a semantic relation over valid tensor programs that the compiler output is expected to preserve. ∗ Corresponding email: [email protected].
1
Agentic Property-Based Testing Framework 8. next-iteration feedback Agent User Input
1. target
Target
Operator Discovery
2. candidate operators
Controlled Test Generation
6b. rejection reason 4. prop., gen., and rules
3. knowledge query main workflow feedback loop
Knowledge and Guidance Property Skeletons
Data Generators
5. generated test
Prioritization Rules
Test Validation
Execution Output
Scenario Schema
Passing Tests
Scenario Applicability
Failing Tests
Runtime Safety
Coverage
6a. validated test Test Execution
7. result
Figure 1: P ROPILOT workflow for bootstrapping executable property-based tests from tensor algebra property skeletons. Tensor algebra provides foundations for such properties Kjolstad et al. (2017), but the algebraic relations do not directly become property-based tests (PBTs) Fink and Bishop (1997); Padhye et al. (2019a;b) by themselves. To make a property executable, the tester must decide which operators it applies to, how to generate valid tensor inputs, how to build the compared programs, how to check their outputs, etc. For example, associativity can guide tests for selected binary operators, but only after the test has valid shapes, values, and numerical comparison rules. The central challenge to test DL compilers is therefore to bootstrap executable PBTs from tensor algebra: generating tests that combine well-formed inputs with semantic properties that the compiler should preserve. P ROPILOT. In this paper, we propose P ROPILOT, an agentic PBT framework that turns tensor algebra into executable property-based tests for DL compilers. The core insight is to represent tensor algebra not as ad hoc prompts, but as reusable testing structure. As shown in Figure 1, P ROPILOT realizes this idea through property skeletons, which couple a concrete semantic relation with its operator applicability, inputgeneration rules, and oracle construction rules. This gives AI the missing control layer: one skeleton can scale across many operators and tensor instances, while constraining the agent from inventing unsupported properties, inputs, or oracles. P ROPILOT then addresses two execution challenges.
First, P ROPILOT performs controlled instantiation. Given a target compiler, it discovers supported operators and selects applicable property skeletons before asking the agent to write code. For TVM, this means instantiating checks such as relax.sum with reduction decomposition, relax.add with commutativity or associativity, relax.nn.relu with idempotence, and relax.nn.softmax with shift invariance. The generated PBT contains both sides of the relation, the concrete tensor inputs, and the oracle used to compare outputs. Second, P ROPILOT validates each PBT candidate before execution. Validation checks property applicability, graph validity, TVM API usage, oracle construction, and runtime safety. If a candidate uses an inapplicable property, builds an invalid Relax graph, or calls the API incorrectly, P ROPILOT rejects it with a concrete reason and uses that feedback for repair. Only validated tests are executed. Evaluation. We evaluate P ROPILOT on TVM with 212 operators and 20 property skeletons. The LLM-PBT baseline ran for 24 hours and generated 1,863 tests. Its non-runnable tests are dominated by API misuse (57.27%), invalid Relax model construction (32.96%), incomplete pytest fixture generation (3.70%), TVM DSL misuse (0.27%), and Python syntax error (0.05%). Among runnable tests, only 101 tests (5.42%) have correct property logic, while the remaining have incorrect property logic. Its generated tests also repeated operator-property patterns: 1,237 tests (66.40%) repeated unordered operator-property signatures, while 480 tests (25.76%) repeated stricter ordered operator-property signatures. In contrast, P ROPILOT produces 4,579 generated property-based tests and reduces estimated redundancy to about 30% and invalid generated tests to 0% by using explicit property skeletons and validation feedback. The validated tests also change the type of failures we observe. Among classified P ROPILOT failures, 50% are semantic inconsistencies between tensor math and compiler implementation, 25% are numerical instabilities, and the rest are reference-oracle mismatch or residual API misuse. This result supports
2
Table 1: Information Stored in a Property Skeleton. Field
Role in the skeleton
Example from commutativity
Intent Operator classes Applicability conditions Rejection rule Concretization schema Oracle notes
Semantic relation to check Where the relation usually applies Assumptions the agent must check When not to instantiate the skeleton Shape of the generated relation How outputs should be compared
swapping operands should preserve output symmetric binary pointwise operators operand order has no hidden semantics order-sensitive operators such as subtract op(x, y) vs. op(y, x) exact equality or AllClose for floats
the shift from input generation alone to scalable PBT bootstrapping with both well-formed inputs and executable semantic oracles. In summary, this paper makes three contributions. • We formulate DL compiler testing as the problem of bootstrapping executable PBTs with both wellformed inputs and semantic oracles. • We introduce reusable property skeletons for tensor algebra, together with controlled instantiation and validation to generate executable compiler tests. • We evaluate P ROPILOT on TVM against direct LLM-based PBT generation and fuzzing. Results show that explicit property skeletons and validation reduce invalid tests and produce semantic or numerical failure signals.
2
Background
Oracles in DL Compiler Testing. Prior work Deng et al. (2022); Liu et al. (2023a;b); Ma et al. (2023); Wang et al. (2023); Mu et al. (2025) primarily relies on crash-based oracles and monitors coverage. It reports a compiler issue when compiling an input model leads to crashes. Another commonly used oracle Ma et al. (2023); Liu et al. (2023a;b) takes models validity as the criterion: valid models are expected to compile, while invalid models should be rejected with an appropriate exception. Under this oracle, a compiler issue is reported if a valid model fails to compile or an invalid model is accepted without error. Tensor Algebra Properties as Testable Invariants. Tensor algebra gives semantic relations that can be checked after compilation. For example, add(x, y) should agree with add(y, x) when operand order has no meaning; relu(relu(x)) should agree with relu(x); and a reduction such as sum(x) can be checked by splitting x, reducing each part, and recomposing the partial sums. A compiler transformation should preserve these relations: if two tensor programs are equivalent before compilation, their compiled outputs should match within an appropriate tolerance. This makes tensor algebra useful as an oracle that checks more than whether a model crashes or compiles successfully Zhou et al. (2024). However, a tensor algebra relation is not automatically a PBT. To use it as a test, the tester must decide which operators it applies to, which shapes and dtypes are valid, which input values should be generated, and how outputs should be compared. For example, commutativity is valid for add and multiply, but not for subtract; reduction decomposition requires a valid split axis and a recomposition rule; and floating-point comparisons need tolerances. In this paper, we treat these conditional relations as the source of property skeletons: reusable descriptions that can be instantiated into executable PBTs only when their applicability conditions are satisfied.
3
P ROPILOT
Figure 1 shows the workflow of P ROPILOT. Our goal is to scalably bootstrap executable PBTs from tensor algebra property skeletons. P ROPILOT achieves this in three steps. First, it stores tensor knowledge as reusable property skeletons (Section 3.1). Second, the agent uses these skeletons to synthesize executable PBTs through controlled test generation (Section 3.2). Third, P ROPILOT validates the generated test before execution and also feeds validation or execution results back into later choices. 3.1
Tensor Knowledge as Reusable Property Skeletons
Tensor algebra gives useful semantic relations; e.g., commutativity declares that swapping two operands should not change the result. However, a relation alone is not yet a compiler test. To use it for DL compiler
3
Table 2: Examples of Tensor Algebra Properties. Categories Algebra Properties
Description
Example Property Skeletons
Mathematical semantics of tensor operators
Tensor Properties
Robustness to changes in tensor input structure
Fallback Properties
Concrete checks used when no stronger algebraic family is applicable
Commutativity
max(x, y) == max(y, x)
Associativity
add(x, add(y, z)) == add(add(x, y), z)
Identity
multiply(x, 1) == multiply(x)
Permutation invariance
sum(x) == sum(permute(x))
Geometric decomposition
add(x, y) == concat(add(x1, y1), add(x2, y2))
Decomposition + idempotence
Split x, check relu(relu(x_i)) equals relu(x_i) on each part, then recombine
Reference consistency
Compare compiled output with a trusted eager-mode or interpreter result
Concrete input replay
Re-run a known valid operator example across compilation settings
Shape and dtype preservation
Check that compilation preserves expected output shape and dtype
testing, the test must know which operators are symmetric, which shapes can be used for the operands, and how floating-point outputs should be compared. P ROPILOT encodes such algebraic information in property skeletons. A property skeleton is a reusable property document that tells the agent how a tensor algebra relation should become a test. As shown in Table 1, a skeleton records the relation’s intent, where it can be used, when it should be rejected, how it should be concretized, and how outputs should be compared. For example, the commutativity skeleton states the relation op(x, y) == op(y, x) and restricts it to operators whose operand order is semantically symmetric. As another example, the geometric-decomposition skeleton instead tells the agent to split tensors, apply the operator to the pieces, and recompose the partial results with an operator-specific rule. In total, P ROPILOT is currently equipped with 17 property skeletons, which cover algebra properties, tensor properties, and fallback properties, as shown in Table 2. P ROPILOT is readily extensible to include more properties by adding the corresponding skeleton documents. 3.2
Controlled Test Generation
We observed that directly prompting LLMs to generate PBTs is not effective. In our experiments, more than 90% of generated tests are non-runnable, and only 5.42% contain correct property logic. In other words, most PBTs generated by direct prompting fail to express a runnable, correct property test. P ROPILOT addresses this issue and makes PBT generation scalable in an agentic setting. Instead of asking the agent to invent a complete test from scratch, P ROPILOT asks it to instantiate an explicit property skeleton for a selected operator and data generator. Test Scenario Generation. For each test, the agent first generates its test scenario based on three components: data, apply, assert. These components serve as a compact specification that records what the PBT must implement. data specifies how to generate input tensors for the model. apply invokes operators to build the model and encodes the property that should hold. assert defines the oracle contract and binds the concretized property to an executable checking policy. To support controlled tensor generation, P ROPILOT is equipped with 23 data generators. For example, pure_random generates reproducible random tensors, while identity_injection adds the identity value required by the selected operator, such as a zero tensor for addition or an all-one tensor for multiplication. The following example shows a commutativity scenario for relax.add. The agent generates two sameshape float32 tensors using pure_random generator, builds two models add(x, y) and add(y, x), and checks that their outputs are equal up to AllClose. The agent then generates the executable Python test that implements this scenario. Listing 1: A test scenario for relax.add commutativity. 1 2 3 4 5 6 7
@data( target='tvm_relax', op='relax.add', inputs=('x', 'y'), gen=pure_random, dtype='float32', shape_policy='small_same_shape' ) @apply(relation='lhs=op(x, y), rhs=op(y, x)') @assert(relation=EquivalentOutputs(oracle=AllClose(rtol=1e-5, atol=1e-6)))
Prioritization Rules. We observed that the agent tends to make shallow choices when generation is left unconstrained. For example, it often selects common elementwise operators such as add and multiply,
4
simple properties such as associativity and commutativity, and generic generators such as pure_random. These choices can produce a large amount of duplicated tests. Therefore, testing time is spent on compiler paths that have already been exercised, while other operators supported by the DL compiler and less frequently tested compiler logic remain uncovered. We are inspired by branch-guided testing and address this problem with prioritization rules. After each test execution, P ROPILOT feeds the result and usage statistics back to the agent, including whether there are failures and how many times each operator, property skeleton, generator, and (operator, property, generator) combination has been used so far. Based on this information, P ROPILOT enforces two prioritization rules. First, it prioritizes unused operators, properties, generators, and combinations. Second, after each item is used, it prioritizes under-used cases and cases near previous failures. 3.3
Test Validation and Feedback Loop
To avoid wasting time on invalid tests, P ROPILOT validates an agent-generated test before running it. Validation happens in three ordered steps: scenario schema checks, scenario applicability checks, and runtime safety checks. • Scenario Schema Checks. P ROPILOT first checks whether the generated test scenario contains the required data, apply, and assert components. P ROPILOT also checks that the property and data generator named in the scenario come from the provided knowledge base. These checks are implemented with lightweight keyword checks, and can catch simple LLM hallucinations such as inventing an unknown property or omitting the oracle component. • Scenario Applicability Checks. P ROPILOT next checks whether the scenario can plausibly apply to the selected operator. The agent runs a small smoke check to confirm that the operator exists in the target compiler API. It then checks the property and data generator against the selected operator. For example, commutativity should apply to relax.add but not relax.subtract, and identity_injection should only be used when the operator has a well-defined identity value. • Runtime Safety Checks. After the agent writes the Python test from the scenario, P ROPILOT uses AST analysis to check that the generated test contains the expected testing steps, e.g., build_model(), run_compiler(), check_oracle(), and save_repro(). This check ensures that the generated file is not only syntactically valid Python, but also actually builds a model, runs the compiler, checks the property, and saves reproduction information for failures. Accepted tests are executed and produce execution results, coverage information, and failure artifacts. Rejected tests are saved with short rejection reasons, such as missing scenario components, unknown operators, and inapplicable properties. These rejection decisions are passed back to the next iteration so the agent may avoid repeating the same invalid choice.
4
Evaluation Results
We seek to answer the following research questions. RQ1 What kinds of errors are produced by each testing strategy? RQ2 Do tensor algebra property skeletons expose meaningful semantic and numerical issues in TVM? RQ3 How does P ROPILOT compare with LLM-only property-based testing and fuzzing in code coverage? Subject. We evaluate P ROPILOT on TVM Chen et al. (2018), a widely used DL compiler. Our evaluation targets operator-level compiler behavior and focuses on PBTs instantiated from tensor algebra property skeletons, including algebra properties such as commutativity and identity, tensor properties such as geometric decomposition, and fallback properties such as reference consistency. Baselines. We compare P ROPILOT with two baselines. • LLM-only PBT. This baseline directly prompts GPT-5.5 to generate PBTs. It uses the model’s codegeneration capability, but does not use P ROPILOT’s controlled property-family retrieval, validation schema, or feedback loop. • Fuzzing. This baseline generates TVM test inputs without tensor algebra properties. It extracts type, shape, resource constraints from specification and implementation to generate inputs and measures whether generated inputs can pass TVM validation and compilation.
5
Table 3: Error classification. Method
P ROPILOT
LLM-only PBT
Fuzzing
4.1
Classification
Percentage
Interpretation
Math and implementation inconsistency
50.00%
Numerical instability
25.00%
Reference-oracle mismatch Residual API misuse
12.50% 12.50%
Semantic mismatch between expected algebraic behavior and TVM execution Precision-sensitive behavior exposed by tensor algebra checks Failure requires oracle-side inspection Remaining operationalization issue after validation
API misuse Invalid model construction Incomplete pytest fixture generation TVM DSL misuse Python syntax error Incorrect property logic
60.56% 34.85% 3.91% 0.28% 0.06% 0.34%
Calls APIs that do not exist or have the wrong interface Generated Relax models are malformed Test requires fixtures that are not generated Misuses TVM’s Python DSL or TVMScript surface Generated Python file cannot be parsed Runnable test checks the wrong property relation
Input validation error
94.86%
Model compilation error
5.14%
Invalid inputs rejected before semantic compiler behavior is exercised Generated models reach compilation but fail before property checking
Error Classification
Table 3 compares the error distributions produced by the three testing strategies. For fuzzing, nearly all errors are input-validation failures: 94.86% of fuzzing errors are input validation errors, while only 5.14% reach model compilation. This distribution indicates that unguided generation spends most of its effort producing inputs that TVM rejects before compiler semantics are exercised. LLM-only PBT introduces a different failure mode: most erroneous generated tests never become runnable property tests. The dominant pattern is operationalization failure rather than a failed semantic oracle. For example, generated tests called APIs that do not exist in the configured runtime, such as rng.randint(...) on np.random.Generator or tvm.nd.array(...) through a missing tvm.nd namespace. Other tests failed before execution because they expected an undefined pytest fixture such as vm, used symbolic dimensions such as n before defining them, or contained mismatched parentheses. These examples show that direct LLM generation can produce plausible-looking tests, but many failures occur before the generated test reaches a meaningful property check. In contrast, P ROPILOT’s classified failures are concentrated in semantically meaningful categories. Among P ROPILOT’s property-based testing failures, 50.00% are math and implementation inconsistencies, 25.00% are numerical instability, 12.50% are reference-oracle mismatches, and 12.50% are residual API misuse. Compared with fuzzing, P ROPILOT substantially reduces failures that occur before semantic compiler behavior is exercised. Compared with LLM-only PBT, P ROPILOT reduces operationalization failures by validating property applicability, generated test structure, and runtime safety before execution. 4.2
Failure Detection Capability
Numerical Issues. We detected floating-point errors when instantiating tensor decomposition as the oracle and evaluating three categories of TVM operators: elementwise, mask-based, and reduction-like operators. For reduction-like operators, geometric decomposition exposed mismatches in sum, mean, and prod, where the results computed on the full input tensor and the recomposed results obtained from partitioned tensors were inconsistent. For example, we applied sum to a tensor containing 2,042 elements, each equal to 9,035 in 32-bit floating point. The mathematically expected result is 18,449,470, which is also the value obtained from the decomposed computation. However, the reduction over the original full tensor produced 18,449,656. We observed that after accumulating the first 2,041 elements, the intermediate result was still correct: 18, 440, 435(= 2041 × 9, 035). The error occurred when adding the final element, i.e., 9,035, to this intermediate sum. This mismatch is caused by floating-point precision loss in IEEE 754 single precision. The intermediate sum and the final addend have different magnitudes, so aligning them discards significant bits from 9,035. When the same computation is performed in float64, both the full and decomposed computations produce the expected result. Takeaway. These findings highlights the distinction between generating a large amount of tests and generating semantically useful tests. LLM-only PBT produces high coverage but many non-runnable or logically invalid tests, and fuzzing is dominated by input-validation errors. In contrast, P ROPILOT uses tensor algebra property skeletons, validation, and feedback to steer generation toward tests whose 6
Figure 2: Cumulative branch, line, and function coverage over a 24-hour TVM testing campaign. failures are more likely to represent meaningful compiler behavior. 4.3
Coverage Growth
Figure 2 reports cumulative branch, line, and function coverage over 24 hours. Overall, the LLM-only PBT baseline reaches the highest coverage, while P ROPILOT ranks second and covers slightly more code than fuzzing in each coverage. This result shows that code coverage can be misleading for evaluating property-based compiler testing. The additional coverage achieved by LLM-only PBT therefore does not necessarily come from exercising deeper compiler optimization logic. Instead, much of the increase is caused by generated tests entering paths for invalid API usage, invalid model construction, unsupported shapes, or incomplete fixtures. As discussed in Section 4.1, these paths increase line and branch coverage while contributing little semantic testing value. LLM-only PBT covers more code than fuzzing because the LLM explores more unconstrained and varied invalid tests, which enter a wider range of input-validation and error-handling paths. In contrast, P ROPILOT is intentionally more constrained: it filters generated tests through property applicability and runtime-safety checks before execution, so its coverage is more conservative but more directly tied to meaningful compiler behavior.
5
Related Work
Oracle Design for DL Compiler Testing. Prior work on testing DL compilers has made progress in generating valid and diverse test cases Liu et al. (2022; 2023a;b); Wang et al. (2023); Deng et al. (2022); Ma et al. (2023); Mu et al. (2025); Limpanukorn et al. (2025); Shen et al. (2025). For example, Tzer mutates TVM IR together with compiler pass sequences and uses coverage feedback to exercise tensor-compiler transformations Liu et al. (2022), while OATest injects optimization patterns from documented tests into seed graphs to exercise optimization paths Shen et al. (2025). However, these approaches mainly strengthen the generation side and often use crashes, compilation failures, runtime exceptions, or crossimplementation output differences as oracle signals. Our work is complementary. In P ROPILOT, algebraic properties are encoded as explicit, reusable checks, so semantic consistency is not treated as ad hoc post-processing. Property-Based and Metamorphic Testing. Property-based testing checks whether generated inputs satisfy general behavioral invariants Claessen and Hughes (2000). Metamorphic testing addresses the oracle problem by checking relations between source and follow-up executions when exact expected outputs are hard to obtain Chen et al. (2020); Zhou et al. (2024). We combine these two ideas in unified workflow andoperationalize the relational-oracle view at the tensor-operator level. In P ROPILOT, each property is paired with applicability conditions, data generators, and assertion templates. Thus, properties are not isolated hand-written tests, but reusable templates that can be mapped to many operators. Tensor and Linear Algebra Rules in DL Compilers. Algebraic identities from linear algebra have long been used to justify DL compiler optimizations and graph rewrites Jia et al. (2019); Yang et al. (2021); Willsey et al. (2021). For example, TASO Jia et al. (2019) automatically generates graph substitutions for DNN computation graphs from operator specifications, and its follow-up work TenSat Yang et al. (2021) uses equality saturation to represent many equivalent tensor graphs at once before extracting an optimized graph. These works use algebraic rules mainly as optimization rules. In contrast, we use them as testing invariants. For example, rather than using an identity such as sum(concat( x1 , x2 )) = sum( x1 ) + sum( x2 ) only to rewrite a graph, we execute both sides and check whether the compiler preserves the relation 7
under concrete shape, dtype, axis, and tolerance constraints. LLM- and Agent-Assisted Test Generation. Recent work has explored LLMs as test generators and fuzzing engines. For example, TitanFuzz Deng et al. (2023) uses generative and infilling LLMs to generate and mutate valid DL programs for testing DL libraries. FuzzGPT Deng et al. (2024) further guides LLMs with historical bug-triggering programs to produce more unusual edge cases. Other work uses execution or coverage feedback to improve generated tests. For example, CoverUp Altmayer Pizzorno and Berger (2025) prompts an LLM with coverage information, and TestForge Jain and Goues (2025) iteratively refines generated unit tests using execution and coverage feedback. Recent oracle-generation work also shows that LLMs can synthesize assertions, but that oracle correctness remains a central challenge Hossain and Dwyer (2025); Konstantinou et al. (2024). Our approach uses agents in a more constrained role. Agents select and compose tests from explicit registries of properties, operator mappings, and data-generation strategies, and these tests are then validated before execution. This design keeps the automation and scalability benefits of agents while preserving auditability and semantic control. Takeaways. Overall, our work connects these lines of research by combining strong oracle design, structured property instantiation, and agent-assisted test synthesis. The main distinction is not simply that we use algebraic properties, but that we organize them into a controlled property-base test generation framework that is easy to scale across operators and compiler targets.
6
Conclusion
P ROPILOT is an agentic property-based testing framework for DL compilers. Rather than treating test generation as only the problem of producing well-formed model inputs, P ROPILOT bootstraps executable PBTs from tensor algebra property skeletons. It represents algebraic relations as reusable skeletons, instantiates them with compiler operators and tensor inputs through controlled generation, and validates generated tests before execution to avoid invalid or uninformative tests.
Our evaluation on TVM shows that this structure reduces repeated or invalid LLM-generated PBTs while shifting testing beyond input validation. More broadly, P ROPILOT shows how tensor algebra can be used not only as mathematical background, but as reusable testing knowledge for checking whether DL compiler optimizations preserve executable semantic relations.
References Juan Altmayer Pizzorno and Emery D. Berger. 2025. CoverUp: Effective High Coverage Test Generation for Python. Proc. ACM Softw. Eng. 2, FSE, Article FSE128 (June 2025), 23 pages. doi:10.1145/3729398 Tianqi Chen, Thierry Moreau, Ziheng Jiang, Lianmin Zheng, Eddie Yan, Meghan Cowan, Haichen Shen, Leyuan Wang, Yuwei Hu, Luis Ceze, Carlos Guestrin, and Arvind Krishnamurthy. 2018. TVM: an automated end-to-end optimizing compiler for deep learning. In Proceedings of the 13th USENIX Conference on Operating Systems Design and Implementation (Carlsbad, CA, USA) (OSDI’18). USENIX Association, USA, 579–594. T. Y. Chen, S. C. Cheung, and S. M. Yiu. 2020. Metamorphic Testing: A New Approach for Generating Next Test Cases. arXiv:2002.12543 [cs.SE] https://arxiv.org/abs/2002.12543 Koen Claessen and John Hughes. 2000. QuickCheck: a lightweight tool for random testing of Haskell programs. SIGPLAN Not. 35, 9 (Sept. 2000), 268–279. doi:10.1145/357766.351266 Yinlin Deng, Chunqiu Steven Xia, Haoran Peng, Chenyuan Yang, and Lingming Zhang. 2023. Large Language Models Are Zero-Shot Fuzzers: Fuzzing Deep-Learning Libraries via Large Language Models. In Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis (Seattle, WA, USA) (ISSTA 2023). Association for Computing Machinery, New York, NY, USA, 423–435. doi:10.1145/3597926.3598067 Yinlin Deng, Chunqiu Steven Xia, Chenyuan Yang, Shizhuo Dylan Zhang, Shujing Yang, and Lingming Zhang. 2024. Large Language Models are Edge-Case Generators: Crafting Unusual Programs for Fuzzing Deep Learning Libraries. In Proceedings of the IEEE/ACM 46th International Conference on Software Engineering (Lisbon, Portugal) (ICSE ’24). Association for Computing Machinery, New York, NY, USA, Article 70, 13 pages. doi:10.1145/3597503.3623343 Yinlin Deng, Chenyuan Yang, Anjiang Wei, and Lingming Zhang. 2022. Fuzzing deep-learning libraries via automated relational API inference. In Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (Singapore, Singapore) (ESEC/FSE 8
2022). Association for Computing Machinery, New York, NY, USA, 44–56. doi:10.1145/3540250. 3549085 George Fink and Matt Bishop. 1997. Property-based testing: a new approach to testing for assurance. SIGSOFT Softw. Eng. Notes 22, 4 (July 1997), 74–80. doi:10.1145/263244.263267 Soneya Binta Hossain and Matthew B. Dwyer. 2025. TOGLL: Correct and Strong Test Oracle Generation with LLMs. In Proceedings of the IEEE/ACM 47th International Conference on Software Engineering (Ottawa, Ontario, Canada) (ICSE ’25). IEEE Press, 1475–1487. doi:10.1109/ICSE55347.2025.00098 Kush Jain and Claire Le Goues. 2025. TestForge: Feedback-Driven, Agentic Test Suite Generation. arXiv:2503.14713 [cs.SE] https://arxiv.org/abs/2503.14713 Zhihao Jia, Oded Padon, James Thomas, Todd Warszawski, Matei Zaharia, and Alex Aiken. 2019. TASO: optimizing deep learning computation with automatic generation of graph substitutions. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (Huntsville, Ontario, Canada) (SOSP ’19). Association for Computing Machinery, New York, NY, USA, 47–62. doi:10.1145/3341301.3359630 Tian Jin, Gheorghe-Teodor Bercea, Tung D Le, Tong Chen, Gong Su, Haruki Imai, Yasushi Negishi, Anh Leu, Kevin O’Brien, Kiyokuni Kawachiya, et al. 2020. Compiling onnx neural network models using mlir. arXiv preprint arXiv:2008.08272 (2020). Fredrik Kjolstad, Shoaib Kamil, Stephen Chou, David Lugato, and Saman Amarasinghe. 2017. The tensor algebra compiler. Proc. ACM Program. Lang. 1, OOPSLA, Article 77 (Oct. 2017), 29 pages. doi:10.1145/3133901 Michael Konstantinou, Renzo Degiovanni, and Mike Papadakis. 2024. Do LLMs generate test oracles that capture the actual or the expected program behaviour? arXiv:2410.21136 [cs.SE] https://arxiv.org/ abs/2410.21136 Ben Limpanukorn, Jiyuan Wang, Hong Jin Kang, Zitong Zhou, and Miryung Kim. 2025. Fuzzing MLIR Compilers with Custom Mutation Synthesis. In Proceedings of the IEEE/ACM 47th International Conference on Software Engineering (Ottawa, Ontario, Canada) (ICSE ’25). IEEE Press, 217–229. doi:10. 1109/ICSE55347.2025.00037 Jiawei Liu, Jinkun Lin, Fabian Ruffy, Cheng Tan, Jinyang Li, Aurojit Panda, and Lingming Zhang. 2023a. NNSmith: Generating Diverse and Valid Test Cases for Deep Learning Compilers. In Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2 (Vancouver, BC, Canada) (ASPLOS 2023). Association for Computing Machinery, New York, NY, USA, 530–543. doi:10.1145/3575693.3575707 Jiawei Liu, Jinjun Peng, Yuyao Wang, and Lingming Zhang. 2023b. NeuRI: Diversifying DNN Generation via Inductive Rule Inference. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (San Francisco, CA, USA) (ESEC/FSE 2023). Association for Computing Machinery, New York, NY, USA, 657–669. doi:10.1145/3611643.3616337 Jiawei Liu, Yuxiang Wei, Sen Yang, Yinlin Deng, and Lingming Zhang. 2022. Coverage-guided tensor compiler fuzzing with joint IR-pass mutation. Proc. ACM Program. Lang. 6, OOPSLA1, Article 73 (April 2022), 26 pages. doi:10.1145/3527317 Haoyang Ma, Qingchao Shen, Yongqiang Tian, Junjie Chen, and Shing-Chi Cheung. 2023. Fuzzing Deep Learning Compilers with HirGen. In Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis (Seattle, WA, USA) (ISSTA 2023). Association for Computing Machinery, New York, NY, USA, 248–260. doi:10.1145/3597926.3598053 Yanzhou Mu, Juan Zhai, Chunrong Fang, Xiang Chen, Zhixiang Cao, Peiran Yang, Kexin Zhao, An Guo, and Zhenyu Chen. 2025. Improving Deep Learning Framework Testing with Model-Level Metamorphic Testing. Proc. ACM Softw. Eng. 2, ISSTA, Article ISSTA095 (June 2025), 23 pages. doi:10.1145/3728972 Rohan Padhye, Caroline Lemieux, and Koushik Sen. 2019a. JQF: Coverage-Guided Property-Based Testing in Java. In Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis (Beijing, China) (ISSTA 2019). Association for Computing Machinery, New York, NY, USA, 398–401. doi:10.1145/3293882.3339002 Rohan Padhye, Caroline Lemieux, Koushik Sen, Mike Papadakis, and Yves Le Traon. 2019b. Semantic Fuzzing with Zest. In Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis (Beijing, China) (ISSTA 2019). Association for Computing Machinery, New York, NY, USA, 329–340. doi:10.1145/3293882.3330576 9
Qingchao Shen, Haoyang Ma, Junjie Chen, Yongqiang Tian, Shing-Chi Cheung, and Xiang Chen. 2021. A comprehensive study of deep learning compiler bugs. In Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (Athens, Greece) (ESEC/FSE 2021). Association for Computing Machinery, New York, NY, USA, 968–980. doi:10.1145/3468264.3468591 Qingchao Shen, Zan Wang, Haoyang Ma, Yongqiang Tian, Lili Huang, Zibo Xiao, Junjie Chen, and Shing-Chi Cheung. 2025. Optimization-Aware Test Generation for Deep Learning Compilers. arXiv:2511.18918 [cs.SE] https://arxiv.org/abs/2511.18918 Zihan Wang, Pengbo Nie, Xinyuan Miao, Yuting Chen, Chengcheng Wan, Lei Bu, and Jianjun Zhao. 2023. GenCoG: A DSL-Based Approach to Generating Computation Graphs for TVM Testing. In Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis (Seattle, WA, USA) (ISSTA 2023). Association for Computing Machinery, New York, NY, USA, 904–916. doi:10.1145/ 3597926.3598105 Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021. egg: Fast and extensible equality saturation. Proc. ACM Program. Lang. 5, POPL, Article 23 (Jan. 2021), 29 pages. doi:10.1145/3434304 Yichen Yang, Phitchaya Mangpo Phothilimtha, Yisu Remy Wang, Max Willsey, Sudip Roy, and Jacques Pienaar. 2021. Equality Saturation for Tensor Graph Superoptimization. arXiv:2101.01332 [cs.AI] https://arxiv.org/abs/2101.01332 Chijin Zhou, Bingzhou Qian, Gwihwan Go, Quan Zhang, Shanshan Li, and Yu Jiang. 2024. PolyJuice: Detecting Mis-compilation Bugs in Tensor Compilers with Equality Saturation Based Rewriting. Proc. ACM Program. Lang. 8, OOPSLA2, Article 317 (Oct. 2024), 27 pages. doi:10.1145/3689757
10