Source note
Agentic Proof and Property-Based Testing via Property-Templates in Data-Intensive Computing
Property Based TestingFormal VerificationAgentic Software EngineeringSpark TestingCode Generation Validation
Summary
DualVeri uses reusable property templates to help agents prove and test recurring correctness properties in Apache Spark. It combines Lean 4 proofs over a Spark model with property-based tests against PySpark, reducing synthesis errors and cost across 400 candidate properties.
Problem
- AI-generated code increases the supply of candidate properties, but validating whether each property is correct and whether its test checks the intended behavior remains expensive.
- Data-intensive systems contain large families of similar properties, yet shared structure does not guarantee truth; the study cites 37,971 type-consistent aggregation candidates, including false claims such as global mean equaling the mean of partition means.
- Formal proof covers a model and all modeled inputs, while property-based testing exercises the real implementation. Using only one can miss model gaps or implementation failures.
Approach
- DualVeri expresses four Spark property families as parameterized templates with typed holes: aggregation decomposition, UDF rewrite, higher-order expression rewrite, and operator subsumption.
- A proof template pre-proves the reusable lift from a local law to a pipeline-level theorem. The agent fills the property-specific holes and proves only the local law in Lean 4.
- A PBT template generates typed data, surrounding Spark workloads, and executable checks against PySpark. The agent fills the same property-specific holes instead of writing each test architecture from scratch.
- The study evaluates 100 candidate properties per family, or 400 total, and compares template-guided synthesis with template-free proof and PBT synthesis.
- Proof and testing results are cross-checked: a passing test with no proof suggests missing formal modeling, while a counterexample to a proved property exposes a model-to-runtime mismatch.
Results
- Property templates increased successful agentic proof synthesis by up to 2.6x, with a 1.6x average improvement, and reduced proof hallucinations by 59% at lower cost.
- Template-guided PBT reduced intent misalignments from 22 to 1 and lowered synthesis cost by up to 5.7x, with a 3.8x average reduction.
- The four templates produced 136 successfully synthesized proofs and 387 faithful property-based tests.
- Template-guided PBT exceeded a state-of-the-art Spark fuzzer on code coverage and approached unguided LLM-based PBT.
- The two tracks produced both a proof and a passing test for 130 properties, while disagreements identified gaps between the Lean model and PySpark runtime semantics.