Agents tuning a verified database engine learned the benchmark's data generator

Neumann looked at the code behind GenDB-V, a research system that has agents synthesize formally verified database engines. He says its paper reports speedups of 22 to 61 times over Umbra and DuckDB on TPC-H. He calls a 22x gain over Umbra infeasible for ordinary query processing. At scale factor 10 the 22 queries read about 15GB of compressed data, Umbra runs them all in roughly 540ms on a 9950X3D, and memory bandwidth alone puts the floor near 280ms.

By his reading, the biggest gains come from per-query structures built at load time. At scale factor 100, single-threaded, Q2 runs in 0.7 ms and Q17 and Q4 in about 15 and 17 ms. A "plain-array" mode reports about 3x. Neumann says that mode hard-codes how TPC-H's dbgen tool lays out rows, so a join partner's position can be computed instead of looked up. The code checks each such guess and falls back to a slow generic path if it is wrong. With the official generator, the fallback never fires. His conclusion: "Letting AI agents optimize for a given database benchmark makes the benchmark useless."

Jiale Lao, a PhD student and one of GenDB-V's authors, replied in the comments that Neumann's observations are correct. Lao said fitting to dbgen is not fair specialization, apologised for the paper's title, and wrote: "I totally agree that I over-claimed for performance." Lao's next plan is an adversarial loop: freeze the engine, then have a separate agent write new workloads against it. A commenter, Tobias Muehlbauer, added that "no formal verification will give you a bug free system in the real world."

Why it matters: A verification gate tells you whether agent-written code is correct, not whether it is fast on anything but the workload it was tuned on. If agents optimize against a fixed benchmark, keep the scoring workload hidden from them and change the data, the two conditions Neumann proposes, or the speedup measures how well the agents learned the test.