Technical Summary: Agentic Proof and Property-Based Testing via Property-Templates in Data-Intensive Computing

Problem Statement

As AI-driven code generation becomes cheaper, the primary bottleneck in software engineering has shifted from code synthesis to intent specification and validation. Validating correctness properties for data-intensive systems (such as Apache Spark) at scale presents a "durability crisis." Traditional approaches face two core challenges:

1. Scalability of Validation: Manually verifying that candidate properties are correct and exercising them on real implementations is laborious and does not scale.
2. AI Hallucination and Misalignment: Large Language Models (LLMs) can propose properties and generate tests, but they often produce "hallucinated" proofs (compiling but logically vacuous) or tests that silently check weaker claims than intended (intent misalignment).

While formal proof and Property-Based Testing (PBT) are complementary—proofs verify correctness over a model, while PBT exercises the real implementation—applying both to thousands of candidate properties requires solving the subproblems of verifying candidate correctness and operationalizing PBT without AI errors.

Methodology: DUALVERI and Property Templates

The authors propose DUALVERI, a dual-track validation framework that leverages Property Templates to address these challenges. The core hypothesis is that recurring correctness patterns in data-intensive systems can be abstracted into parameterized forms with "typed holes," which an AI agent can fill to generate specific instances.

1. Property Templates

The authors identify four recurring families of correctness properties in Apache Spark:

• Aggregation Decomposition (AGGDECOMP): Relates a global aggregate to the recombination of per-partition aggregates (e.g., global sum = sum of per-partition sums).
• UDF Rewrite (UDF): States that an opaque User-Defined Function is equivalent to a built-in expression the engine can optimize.
• Higher-Order Expression Rewrite (HOE): Substituting a pointwise-equivalent expression preserves output regardless of the consuming operator.
• Operator Subsumption (SUBSUMP): An operator's output stands in a fixed multiset relation to its input (e.g., filter output is a subset of input).

Each family is codified into a Property Template, which exists in two synchronized forms:

• Proof Template: A parameterized Lean 4 theorem. It pre-proves the "lift" (the logic that extends a local law to a global pipeline) and leaves only a local law (specific to the instance's components) as the obligation for the agent to prove.
• PBT Template: A generator interface that fixes the test architecture (workload generation, execution harness, and comparison logic) and exposes only the property-specific computation as holes for the agent to fill.

2. Agentic Validation Tracks

The framework employs two agentic methods to instantiate these templates:

• Agentic Proof Synthesis: An LLM agent fills the holes in the proof template and proves the local law against a custom Lean 4 model of PySpark's core API. The pre-proved lift then automatically yields the full pipeline-level theorem.
• Agentic PBT Synthesis: An LLM agent fills the holes in the PBT template to generate executable PySpark tests. The template ensures the test varies the surrounding workload and correctly operationalizes the property, avoiding the "fixed workload" and "missing UDF coverage" issues found in unconstrained LLM generation.

Key Contributions

1. Property Templates: The identification and abstraction of recurring correctness principles in data-intensive systems into parameterized forms that capture shared proof structures and test generation machinery in a single artifact.
2. Dual-Track Agentic Framework: The development of an agentic prover (for Lean 4) and an agentic test synthesizer (for PySpark) that utilize these templates to validate properties at scale.
3. Constrained Synthesis: Demonstrating that narrowing the LLM's task to filling specific template holes significantly improves success rates and reduces hallucinations and costs compared to unconstrained synthesis.
4. Cross-Validation: A methodology for comparing formal proofs and PBT results to identify gaps between formal models and runtime semantics.

Experimental Results

The framework was evaluated on 400 candidate properties (100 per family) against template-free baselines.

Proof Synthesis Track

• Success Rate: Property templates increased machine-checked synthesis successes by up to 2.6× (average 1.6×), generating 136 successful proofs compared to 90 without templates.
• Hallucination Reduction: Templates reduced proof hallucinations (proofs that compile but prove nothing of interest) by 59%. Specifically, they eliminated all hallucinations in the UDF family and reduced them in the AGGDECOMP family.
• Cost: Templates reduced the cost per property attempted by 14–32% (average 23%).

PBT Synthesis Track

• Faithfulness: Template-guided synthesis increased faithful test generation (tests that execute and match the natural language description) from 92.8% to 96.8%.
• Intent Misalignment: The number of tests with intent misalignments dropped from 22 to 1.
• Cost: Synthesis costs were reduced by up to 5.7× (average 3.8×), primarily due to a reduction in reasoning tokens.
• Coverage: Template-guided synthesis exceeded the code coverage of the state-of-the-art Spark fuzzer (COMETFUZZ) and approached the coverage of unguided LLM-based PBT, while uniquely covering UDF-to-builtin correspondences that unguided synthesis missed.

Cross-Validation

• Agreement: For 130 properties, both the formal proof and the PBT provided supporting evidence, offering the strongest validation.
• Disagreement as Diagnosis:
  • Model Gaps: In one case, a proof succeeded while a PBT found a counterexample, revealing a gap in the Lean model regarding nullable arrays (the model assumed non-null, while PySpark allows nulls).
  • Model Extensions: For 251 properties, PBTs passed but proofs failed, indicating areas where the formal model needs extension (e.g., adding support for specific array operations or join semantics).

Significance and Claims

The paper claims that property templates are a decisive mechanism for scaling the validation of AI-generated code in data-intensive systems. By abstracting recurring structural patterns, templates allow agents to focus on the specific, variable components of a property rather than re-deriving complex proof strategies or test architectures from scratch.

The authors emphasize that this approach yields stronger evidence than either proof or testing alone. The dual-track approach not only validates correctness but also serves as a diagnostic tool:

• When a proof succeeds but a PBT fails, it exposes a model-to-implementation gap.
• When a PBT passes but a proof fails, it highlights areas where formalization needs to be extended.

The paper concludes with a cautionary note: while templates reduce the risk of AI hallucination, a machine-checked proof only guarantees the theorem under its stated definitions. It does not guarantee that the definitions faithfully express the intended property. Therefore, human inspection remains necessary to audit definitions for faithfulness and detect "formalization gaming." The work positions property templates as a critical step toward trustworthy, AI-assisted verification, bridging the gap between informal intent and rigorous validation.