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

Seongmin Lee, Yaoxuan Wu, Miryung Kim. 2026.

What this paper does with SQLancer

One citation, describing SQLancer as detecting logic and optimization bugs in database engines through constructed oracles such as query partitioning -- the testing-side precedent for the paper's own property-based track. A study of recurring correctness properties in Apache Spark, expressed as parameterised property templates. The authors use them in a dual-track framework that both proves properties in the Lean 4 theorem prover and instantiates them as executable PySpark property-based tests, reporting that templates raise agentic proof success by up to 2.6x and cut proof hallucinations by 59%. Written by claude-opus-5 from the 1 place this paper refers to SQLancer. The quotations below are the paper's own words, stored verbatim when the text was extracted.

How it was classified

uses infrastructure — no

SQLancer is cited, not used; nothing in the mentions describes reusing its code.

extends technique — no

No technique is extended; the citation is background.

compares with — no

No empirical comparison against SQLancer is reported in the mentions.

describes as state of the art — no

The citation does not characterise SQLancer as the state of the art.

SQLancer publications it cites (2)

Bibliography entries that resolved to a SQLancer publication, or to a paper by one of the project's authors. A sentence citing one of these numbers is a reference to SQLancer even when it never writes the name.

#	Entry	Matched as
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.	sqlancer publication · TLP
29	——, “Detecting Optimization Bugs in Database Engines via NonOptimizing Reference Engine Construction,” inProceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Found...	sqlancer publication · NOREC

Every place it refers to SQLancer (1)

1 sentence, each stored verbatim from the extracted text with where it was found and how. “Citation marker” means the sentence names no tool at all and was reached through a reference number that resolved to a SQLancer publication.

Id	Sentence	Found by	Where
M1	On the testing side, SQLancer detects logic and optimization bugs in database engines through constructed oracles such as query partitioning and a non-optimizing reference engine [ 28], [29].	name background	C Cross-Validation: PBT Against Formal Proofs page 10

This page is rendered from _data/papers/paper_arxiv_2607_09072.json, extracted from arxiv. 12 pages, 32 references parsed.