Whiel pairs AI-generated ideas with formal checks for database programs

A language model can propose a faster database query or a procedure for updating stored query results. Checking a few example databases may expose mistakes, but it cannot establish that the proposal works across every permitted input. Whiel addresses that verification problem by letting AI suggest mathematical ingredients while separate tools check the reasoning.

The manuscript, by Jesse Comer, Fangzhu Shen, Shuo Zhang, Mayur Naik, Sudeepa Roy and Val Tannen, presents a common verification framework for several difficult database problems. These include recursive query equivalence, query containment, view-based rewriting and incremental view maintenance. Its arXiv version was submitted on November 3, 2026.

One language for different correctness questions

Whiel represents a program’s state as a database instance. Commands change relations using relational algebra operations, with loops and conditionals controlling execution. This imperative structure can describe both queries and evaluation algorithms that are not expressible in the original query language.

A verification task specifies an initial condition, a program and a required final condition. For example, it might ask whether two methods for computing reachable pairs of graph nodes return the same relation.

The precise guarantee concerns terminating executions: whenever the initial condition holds and the program finishes, its result must satisfy the final condition. A validity proof does not, by itself, establish that the program always terminates. Conversely, one permitted input that produces a terminating run with an incorrect result is enough to disprove the specification.

AI proposes; symbolic tools check

Whiel first transforms the task into a form containing a single loop, using a transformation whose preservation of validity is proved in Lean. The central search problem is then to find a loop invariant: an assertion that supports reasoning throughout execution and establishes the required result at exit.

Its language-model proposer can submit candidate assertions or a concrete counterexample. A symbolic verifier checks proposals using the Vampire theorem prover and Whiel’s LeveledHoudini algorithm. Feedback supports further proposals, while accepted assertions accumulate into an inductive core.

An important feature is the use of “prophecy variables,” which represent the eventual values of relations. These support arguments connecting intermediate computations to final results. Leveled invariants organize that reasoning into stages, allowing established properties of terminal values to support further claims while keeping the verification conditions in first-order logic.

The process is not guaranteed to settle every task. The paper establishes that Whiel’s validity problem is coRE-complete. Vampire also reasons over arbitrary structures, whereas Whiel’s database states are finite; proving validity over arbitrary structures is sound for finite ones, but cannot establish every finitely valid entailment. Resource exhaustion can leave a task unresolved.

What the benchmark shows

The authors constructed 86 tasks: 69 valid specifications and 17 invalid ones. Sources include classical database problems, programs translated from real systems, and language-model-generated programs. Every task has a Lean-certified reference answer, hidden from the proposer during experiments.

Using GPT-5.5, default Whiel accepted answers for 73 tasks. A single-proposal baseline solved 46, while a baseline that asked the same model to construct Lean proofs directly solved 20. Average reported token costs across all tasks were $0.49 for Whiel and $2.08 for direct proof generation.

These comparisons have important boundaries. Whiel’s 600-second search budget included model interaction and verifier checks, but excluded certification. The direct Lean baseline had no time limit and counted success only when Lean accepted its proof.

Curated reasoning tutorials increased GPT-5.5 coverage to 77 tasks. Adding both tutorials and inspection tools did not improve on tutorials alone. Passing unresolved tasks successively to GPT-5.6 Sol and GPT-6 Astra brought cumulative coverage to 85 of 86 in each tested configuration—not 85 successes from one model alone.

Finding an answer is not certifying it

Whiel’s independent, LLM-free certifier reconstructs validity proofs in Lean or replays counterexamples in Lean’s kernel. Successfully certified results depend on the kernel and the fidelity of the formal definitions, rather than trust in the proposer or search machinery.

That final step remained a substantial bottleneck. Across four configurations, 293 of 340 verifier-accepted answers completed certification within the stated limits: 225 of 272 validity answers and all 68 invalidity answers. The remaining attempts encountered 41 timeouts and six memory-limit failures.

The evidence therefore supports a distinction: Whiel’s architecture helped discover checked answers on this curated suite, but search acceptance did not always yield a completed certificate. The authors identify broader benchmarking and lower certification time and memory requirements as future work.