Whiel：面向关系程序验证的神经符号平台，输出经 Lean 认证

View PDF HTML (experimental)

Abstract:We present the Whiel (a contraction of Whi(le-R)el) system for Lean-certified reasoning about imperative relational programs. The system can encode containment and equivalence problems for Datalog, its extensions with negation, and the core fragment of graph query languages. It can also represent optimized or incremental evaluation algorithms that are not expressible in the original query language, as well as first-order specifications of integrity constraints, schema mappings, and views arising in data integration, exchange, and sharing. Whiel's program states are database instances, and its imperative structure enables compositional Hoare-style reasoning with first-order relational specifications, using prophecy variables and leveled invariants to support inductive arguments. Whiel supports neurosymbolic discovery of loop invariants whose verification conditions can be checked using the Vampire first-order theorem prover. Counterexamples are fed back into the neurosymbolic pipeline, while proposed solutions are translated into Lean proof certificates. To validate the Whiel system, we evaluate its performance on a curated benchmark suite. In summary, we envision the Whiel system as a tool for tackling mathematically demanding, typically undecidable problems involving complex query and constraint languages, with a high degree of trust in its output.

Subjects:	Databases (cs.DB); Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO)
Cite as:	arXiv:2611.05612 [cs.DB]
	(or arXiv:2611.05612v1 [cs.DB] for this version)
	https://doi.org/10.48550/arXiv.2611.05612 arXiv-issued DOI via DataCite (pending registration)

Submission history

From: Jesse Comer [view email]
[v1] Tue, 3 Nov 2026 20:56:53 UTC (172 KB)