arXiv cs.CL· Jiale Lao, Immanuel Trummer·· 12 小时前AI 评分48
GenDB-V：让 AI 智能体生成并形式化验证数据库系统
Stop Handcrafting Your Engine! GenDB-V: Towards AI-Generated and Formally Verified Database Systems
AI 导读
GenDB-V 让 AI 智能体合成针对硬件与负载特化的数据库引擎，并对其做形式化验证以保证正确性。在 TPC-H 和 SEC-EDGAR 上，经形式化验证的模板实现相对 DuckDB 与 Umbra 取得 22.0-61.3x 几何平均加速，经形式化验证的通用引擎在 TPC-H 上加速 1.27-3.4x。
正文 · 原文
Abstract:For over 50 years, the database community has developed a wide range of successful engines to answer two fundamental questions: how can database systems run faster, and how can we ensure their correctness? Experience with these engines shows that performance depends on hardware and workloads. As both change over time, we repeatedly redesign and rebuild database systems, a time-consuming and expensive process. Correctness remains another long-standing challenge: recent studies continue to uncover wrong-answer bugs even in mature database engines, despite years of development and testing. To address these, we present GenDB-V, a system that enables AI agents to synthesize database engines specialized to hardware and workloads for performance, and formally verified for correctness. GenDB-V supports specialized implementations of SQL templates and general-purpose engines that accept any query within a supported SQL subset. First, we develop SQLSpec to formalize SQL semantics and deterministically construct fixed, implementation-agnostic synthesis targets. Second, we enable joint synthesis of fast code and formal proofs through storage--execution co-optimization, performance-first exploration, and three-layer modular proofs that bridge low-level execution to SQLSpec semantics. Third, we verify the synthesized code and proofs against the fixed synthesis targets in an isolated pipeline, proving SQL correctness and program safety. We evaluate GenDB-V on TPC-H and SEC-EDGAR. For verified template implementations, GenDB-V achieves geometric-mean speedups of 22.0-61.3x over DuckDB and Umbra. For a verified general-purpose engine, GenDB-V also achieves speedups of 1.27-3.4x on TPC-H. GenDB-V also achieves better performance than a testing-based LLM synthesis method, while our audit and tests expose incorrect answers in that method's implementations for 16 of 28 templates.
| Subjects: | Databases (cs.DB); Artificial Intelligence (cs.AI); Computation and Language (cs.CL); Machine Learning (cs.LG) |
| Cite as: | arXiv:2611.02779 [cs.DB] |
| (or arXiv:2611.02779v1 [cs.DB] for this version) | |
| https://doi.org/10.48550/arXiv.2611.02779 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Jiale Lao [view email]
[v1]
Mon, 2 Nov 2026 08:56:44 UTC (155 KB)
来源：arXiv cs.CL · arxiv.org