arXiv CSopen access

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

arXiv:2607.09072v1 [cs.SE] 10 Jul 2026

Agentic Proof and Property-Based Testing via Property-Templates in Data-Intensive Computing Seongmin Lee*

Yaoxuan Wu*

Miryung Kim

University of California, Los Angeles Los Angeles, CA, USA [email protected]

University of California, Los Angeles Los Angeles, CA, USA [email protected]

University of California, Los Angeles Los Angeles, CA, USA [email protected]

Abstract—As the cost of code generation becomes cheaper with AI, the new bottleneck in software engineering has shifted to intent specification and validation. Overcoming this durability crisis of AI-driven coding requires more than traditional fuzzing: each candidate property must be both proven correct over a model of the system and shown to hold on the real implementation, making formal proof and systematic property-based testing (PBT) complementary. However, validating properties this way at scale requires solving two core subproblems: (1) verifying that candidate properties are indeed correct, and (2) operationalizing PBT without AI hallucination. We hypothesize that recurring property patterns, cast as property templates—abstract, parameterized forms with holes—address both subproblems at once. This paper investigates the value of recurring property patterns in a target system, Apache Spark. In data-intensive scalable computing systems, numerous correctness properties arise from the principles of data partition, computation decomposition, and data-flow computation. For instance, a classic recurring pattern is aggregation decomposition, where, for all data D and workloads Q, a global function executed on the entire dataset relates to a local function followed by a recombiner. We design an agentic, dual-track validation framework that uses property templates to formally verify their correctness in the Lean 4 theorem prover, and instantiate PBT templates as concretized executable PBTs. Our evaluation shows that property templates increase agentic proof engineering success by up to 2.6× (avg: 1.6×) and reduce proof hallucinations by 59%. Template-guided PBT synthesis reduces intent misalignments from 22 to 1 and cuts synthesis cost by up to 5.7× (avg: 3.8×). Template-guided synthesis further exceeds a state-of-the-art Spark fuzzer and approaches unguided LLM-based PBT on code coverage. Finally, comparing the two tracks is informative: for example, when a proof succeeds yet a PBT finds a counterexample, the mismatch identifies a gap between the formal model and the implementation.

I. I NTRODUCTION Establishing that a software system behaves as intended rests on two complementary validation techniques. This behavior is captured as a specification—a conjectured property the system should satisfy. Formal proof [1] mathematically verifies it against a model of the system, while property-based testing (PBT) [2], [3], [4] exercises the real implementation on many generated inputs. The two are complementary: a proof determines whether the property is in fact correct, while PBT tests whether the implementation actually obeys it. Applying both therefore yields far stronger evidence than either alone. * Seongmin Lee and Yaoxuan Wu contributed equally to this work.

A real software system’s correctness hinges on complex, endto-end properties of its behavior. For example, a query should return the same results whether or not the engine optimizes it, for every input dataset, rather than merely producing the correct output for a single function. Many such properties must be validated, including the correctness of each optimization, rewrite, and equivalence on which the engine relies. Validating even one property through a machine-checked proof, an executable test, or both is laborious. Repeating this process by hand, property after property, does not scale. Language models can now propose candidate properties at scale [5], [6], but this only sharpens the validation problem: a proposed property may be subtly false, and a generated test may silently check something weaker than intended. The problem we address is how to validate these properties at scale by confirming that each is correct and exercising it as intended. Data-intensive systems such as Apache Spark [7] are built on a few underlying principles—partitioning data across a cluster, decomposing computation over the partitions, and composing operators into dataflow pipelines. These principles make a system’s correctness properties recur: the same structural relationship reappears as a family of closely related properties across the API. Aggregation decomposition is one such family. It relates a global aggregate to the recombination of perpartition aggregates, with one member for every aggregator: a global sum equals the sum of per-partition sums, a global max equals the maximum of per-partition maxima, and so on. A second family, UDF rewrite, captures a different relationship. It states that an opaque user-defined function is equivalent to a built-in expression that the engine can optimize. For instance, a Python UDF that uppercases a string is equivalent to the built-in upper, with one member for every replaceable UDF. Each family is also vast and not uniformly true: aggregation decomposition, for instance, does not hold for the mean, since a global mean does not equal the mean of per-partition means. Telling such false members apart is hard at scale, as the family admits 37,971 type-consistent instantiations, many of which type-check yet are false. Validating so many candidates, true and false alike, by hand is infeasible. We therefore exploit this recurrence with two pieces: a property template that codifies a family’s shared structure once as a parameterized form with typed holes, and agentic methods that turn it into a machine-checked proof and an executable test

of each concrete member. A single template takes two forms Generate a potential property over the same property: a proof template, a parameterized Lean 4 theorem that reduces an instance’s proof to one local obligation which lifts to the full property by construction; and Proof-Engineering Property-based Testing a PBT template, a generator that turns the same instance into a Prove whether it is a correct Test whether it holds diverse, executable test of the real system. For each form, the property on a model true on a real system agent fills only the template’s property-specific holes—rather Serve as a conjecture worth proving than re-deriving a proof or re-authoring a test from scratch—so Proof: ?? PBT: ✓ that the cost of validation is amortized across the whole family. Must hold in a real system PBT: ?? Proof: ✓ We build property templates for four families of Spark properties whose violation silently corrupts results: aggregation Fig. 1: Proof and property-based testing each supply the decomposition, UDF rewrite, higher-order expression rewrite, evidence the other lacks when validating a property. and operator subsumption. We evaluate them on 100 candidate properties per family, for 400 properties in total, against for all inputs; written in a proof assistant such as Lean, Rocq, template-free baselines on both tracks. On the proof track, or Isabelle, it is verified by the tool itself, yielding a machinea pre-verified proof structure raises machine-checked synthesis checked guarantee [1], [8], [9]. PBT instead checks a property successes by up to 2.6× (avg: 1.6×) and reduces hallucinated on the real implementation [2]: rather than a single input and proofs, which compile but prove nothing of interest, by 59%, its expected output, as in a conventional test, one writes a at lower cost. On the PBT track, fixing the test architecture property meant to hold for all inputs together with a generator cuts intent misalignments in synthesized tests (from 22 to 1) that produces many varied, well-formed inputs, and checks the and LLM synthesis cost by up to 5.7× (avg: 3.8×). Finally, property on each, shrinking any counterexample to a minimal the two tracks corroborate each other on 130 properties that case. Because a single model and its generators yield large earn both a proof and a passing test, and disagree informatively volumes of tests, PBT can drive system-level testing of complete elsewhere: a passing PBT without a proof identifies properties implementations, not just unit checks [10]. This scale makes that may benefit from broader formal modeling, whereas a PBT a practical vehicle for specification validation: AWS’s Kiro PBT counterexample to a proven property exposes a mismatch turns a natural-language specification into executable properties between the Lean model and PySpark runtime semantics. checked against the (increasingly AI-written) code [11]. This paper makes the following contributions: Proof and PBT are symbiotic rather than redundant (Figure 1): • We identify the recurring principles behind the correcta proof gives a sound guarantee over a model of all inputs, ness properties of data-intensive systems and abstract each while PBT gives empirical evidence from the real system on resulting family of properties into a property template: many, so each reaches evidence the other cannot. A property a parameterized form with typed holes that captures the that survives extensive testing is worth proving, both to extend family’s shared proof and shared test in a single artifact; in the guarantee to all inputs and to delineate the scope the formal our evaluation, four such templates produced 136 successfully model must capture. A proved property, in turn, still calls for synthesized proofs and 387 faithful PBTs. empirical evidence: should a test find a counterexample, either • To validate properties at scale, we develop two templatethe proof is unsound or a gap separates the model from the guided agentic methods: an agentic prover that synthesizes implementation. Agreement along both tracks is the strongest machine-checked Lean 4 proofs over a model of PySpark’s evidence of all. core API, and an agentic test synthesizer that produces executable PySpark tests. B. Recurring Properties in DISC • Narrowing the LLM to the template’s holes is decisive: a) DISC: Data-Intensive Scalable Computing Systems: on the proof track, synthesis successes rise by up to 2.6× Data-intensive scalable computing (DISC) systems such as and hallucinations fall by 59%; on the PBT track, intent Apache Spark [7] process datasets too large for a single machine misalignments fall from 22 to 1 at up to 5.7× lower cost, by partitioning the data across a cluster and computing over compared with template-free synthesis of the same property. the partitions in parallel. Unlike a classical relational database, • We cross-validate the two tracks against each other: their where the user issues a declarative query and the engine owns agreement gives the strongest evidence available, while their the entire execution plan, a DISC program is an explicit pipeline disagreement surfaces model-to-implementation gaps neither of coarse-grained transformations— map , filter, groupBy, finds alone. join, and user-defined functions—that the framework compiles into a distributed dataflow DAG and executes lazily (Figure 2, II. BACKGROUND AND M OTIVATION left). Because this model interleaves relational operators with A. Validating a Specification: Proof and PBT arbitrary user code and exposes partitioning to the program Two methods establish that a system satisfies a specification: itself, the engine’s freedom to optimize rests on structural formal proof and property-based testing (PBT). A proof reasons invariants governing how operators commute, distribute, and deductively over a model of the system to establish a property recombine across partitions. Such invariants recur throughout

1 DISC computation ⃝

2 The aggregation-decomposition family ⃝ aggregator

relation

3 A cheaper, equivalent plan ⃝

agg(

expensive: all rows cross the shuffle

recombiner

workload Q

DataFrame D

) R recombine( agg(

), . . . , agg(

shuffle

))

agg

map join

agg

global count ≥ largest per-partition count count(

) ≥ max( count(

), . . . , count(

))

cheap: pre-aggregate; only partials cross the shuffle

scan

agg agg agg

distinct values = union of per-partition distinct sets unique( A workload Q runs over a DataFrame D partitioned across a cluster as a lazy dataflow DAG of operators.

) = ∪( unique(

), . . . , unique(

))

Choosing an aggregator, a relation, and a recombiner gives a member relating the global aggregation to recombining the partitions.

shuffle

=

recomb

When the relation is ‘=’, the engine pre-aggregates below the shuffle—a cheaper, equivalent plan.

Fig. 2: An example recurring property family, aggregation decomposition, shown end to end.

denotes a DataFrame partition.

DISC and hold for every input dataset and every upstream pipeline. Particularly important are equivalences that enable the system to replace an expensive computation with a cheaper one proved to produce the same result, such as by pre-aggregating below a shuffle.

C. Pilot Study: Using LLMs for PBT Synthesis in DISC

A family’s shared structure makes a system’s true invariants easier to find: by varying its components, one generates candidate properties in bulk. AGG D ECOMP, for instance, is realized by any two of PySpark’s 117 collection-reducing functions—an aggregator and a recombiner—related by any of 9 comparison operators, so it alone yields 117×117×9 = 123,201 candidates, 37,971 of them type-consistent.

We present D UALV ERI, a framework that validates a system’s many correctness properties at scale by making both proving and property-based testing agentic. For each recurring property family of Section II—HOE, UDF, AGG D ECOMP, and S UBSUMP (Table I)—D UALV ERI builds a property template: it parameterizes the family’s shared structure—turning the components that vary across members into typed holes an agent fills—and pairs it with the machinery to prove and test each instance. Our key hypothesis is that such a template makes validating a family’s many properties both accurate and cost-efficient: because the properties share a common proof structure and test-generation machinery, the agent has less to complete on its own, so each proof and test is cheaper to produce and easier to get right. Each property template comes in two forms that share its holes—a proof template for the proof track and a PBT template for the PBT track. The proof template is a parameterized theorem that reduces each proof to a single local law, so the proof agent establishes the property over a model of PySpark’s core API instead of reasoning about the whole computation

We first ask whether a SOTA LLM can synthesize systematic PBTs without DISC-specific structure. Using GPT-5.5 (medium reasoning), we generate 100 PySpark PBTs sequentially, each via plan-then-code; the model sees prior properties’ names and statements to avoid duplication but receives no templates, These invariants come in families. We identify four recurring examples, or execution feedback. families, with examples in Table I: higher-order expression The resulting tests are individually meaningful but collecrewrite (HOE), where substituting a pointwise-equivalent tively unsystematic in two ways. No workload variation: no expression preserves the output whatever operator consumes it; test varies the surrounding operator sequence or embeds the UDF rewrite (UDF), where a Python user-defined function— property in a generated upstream workload; only the input opaque to the engine—rewrites to an equivalent built-in; agdata changes. No UDF coverage: no test creates or invokes gregation decomposition (AGG D ECOMP), where an aggregate a Spark UDF, so none relates a user-defined computation to over the whole dataset equals recombining the same aggregate a built-in. Property templates systematically target selected computed per partition; and operator subsumption (S UBSUMP), property forms, while basic generators vary the surrounding where an operator’s output stands in a fixed multiset relation workloads; we further evaluate both in Section IV-B. to its input. Figure 2 makes one family concrete: its center shows several members of aggregation decomposition, each III. D UALV ERI : P ROPERTY T EMPLATES FOR D UAL -T RACK licensing a cheaper plan. VALIDATION

But this abundance is double-edged: the candidates are too many to check by hand, and sharing the structure is no guarantee of truth—many are false. In AGG D ECOMP, a global mean = the mean of the per-group means silently fails whenever partitions differ in size; in UDF, Python’s x.strip() ≡ F.trim(x) silently fails on Unicode whitespace that Spark’s ASCII-only trim ignores. Both candidate properties are welltyped, but both are false. Which candidates are genuine properties of the family must therefore be determined one at a time, because neither shared structure nor successful typechecking establishes that a candidate is true. Doing so at scale requires automated proof and testing.

TABLE I: Recurring property families in data-intensive computing. Each family is a group of properties that share one structure; the Description highlights the components that vary across members (numbered and colored), and each Example gives members as tuples of those components. Family

Description

Example members

HOE

For every input dataset and any surrounding operations, replacing [1. an expression] with [2. a pointwise-equivalent rewrite] leaves the DataFrame output unchanged, whatever operator consumes it.

[1. size(reverse(arr))] ≡ [2. size(arr)] — reversing preserves length. [1. array_contains(arr,elem)] ≡ [2. array_position(arr, elem) > 0] — present iff the position is positive.

UDF

For every input dataset and any surrounding operations, [1. a Python UDF expression] and [2. an equivalent PySpark built-in] are interchangeable in any DataFrame operation that takes a column expression.

[1. abs(x)] ≡ [2. F.abs(x)] — same absolute value. [1. x[i:j]] ≡ [2. F.substring(x,i+1,j-i)] — same substring (1-based indices).

AGG D ECOMP

For every input dataset and any preceding operations, [1. aggregating] over the whole dataset stands in [2. a fixed relation] to [3. recombining] the same aggregate computed per group.

global [1. count] [2. ≥] [3. max] of the per-group counts. global [1. unique] [2. =] [3. union] of the per-group uniques — distinct values.

S UBSUMP

For every input dataset and any preceding operations, [1. an operator]’s output stands in [2. a fixed multiset relation] to the rows it receives.

[1. orderBy] output [2. =] input as multisets — reorders only. [1. filter] output [2. ⊆] input as multisets.

from scratch. The PBT template is a generator interface that the components alone, and a lift that carries the local law up varies the surrounding workload and encodes the property check to the global statement. We build each proof template around through holes, so the testing agent produces many tests that this split: we pre-prove the lift once per template and leave the correctly operationalize the property on the real implementation. local law as the single obligation an instance must discharge, Filling a template’s holes—for AGG D ECOMP, the aggregator, so the agent never re-derives the global argument. Figure 3 recombiner, and relation—yields a concrete property such as shows this for AGG D ECOMP and UDF: the proof template (count, max, ≥) that both forms carry, validated along a proof (above) is the holed structure—its holes, local law, and pretrack (Section III-A) and a PBT track (Section III-B). proved lift. Given a concrete property, the agent takes four steps using the proof template: (1) fills the template’s holes; Generation of Candidate Properties. Before detailing the two (2) proves the matching local law against our Lean model, tracks (Sections III-A and III-B), we explain how the concrete iterating on the compiler’s feedback until it checks; (3) bundles candidate properties they validate are generated. We prompt the components and proof into a filled template; and (4) reads an LLM with each template’s natural-language definition to off the pipeline-level property from the pre-proved lift. What generate candidate properties. For AGG D ECOMP, the prompt the local law asserts and what the lift ranges over differ by reads: template, which we make concrete next. “You are a research engineer specialising in PySpark semantics. Propose one new aggregation-decomposability property following the triplet structure global_result = recombine(groupBy(key).agg(fn(val))). Output the chosen (aggregator, recombine, relation) ...”

and the LLM returns instances such as (sum, sum, =), (count, sum, =), and (count, max, ≥). A deduplication memory was used across iterations to keep the generated candidates diverse. A. Agentic Proof Synthesis with Proof Template Lean Set Up. Given a candidate property instantiated from a template, we synthesize its proof over a custom Lean 4 model of a subset of PySpark’s core API. The model captures the core semantics a correctness property must refer to—how a DataFrame is represented, how a workload transforms it, and the structural laws that govern these transformations. In total it comprises 17 data types, 71 functions and relations, and 60 theorems; we detail its three layers, the domain-helper and lemma libraries, and representative Lean code below. Agentic Proof Synthesis. A property’s proof is global—it must hold for every input dataset and every upstream workload—but it always splits into a local law, an instance-specific fact about

Aggregation decomposition. The components are an aggregator, a recombiner, and a relation (Figure 3a). The local law decompose_law states, on a single arbitrary DataFrame, that the global aggregation stands in the relation to recombining the per-group aggregations; a single pre-proved theorem .lift extends it to any input run through any upstream workload. For the running instance (count, max, ≥), the agent proves only that a global count is at least the maximum of the per-group counts, and .lift yields the end-to-end property. UDF rewrite. The components are a built-in expression and a user-defined function over the same columns (Figure 3b). The local law equiv_law states that the two agree pointwise—on every input the UDF returns exactly what the built-in does. Here the lift is not a single theorem but a rewrite rule per DataFrame operator: for each operator the expression may sit in (select, filter, orderBy, . . . ), one pre-proved theorem licenses replacing the built-in with the UDF inside that operator without changing any surrounding pipeline’s output. For an instance such as abs (Python abs replaced by PySpark F.abs), the agent proves only the pointwise equivalence, and every such rewrite follows from the template. The two cases differ in where the proof effort falls. For

(a) Proof Template for AggDecomp

Agentic Framework

A holed Lean structure: the 3 holes (aggregator, recombiner, relation) and decompose law — the one fact an instance must prove, on a single DataFrame

structure AggDecompTemplate where aggregator : DB → α recombiner : List α → α relation : α → α → Prop decompose_law : ∀ db, relation (aggregator db) (recombiner ((groupBy key db).map aggregator))

Given a filled Lean structure, .lift extends to hold for any input data and any upstream workload.

lift

def aggregator := count

Concretization 1: def recombiner := max def relation := (· ≥ ·) the global count is at least the pergroup max (count, max, ≥) 1. Define 3 holes for concretization Concretization 2: the global distinct def aggregator := unique def recombiner := union equals the union def relation := (· = ·) of per-group distincts (unique, union, =)

theorem count_ge_max_law (db) : count db ≥ max ((groupBy key db).map count) := by ...

2. Prove the local law

theorem unique_union_law (db) : unique db = union ((groupBy key db).map unique) := by ...

def countGeMax : AggDecompTemplate := { aggregator := aggregator, recombiner := recombiner, relation := relation, decompose_law := count_ge_max_law }

Concretization 1: Python native abs can be equivalently used with PySpark F.abs

A holed Lean structure: the 2 holes (Python UDF expression, PySpark built-in) and equivalence law — two expressions are semantically equivalent def builtin := Expr.abs def UDF := Expr.udf “abs”

def uniqueUnion : AggDecompTemplate := { aggregator := aggregator, recombiner := recombiner, relation := relation, decompose_law := unique_union_law }

Concretization 2: Python native def builtin i j := [i:j] can be Expr.substring i j equivalently used def UDF i j := Expr.udf “substring” (i+1), (j-i) with PySpark substring(_,i+1 ,j-i)

lift

theorem unique_union_decomposition (pre) (db) (key) : unique (pre db) = union ((groupBy key (pre db)).map unique) := uniqueUnion.lift pre db

Given a filled Lean structure, .rewrite[Operator] extends the equivalence for each dataframe operator structure UDFTemplate where builtin : α → β UDF : α → β equiv_law : ∀ x, udf x = builtin x

theorem UDFTemplate.rewriteSelect

lift

theorem UDFTemplate.rewriteFilter theorem UDFTemplate.rewriteOrderBy

theorem abs_select_eq : ABS.rewriteSelect theorem abs_law : ∀ n, UDF n = builtin n := by ...

1. Define 2 holes for concretization

theorem count_ge_max_decomposition (pre) (db) (key) : count (pre db) ≥ max ((groupBy key (pre db)).map count) := countGeMax.lift pre db

4. The final theorem of the target property is automatically derived

3. Construct a filled Lean structure

(b) Proof Template for UDF

Agentic Framework

lift

theorem AggDecompTemplate.lift (t) (pre) (db) (key) : t.relation (t.aggregator (pre db)) (t.recombiner ...) := by …

2. Prove the local law

theorem substring_law : ∀ s i j, UDF s i j = builtin s i j := by ...

def ABS : UDFTemplate := { builtin := builtin, UDF := UDF, equiv_law := abs_law }

theorem abs_filter_eq : ABS.rewriteFilter

lift

4. The final theorem of the target property is automatically derived

3. Construct a filled Lean structure def SUB : UDFTemplate := { builtin := builtin, UDF := UDF, equiv_law := substring_law }

theorem abs_orderby_eq : ABS.rewriteOrderBy

theorem sub_select_eq : SUB.rewriteSelect theorem sub_filter_eq : SUB.rewriteFilter

lift

theorem sub_orderby_eq : SUB.rewriteOrderBy

Fig. 3: Proof templates and their agentic use for the two proof-track families, AGG D ECOMP (a) and UDF (b), and two concretizations per template. The agent fills the holes and proves only the local law (steps 1–3); the template’s pre-proved lift then yields the pipeline-level theorem automatically (step 4). AGG D ECOMP the lift is small, so the local law the agent proves is the harder part; for UDF the pointwise equivalence is usually easy, and the labor shifts to the per-operator lift the template pre-proves. This pre-proved template, written once per property family and reused across its instances, averages 546 non-comment lines of Lean. B. Agentic PBT Synthesis with PBT Template

for PySpark schemas, input data, DataFrame operators, and expression operations. These generators vary not only the input rows but also the workload surrounding the property under test. They compose operators and expressions into different sequences and pipeline shapes, allowing each PBT to exercise the property in a range of workload contexts. The generators are also designed to produce well-formed workloads. They use schema-valid column references and type-compatible expressions, construct DataFrame dependencies as valid acyclic graphs, and enforce operator-specific constraints such as schema compatibility and join-key alignment.

Agentic PBT Synthesis. A property-based test consists of two parts: a property-specific computation and a reusable test architecture. The architecture generates varied, well-formed Aggregation decomposition. The AGG D ECOMP template workloads, executes both sides of the property, and compares (Figure 4a) exposes three holes, AGG, RECOMBINE, and their results end to end. Our PBT templates fix this architecture COMPARE, along with two column-type declarations that and expose only the property-specific computation as holes. select the grouping and aggregation columns from the generated The agent fills these holes, producing a test that runs directly workload W. The template constructs both the global and peragainst PySpark. This separation addresses limitations of PBTs generated from scratch. An unaided LLM typically keeps group computations from the same W and the same columns, the surrounding workload fixed and does not exercise UDFs leaving only the property-specific operations to the agent. As (Section II-C); even when given a property, it may silently test highlighted, the agent sets AGG to F.count, RECOMBINE to a different claim (Section IV-B). Figure 4 shows two templates F.max, and COMPARE to approx_geq. with their property-specific holes filled and highlighted. We UDF rewriting. The UDF template (Figure 4b) exposes two next describe the basic generators used to construct workloads, holes, UDF, the function under test, and BUILTIN, its claimed followed by the two templates. built-in equivalent, along with input and output column types. Basic Generators. We build a library of basic generators The output type also determines where the expression can

import pyspark.sql.functions as F class AggDecompTemplate: 3 partition_col_type = DiscreteType # hole: key type for groupBy (no float) 4 agg_col_type = NumericType # hole: col type for aggregation 5 def AGG(self, col): # hole: aggregation 6 return F.count(col) 7 def RECOMBINE(self, col): # hole: recombination 8 return F.max(col) 9 def COMPARE(self, a, b): # hole: comparison 10 return approx_geq(a, b) 11 def test(self): 12 S = GenSchema(); D = GenData(S) 13 W = GenWorkload(D) 14 col_p = PickTypedCol(W, self.partition_col_type) 15 col_a = PickTypedCol(W, self.agg_col_type) 16 g = W.agg(self.AGG(col_a)) 17 l = (W.groupBy(col_p) 18 .agg(self.AGG(col_a).alias(col_local)) 19 .agg(self.RECOMBINE(col_local))) 20 assert self.COMPARE(g, l)

import pyspark.sql.functions as F class UDFTemplate: 3 input_col_types = [IntegerType] # hole: col type(s) accepted by the UDF 4 output_col_type = IntegerType # hole: col type produced by the UDF 5 def UDF(self, col): # hole: user-defined function

1

1

2

2

(a) AGG D ECOMP template instantiated for the property that the global count is at least the maximum per-group count. The highlighted holes specify F.count, F.max, and the tolerance-aware comparison approx_geq.

6 7 8 9 10 11 12 13 14 15 16 17 18 19

@udf(returnType=IntegerType()) def fn(x): return ˜x return fn(col) def BUILTIN(self, col): # hole: equivalent built-in return F.bitwiseNOT(col) def test(self): S = GenSchema(); D = GenData(S) W = GenWorkload(D) col_in = PickTypedCol(W, self.input_col_types) op = GenOp(self.output_col_type) DW = GenDownstream(self.output_col_type) r_u = DW(op(W, self.UDF(col_in))) r_b = DW(op(W, self.BUILTIN(col_in))) assert self.compare_DF(r_u, r_b)

(b) UDF template instantiated with a user-defined bitwise negation (˜x) and its PySpark built-in counterpart, F.bitwiseNOT. The template evaluates both expressions within otherwise identical pipelines and compares their final DataFrames.

Fig. 4: PBT templates instantiated by the LLM. Highlighted regions are agent-filled property holes, while Gen* and Pick* denote reusable workload generators; the remaining test architecture is fixed by the template. appear; for example, a Boolean output allows operators such TABLE II: Proof synthesis outcomes per property family, over as filter. The template samples an upstream workload W, a the in-scope properties of each. Compiles counts proofs that compatible operator op, and a downstream workload DW. It pass lake build; Success counts proofs that additionally then runs two branches that share the same workloads and pass a manual inspection of the generated Lean file for cheat operator and differ only in whether they use UDF or BUILTIN. patterns (trivial relation, input collapse, etc.); Hallucinated is As highlighted, the agent fills UDF with a @udf-decorated the remainder. Cost is reported per property attempted. bitwise negation and BUILTIN with F.bitwiseNOT. Property Cost/prop Compiles Success Hallucinated (USD) Our PBT-track implementation includes 7,899 LOC of Family (# props) Config generator code and 1,109 LOC of template code. The generators HOE (37) T EMPLATE 28 28 (100%) 0 ( 0%) $0.78 N OT EMP 17 17 (100%) 0 ( 0%) $1.02 support 12 column types, including arrays and maps, 23 T EMPLATE 54 54 (100%) 0 ( 0%) $0.77 DataFrame operators, and 93 expression operations spanning UDF (68) N OT EMP 28 21 ( 75%) 7 (25%) $1.02 aggregation, string, array, window, and higher-order operaT EMPLATE 13 6 ( 46%) 7 (54%) $1.03 AGG D ECOMP (89) tions. N OT EMP 15 5 ( 33%) 10 (67%) $1.17 IV. E VALUATION We evaluate our framework across four property families over PySpark: HOE, UDF, AGG D ECOMP, and S UBSUMP. For each, the generation procedure of Section III instantiates 100 candidate properties—400 in total—the fixed population every experiment below runs on, presented identically to each configuration. Produced automatically from the template’s definition rather than by hand, they span the family broadly and keep the hard and/or invalid properties, so that the evaluation reflects the real-world challenge of property validation. A. Proof Synthesis a) Research Questions: We ask two questions about the effect of the property template on LLM-driven proof synthesis: RQ1. Does the property template improve proof synthesis efficiency, measured in both success rate and LLM cost per property attempted? RQ2. Does the property template reduce proof hallucinations? A successful lake build certifies the proof, not the definition it rests on: it guarantees the theorem follows from

S UBSUMP (49)

T EMPLATE N OT EMP

48 48 (100%) 47 47 (100%)

0 ( 0%) 0 ( 0%)

$0.42 $0.48

its definitions, not that they encode the intended property. An agent can thus pass the compiler while mis-stating the property, assuming vacuous hypotheses, or smuggling in an unsound shortcut—a compiling but misdirected proof we term a proof hallucination. As the compiler cannot catch this, we manually inspect every compiling proof. b) Experimental Setup: Of the 100 properties per family, we retain those that fall within the scope of our Lean 4 model of PySpark’s core API (Section III-A; Table II). Excluded candidates leave the scope for three reasons: (i) primitives absent from the Expr model (higher-order array ops, IEEE754/NaN, regex); (ii) aggregators with no sound pure-functional model (first/last, try_sum); or (iii) operations outside the single-input pipeline (two-input joins), leaving 243 of 400 candidates in scope. We compare two configurations of the same proof-synthesis agent: an LLM that explores the Lean formalization through

the cost gap remains; the paired McNemar test accordingly finds the success difference significant for HOE (p < 0.01) and UDF (p < 10−6 ) but not for AGG D ECOMP or S UBSUMP. The split reflects how much of the proof the template takes over. For HOE and UDF the per-property sub-goal is the easy part; (a) HOE (b) UDF (c) AGG D ECOMP (d) S UBSUMP the real work is lifting it to the operation level and proving it Fig. 5: Synthesis successes per property family: by T EMPLATE across the many DataFrame operators a pipeline may apply, and only (blue), N OT EMP only (red), or both (centre). that lifting is exactly what the pre-verified template supplies (Section III-A). The agent is thus spared designing the overall the lean-lsp MCP toolset and iteratively drafts and revises Lean proof strategy—the step where LLM proof synthesis most often code until it obtains a complete, machine-checked proof of the slips into unstructured low-level tactic search [13]. N OT EMP, target property. The two configurations differ in a single respect: given no template, must invent both the high-level structure and whether the agent is given the relevant property template its Lean proof within one turn budget, which both narrows its (Section III-A). T EMPLATE hands the agent the matching coverage and raises its cost. For AGG D ECOMP and S UBSUMP property template and instructs it to instantiate and apply it. the sub-goal already operates over the DataFrame itself, so little N OT EMP withholds the template—it is neither available to is left to lift—only the extension to an arbitrary initial input nor mentioned to the agent—so the agent must produce the and prefix workload—and T EMPLATE and N OT EMP come whole proof on its own. In both configurations the agent runs out nearly even on synthesis successes, though T EMPLATE under the same budget (GPT-5.5, medium reasoning, max stays cheaper. The two differ in absolute difficulty, though: output tokens=65,536, up to 24 agentic turns) and is asked S UBSUMP is easy enough that both nearly always succeed, to prove the same property. The turn cap is raised to 32 for while AGG D ECOMP’s multi-input aggregation reasoning is AGG D ECOMP, whose proofs do not appear within 24 turns. challenging enough that both configurations fail more often. We report three metrics. Compiles is the number of properties Answer to RQ1. The property template raises synthesis whose final .lean file passes lake build with no sorry. successes from 90 to 136—up to 2.6× per family, averaging Success (a synthesis success) is the subset of compiling 1.6×. T EMPLATE is also cheaper per property in every proofs that we additionally judge, by manual inspection of the family, with N OT EMP spending 14–32% more (avg: 23%). generated Lean file, to actually establish the property’s intended claim rather than a trivially-true substitute; Hallucinated is the remaining compiling proofs. Cost is the client-side USD spent e) Hallucination analysis: Hallucination surfaces only on LLM calls at GPT-5.5 rates ($5/M input, $30/M output, in UDF and AGG D ECOMP, and for a common reason. It reasoning included in output), reported per property attempted. arises from slack in translating a property’s natural-language Because both configurations are evaluated on the same in-scope description into Lean: when each element of the description properties, we test their difference in Success with a paired maps one-to-one onto a single definition in the Lean model—as McNemar test [12], both overall and per family. it does for HOE and S UBSUMP—there is little room for a c) Results: Across the four property families, T EMPLATE plausible-looking but incorrect encoding. UDF, which must produces 136 synthesis successes against N OT EMP’s 90 encode an arbitrary lambda expression, and AGG D ECOMP, (Table II), a per-family improvement of 1.0–2.6× (averaging which composes more complex multi-input computations, 1.6×). T EMPLATE is also cheaper per property attempted in leave much more room. The template removes the resulting every family, with N OT EMP spending 14–32% more (averaging hallucination for UDF but leaves it for AGG D ECOMP; we 23%). Hallucinations appear in only two families: T EMPLATE examine each in turn. hallucinates only on AGG D ECOMP, where its rate stays below For UDF, N OT EMP frequently hallucinates through carrier N OT EMP’s (54% vs. 67% of compiling proofs), while N OT EMP collapse: it reduces a multi-column operation to a single input also hallucinates on UDF; on the remaining two families neither or a constant so that the two sides coincide trivially—modelling configuration hallucinates at all. Figure 5 shows the property- 2-argument null-safe equality as x == x, a three-column level overlap: 55 properties are successfully synthesized by array_join as "x|x|x", or a four-column except-cardinality T EMPLATE alone, 81 by both configurations, and just 9 by as size(except([x,x],[x,x])) = 0. 7 of N OT EMP’s 28 N OT EMP alone. By the paired McNemar test, this overall compiling UDF proofs (25%) collapse this way. In contrast, advantage is significant (p < 10−6 ). T EMPLATE therefore T EMPLATE produces none: all 54 of its compiling proofs are covers all but 9 of the 145 properties that either configuration synthesis successes. The template hands the agent the proof’s can synthesize successfully. high-level structure outright, so its effort goes to a narrower d) Per property family analysis: These numbers point to sub-problem instead of the low-level tactic search that N OT EMP where the LLM’s effort goes. The template’s benefit is large for often falls into, and trivial shortcuts like carrier collapse stop HOE and UDF—synthesis successes rise 1.6× and 2.6×, and being a viable strategy. N OT EMP pays about a third more per property—but small for Unlike UDF, for AGG D ECOMP both configurations halluAGG D ECOMP and S UBSUMP, where the two configurations cinate, and in the same two forms: a tautological relation land within a single synthesis success of each other and only (P ∨ ¬P , a full trichotomy, x = x, a vacuous implication)

TABLE III: PBT synthesis outcomes per property family, one attempt per property. A test is Faithful if it executes and matches its natural-language description; otherwise it fails as Non-exec. (does not execute) or NL-mis. (executes but diverges from it). Property Family (# props)

Config.

Faithful

Cost/prop (USD)

HOE (100)

T EMPLATE G EN O NLY N OT EMP

3 10 5

0 3 3

97 (97.0%) 87 (87.0%) 92 (92.0%)

$0.031 $0.122 $0.172

UDF (100)

T EMPLATE G EN O NLY N OT EMP

2 13 2

0 15 16

98 (98.0%) 72 (72.0%) 82 (82.0%)

$0.034 $0.158 $0.194

T EMPLATE AGG D ECOMP (100) G EN O NLY N OT EMP

2 16 0

0 98 (98.0%) 1 83 (83.0%) 0 100 (100.0%)

$0.060 $0.124 $0.152

T EMPLATE G EN O NLY N OT EMP

5 9 0

1 3 3

$0.151 $0.167 $0.195

S UBSUMP (100)

Non-exec. NL-mis.

94 (94.0%) 88 (88.0%) 97 (97.0%)

and a degenerate aggregator (a constant in place of the datadependent statistic, a different statistic, or the wrong null/defined gate). 7 of T EMPLATE’s 13 compiling proofs and 10 of N OT EMP’s 15 hallucinate—T EMPLATE’s almost all tautological relations, N OT EMP’s spread across tautological relations and, more often, constant aggregators. Here the template does not separate the two configurations: its DecompTriple hands the relation and the aggregator to the agent to define—which UDF’s template does not—so even with the template in place the agent retains many angles from which to cheat. N OT EMP hallucinates somewhat more (67% vs. 54% of compiles), but neither is clean. Answer to RQ2. The property template sharply reduces hallucination: it eliminates N OT EMP’s UDF hallucinations (7 proofs to none) and cuts AGG D ECOMP’s (10 to 7), lowering the total across the families from 17 (N OT EMP) to 7 (T EMPLATE)—a 2.4× reduction.

holes; G EN O NLY supplies only the generators; N OT EMP neither. A PBT is faithful only if it both executes and matches the property’s natural-language description; otherwise it fails as non-executable or NL-misaligned (executes but diverges). c) RQ3 Faithfulness Results: T EMPLATE is the most faithful configuration—387/400 (96.8%), against N OT EMP’s 371/400 (92.8%) and G EN O NLY’s 330/400 (82.5%) (Table III). NL misalignments drive the gap: T EMPLATE produces just 1, versus 22 for N OT EMP and 22 for G EN O NLY. N OT EMP’s 22 cluster where a property’s semantics are subtle—19 boundarysemantics errors (16 in UDF, where the UDF and built-in diverge on null, NaN, or encoding; 3 in HOE, on null handling across the two sides) and 3 in S UBSUMP that substitute row count for multiset containment. By fixing the harness structure, the template closes this room for misencoding. Generator access alone does not help: G EN O NLY (82.5%) falls below even N OT EMP (92.8%), as assembling a complete PBT from building blocks yields far more non-executable failures (48 vs. 7). The template does not eliminate such nonexecutable failures either—they stem from hallucinated Python and PySpark API calls, a code-level issue independent of the PBT structure. d) RQ3 Token Cost Results: T EMPLATE also cuts cost, most where it constrains synthesis most tightly: per attempt it is 5.7× cheaper on UDF and 5.5× on HOE ($0.03 vs. $0.17–$0.19), tapering to 2.5× on AGG D ECOMP and 1.3× on S UBSUMP. Most of the saving is in reasoning tokens—a 2.5× drop, from 4,500 to 1,800. G EN O NLY, still assembling the full harness, achieves only a 1.1–1.5× cost reduction. Answer to RQ3. T EMPLATE increases faithful PBT synthesis from 92.8% to 96.8%, reducing NL misalignments from 22 to 1 and cutting cost by up to 5.7× for UDF and HOE.

e) Experimental Setup (RQ4): The two unrestricted baselines are LLM-PBT and C OMET F UZZ [14]. LLM-PBT is the unconstrained LLM generation of our pilot study B. PBT Synthesis (Section II-C): GPT-5.5 synthesizes 100 PySpark PBTs with no a) Research Questions: template or pre-specified family (full prompt in supplemental). RQ3. On the same concrete property, does the property template C OMET F UZZ is a Spark fuzzer; it asserts no properties, so we improve PBT synthesis accuracy and reduce LLM cost, compare it on code coverage alone. We assess three coverage compared with synthesizing the test without it? dimensions: (i) API coverage of PySpark expression operations RQ4. Does confining synthesis to template families sacrifice and DataFrame operators (vs. LLM-PBT); (ii) code coverage the behavioral coverage against unrestricted DISC test- of Spark’s catalyst and execution modules (vs. both); and ing—fuzzing and unguided, LLM-generated PBT? (iii) overlap in the kinds of properties tested (vs. LLM-PBT). As in §IV-A, RQ3 isolates the template’s effect—the same f) API coverage: All four template families exercise more property synthesized with and without it. RQ4 instead probes PySpark expression operations than LLM-PBT’s 56, ranging a potential cost of the approach: comparing template-guided from 85 to 164 (Figure 6); UDF leads at 164, as each property synthesis against two unrestricted baselines, it asks whether pairs a UDF with a specific built-in. For DataFrame operators, confining generation to a few predefined families sacrifices the S UBSUMP reaches 52 against LLM-PBT’s 36, while the other behavioral coverage they attain. three are comparable (34–36). Coverage grows with the number b) Experimental Setup (RQ3): For RQ3, we evaluate of executions per property (k) because each template execution all 400 properties across three configurations, all single- samples a fresh workload, whereas LLM-PBT’s fixed workload round with GPT-5.5 (medium reasoning) (Table III). A PBT does not vary with k. template supplies two reusable parts—workload generators g) Code coverage: On Spark’s catalyst and and a harness that wires them around the property (§III-B). execution modules (Figure 7), template-guided synthesis T EMPLATE supplies both, leaving the LLM only the property exceeds the C OMET F UZZ fuzzer in every family, on both

TABLE IV: Cross-validation of T EMPLATE proofs and T EM PLATE PBTs across 400 properties, with each PBT run for 20 test executions.

Fig. 6: API coverage over the first 100 properties per family as a function of executions per property (k): unique expression operations (left) and DataFrame operators (right). Templateguided curves grow with k; LLM-PBT (dashed) is flat.

Faithful PBT No faithful PBT Passing Failing Successful proof 130 1 5 No successful proof 251 5 8 Total 381 6 13

Total 136 264 400

We cross-validate the proof and PBT results for all 400 properties under the T EMPLATE setting, using the artifact classifications from RQ2 and RQ3. Each PBT is executed 20 times. A faithful PBT is failing if at least one execution raises an assertion error and passing otherwise. Table IV summarizes the resulting proof and PBT outcomes. For 130/400 properties, both tracks provide supporting evidence: Lean establishes the intended property over the formal model, while a faithful PBT executes on PySpark without finding a counterexample. These cases provide the strongest evidence available from the two Fig. 7: Line, branch, and method code coverage of Spark’s tracks. catalyst and execution modules as a function of cua) Counterexamples are diagnostic: A faithful PBT finds mulative test executions. Template families and LLM-PBT: a counterexample for 6 properties, refuting each on the 100 PBTs × 5 executions; C OMET F UZZ: 500 fuzz iterations. real implementation. For one, a Lean proof also succeeds; the disagreement, invisible to either track alone, exposes line coverage (12.5–14.4% vs. 11.9%) and method coverage a model–runtime gap. Lean proves size(array_except (9.0–10.5% vs. 7.5%). Against LLM-PBT (15.2% line, 10.3% (filter(arr, x → x < 0), arr)) = 0 over the total method) the families split: UDF and S UBSUMP come within a array type List, which has no null inhabitant, while PySpark percentage point on both and edge ahead on branch coverage admits nullable array columns for which the equality fails. This (2–4% higher), whereas HOE and AGG D ECOMP trail by case reveals a gap in the model’s treatment of nullable arrays. b) PBT localizes where proofs must grow: For 251 2.3–2.7 points on line and 1.1–1.3 on method. These gains properties, a faithful PBT executes without an assertion error, come from the generators, which vary input schemas and but the proof track produces no successful proof. Of these, surrounding operations to reach broad engine paths within 107 fall outside the current model. Extending the array model each family. Unlike a fuzzer, these tests also assert the would bring the most into scope—58 properties, led by count property they target. aggregates (15), arrays_zip (13), and array reductions (12)— h) Property-space overlap: Of the 100 LLM-PBT properties, 32 broadly align with our families (12 HOE, 7 followed by DataFrame extensions such as join, set, and AggDecomp, 13 Subsump, 0 UDF); the remaining 68 are window semantics. Another 138 exhaust the proof budget, single-operation expected-output (55), operator-algebra (5), motivating stronger search such as helper-lemma synthesis [15]. round-trip (6), and execution-invariance (2) properties (full The last 6 compile but prove nothing of interest. breakdown in supplemental). This reveals a breadth–depth Answer to RQ5. For 130 of 400 properties (32.5%), a tradeoff: direct synthesis spans more property forms, while Lean proof and a faithful passing PBT agree—the strongest templates instantiate reusable families systematically. The combined evidence. Disagreements are diagnostic: a councontrast is clearest for UDFs: none of the 100 LLM-PBT terexample to a proven property exposes a model–runtime tests uses a Spark UDF, whereas the UDF template yields 98 gap and its fix, and a proof-less passing test localizes where faithful UDF-to-builtin PBTs. formalization and proof search pay off most. Answer to RQ4. Template-guided synthesis exceeds C OMETF UZZ on every coverage metric and approaches LLM-PBT (up to 4% higher on branch), while exclusively covering UDF-to-builtin correspondence—a class unguided synthesis never generates. C. Cross-Validation: PBT Against Formal Proofs RQ5. What evidence and diagnostic value arise from validating the same property by both formal proof and PBT?

V. T HREATS TO VALIDITY Measurement. Assessing candidate-property correctness, proof hallucinations, and PBT faithfulness requires manual semantic judgment and may introduce reviewer error. We release all proofs and tests for independent re-examination. Our coverage metrics measure behavioral breadth rather than semantic adequacy or fault-detection effectiveness. Experimental design. Both synthesis tracks are stochastic and use one run per property and configuration. We compare

configurations over the same property sets under fixed model settings, budgets, and environments, and aggregate results across hundreds of properties, reducing sensitivity to isolated generations. Results may still vary across runs and with different template designs, generators, lemmas, or formal models. Generalizability. We evaluate four recurring property families in PySpark using one model configuration. The families represent several forms of equivalence and other relational properties in data-intensive systems, but effect sizes may differ for other families, systems, formalizations, or models.

proaches synthesize programs or prove mathematical theorems, a single template drives both a Lean proof and an executable PySpark test, validating the correctness of real software systems by proof and execution alike. Second, these methods attach no precondition to their holes, so an instantiation is a conjecture checked after the fact—filtered by counterexample search and proved one at a time—whereas our template carries the family’s local law (AGG D ECOMP’s decomposition law, UDF’s pointwise equivalence) as a precondition: proved once, any satisfying instantiation lifts to a correct property over an arbitrary pipeline and workload, so the agent discharges only the local law and the instance is correct by construction. VI. R ELATED W ORK c) Testing and verifying data-intensive and querya) Property-based testing and property specification: processing systems: A body of work targets the correctness Goldstein et al. [3] empirically study developers’ PBT ex- of data-processing systems themselves. On the verification perience and find property specification a central obstacle: side, automated SQL equivalence provers decide whether two developers struggle both to identify suitable properties and to relational queries are equivalent and thereby verify rewrite turn informal intent into executable ones. Lahiri [6] frames rules, as in Cosette [25] and SQLSolver [26]; WeTune [27] this as a grand challenge for the age of AI agents: formal- goes further, automatically discovering new rewrite rules izing informal intent into checkable specifications is what and verifying them with such a prover. On the testing side, makes agent-generated code trustworthy rather than merely SQLancer detects logic and optimization bugs in database abundant. Hughes et al. [16] give a taxonomy of reusable engines through constructed oracles such as query partitioning property patterns for pure functions—invariants, postconditions, and a non-optimizing reference engine [28], [29]. Closest to metamorphic and inductive properties, and model-based speci- our setting, big-data testers generate Spark inputs by symbolic fications. Segura et al. [17] represent metamorphic relations execution of dataflow operators and UDFs [30] or frameworkas templates that make explicit the source/follow-up inputs abstraction fuzzing [31]. Each fixes both target and technique— and the expected output relation, but use templates primarily one query pair, one engine, or one program at a time. Our as a documentation mechanism. Earlier, Dwyer et al. [18] work instead treats the optimization-relevant equivalences of catalog recurring specification patterns for temporal properties data-intensive computing as recurring property families, and in finite-state verification, mapping common requirements onto validates each instance at scale along both a proof track and a temporal logics for model checking. Most closely related, PBT track over real PySpark. agentic tools drive LLMs to infer and run property-based VII. C ONCLUSION tests: Agentic PBT [5] finds real bugs across the Python ecosystem, and AWS’s Kiro [11] turns requirements into PBT We set out to make the validation of a software system’s for “spec correctness” in an IDE, while stopping short of formal many correctness properties tractable at scale. Our central idea verification. Our work is complementary: rather than inferring is to capture each recurring property family once as a property or generating tests one module at a time, we organize recurring template. Each candidate property is then validated along two property families as templates and validate each instance at complementary tracks: a machine-checked Lean 4 proof and scale along both a proof track and a PBT track. an executable property-based test against the real system. In both tracks, the template fixes the shared structure and leaves b) Structure-guided synthesis and theorem proving: A recurring idea in synthesis and theorem proving is to only property-specific holes to be filled. Instantiated for datasupply partial structure that guides search toward a target intensive computing on Apache Spark, property templates fixed in advance. S KETCH [19] fills the holes of a partial increase machine-checked synthesis successes by up to 2.6× program against a specification, and DSP [13] maps an informal and reduce proof hallucinations by 59%. They also reduce proof into a formal sketch that guides an automated prover intent misalignments in synthesized tests from 22 to 1, while over easier subproblems. Closest to our setting, SITA [20] lowering synthesis cost by up to 5.7×. abstracts existing Lean formalizations into reusable structures This experience also surfaces a caution as agentic theorem that an LLM instantiates for concrete theorems—much as our proving attracts growing attention. A proof accepted by Lean templates parameterize a proof’s shared structure. A related line establishes the encoded theorem under its stated definitions instead supplies the auxiliary facts a proof needs: synthesizing and assumptions, but the encoded theorem may not faithfully the helper or implication lemmas witnessed during a stuck express the intended property. An agent may misstate the proof [21], [22], or discovering new lemmas by instantiating property, introduce vacuous hypotheses, or rely on additional user-provided schemes (IsaScheme [23]) or LLM-generated axioms that weaken the intended guarantee. Templates reduce lemma templates (Lemmanaid [24]), filtering false conjectures such failures by fixing a family’s statement structure, but by counterexample. Our property templates share this structure- confirming that a machine-checked proof reflects genuine intent guided view but differ in two ways. First, whereas these ap- still requires human inspection. Detecting this formalization

gaming [32] automatically—auditing definitions for faithfulness and proofs for unsound dependencies—is an important open problem for trustworthy AI-assisted verification. DATA AVAILABILITY Our code, models, and data are available at https:// anonymous.4open.science/r/AgentLeanDiscprop-1597/.

R EFERENCES [1] L. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer, “The Lean Theorem Prover (System Description),” in Automated Deduction - CADE-25, A. P. Felty and A. Middeldorp, Eds. Cham: Springer International Publishing, 2015, pp. 378–388. [2] K. Claessen and J. Hughes, “QuickCheck: A lightweight tool for random testing of Haskell programs,” in Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP ’00). ACM, 2000, pp. 268–279. [3] H. Goldstein, J. W. Cutler, D. Dickstein, B. C. Pierce, and A. Head, “Property-Based Testing in Practice,” in Proceedings of the IEEE/ACM 46th International Conference on Software Engineering, ser. ICSE ’24. New York, NY, USA: Association for Computing Machinery, Apr. 2024, pp. 1–13. [4] Z. Paraskevopoulou, C. HriŢcu, M. Dénès, L. Lampropoulos, and B. C. Pierce, “Foundational property-based testing,” in Interactive Theorem Proving, C. Urban and X. Zhang, Eds. Cham: Springer International Publishing, 2015, pp. 325–343. [5] M. Maaz, L. DeVoe, Z. Hatfield-Dodds, and N. Carlini, “Agentic PropertyBased Testing: Finding Bugs Across the Python Ecosystem,” 2025. [6] S. K. Lahiri, “Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents,” 2026. [7] M. Zaharia, R. S. Xin, P. Wendell, T. Das, M. Armbrust, A. Dave, X. Meng, J. Rosen, S. Venkataraman, M. J. Franklin, A. Ghodsi, J. Gonzalez, S. Shenker, and I. Stoica, “Apache Spark: A unified engine for big data processing,” Communications of the ACM, vol. 59, no. 11, pp. 56–65, 2016. [8] X. Leroy, “Formal verification of a realistic compiler,” Communications of the ACM, vol. 52, no. 7, pp. 107–115, 2009. [9] G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood, “seL4: Formal Verification of an OS Kernel,” in Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles (SOSP). ACM, 2009, pp. 207–220. [10] J. Hughes, “Experiences with QuickCheck: Testing the Hard Stuff and Staying Sane,” in A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (LNCS 9600). Springer, 2016, pp. 169–186. [11] Kiro, “Correctness with Property-based tests,” https://kiro.dev/docs/specs/correctness/, Nov. 2025. [12] Q. McNemar, “Note on the sampling error of the difference between correlated proportions or percentages,” Psychometrika, vol. 12, no. 2, pp. 153–157, Jun. 1947. [13] A. Q. Jiang, S. Welleck, J. P. Zhou, W. Li, J. Liu, M. Jamnik, T. Lacroix, Y. Wu, and G. Lample, “Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs,” in The Eleventh International Conference on Learning Representations (ICLR 2023), 2023. [14] Apache DataFusion Comet Developers, “Apache DataFusion Comet: Fuzz Testing,” https://github.com/apache/datafusion-comet/tree/ 03e833b955d369f994d9652026ca3c1eb641acac/fuzz-testing. [15] A. Sivaraman, A. Sanchez-Stern, B. Chen, S. Lerner, and T. Millstein, “Data-driven lemma synthesis for interactive proofs,” Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA2, pp. 505–531, 2022. [16] J. Hughes, “How to Specify It! A Guide to Writing Properties of Pure Functions,” in Trends in Functional Programming: 20th International Symposium, TFP 2019, Vancouver, BC, Canada, June 12–14, 2019, Revised Selected Papers. Berlin, Heidelberg: Springer-Verlag, Jun. 2019, pp. 58–83. [17] S. Segura, A. Durán, J. Troya, and A. Ruiz Cortés, “A Template-Based Approach to Describing Metamorphic Relations,” in 2017 IEEE/ACM 2nd International Workshop on Metamorphic Testing (MET). IEEE, 2017, pp. 3–9. [18] M. B. Dwyer, G. S. Avrunin, and J. C. Corbett, “Patterns in Property Specifications for Finite-State Verification,” in Proceedings of the 21st International Conference on Software Engineering (ICSE). New York, NY, USA: ACM, 1999, pp. 411–420. [19] A. Solar-Lezama, L. Tancau, R. Bodı́k, S. A. Seshia, and V. A. Saraswat, “Combinatorial sketching for finite programs,” in Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS XII). ACM, 2006, pp. 404–415.

[20] C. Li, W. Ma, Z. Wang, and Z. Wen, “SITA: A Framework for Structureto-Instance Theorem Autoformalization,” in Proceedings of the AAAI Conference on Artificial Intelligence (AAAI 2026), vol. 40. AAAI Press, 2026, pp. 19 224–19 232. [21] W. Yang, G. Fedyukovich, and A. Gupta, “Lemma Synthesis for Automating Induction over Algebraic Data Types,” in Principles and Practice of Constraint Programming (CP 2019), ser. Lecture Notes in Computer Science. Springer, 2019, pp. 600–617. [22] A. Brendel, A. Sivaraman, and T. Millstein, “Synthesizing implication lemmas for interactive theorem proving,” Proceedings of the ACM on Programming Languages, vol. 9, no. OOPSLA2, pp. 2254–2278, 2025. [23] O. Montaño-Rivas, R. L. McCasland, L. Dixon, and A. Bundy, “Schemebased theorem discovery and concept invention,” Expert Systems with Applications, vol. 39, no. 2, pp. 1637–1646, 2012. [24] Y. Alhessi, S. H. Einarsdóttir, G. Granberry, E. First, M. Johansson, S. Lerner, and N. Smallbone, “Lemmanaid: Neuro-symbolic lemma conjecturing,” arXiv preprint arXiv:2504.04942, 2025. [25] S. Chu, C. Wang, K. Weitz, and A. Cheung, “Cosette: An Automated Prover for SQL,” in 8th Biennial Conference on Innovative Data Systems Research (CIDR), 2017. [26] H. Ding, Z. Wang, Y. Yang, D. Zhang, Z. Xu, H. Chen, R. Piskac, and J. Li, “Proving Query Equivalence Using Linear Integer Arithmetic,” Proceedings of the ACM on Management of Data, vol. 1, no. 4, pp. 1–26, 2023. [27] Z. Wang, Z. Zhou, Y. Yang, H. Ding, G. Hu, D. Ding, C. Tang, H. Chen, and J. Li, “WeTune: Automatic Discovery and Verification of Query Rewrite Rules,” in Proceedings of the 2022 International Conference on Management of Data. New York, NY, USA: ACM, 2022, pp. 94–107. [28] M. Rigger and Z. Su, “Finding Bugs in Database Systems via Query Partitioning,” Proceedings of the ACM on Programming Languages, vol. 4, no. OOPSLA, pp. 1–30, 2020. [29] ——, “Detecting Optimization Bugs in Database Engines via NonOptimizing Reference Engine Construction,” in Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. New York, NY, USA: ACM, 2020, pp. 1140–1152. [30] M. A. Gulzar, S. Mardani, M. Musuvathi, and M. Kim, “White-Box Testing of Big Data Analytics with Complex User-Defined Functions,” in Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. New York, NY, USA: ACM, 2019, pp. 290–301. [31] Q. Zhang, J. Wang, M. A. Gulzar, R. Padhye, and M. Kim, “BigFuzz: Efficient Fuzz Testing for Data Analytics Using Framework Abstraction,” in Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering. New York, NY, USA: ACM, 2020, pp. 722–733. [32] K. Kim, A. Poiroux, and A. Bosselut, “Do LLMs Game Formalization? Evaluating Faithfulness in Logical Reasoning,” 2026.