arXiv cs.CL· Jiale Lao, Immanuel Trummer·· 11 小时前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。
正文 · AI 翻译
摘要：50 多年来，数据库社区开发了多种成功的引擎，以回答两个基本问题：数据库系统如何运行得更快，以及我们如何确保其正确性？这些引擎的经验表明，性能取决于硬件和工作负载。随着两者随时间变化，我们反复重新设计和重建数据库系统，这是一个耗时且昂贵的过程。正确性仍然是另一个长期存在的挑战：尽管经过多年的开发和测试，最近的研究仍不断在成熟的数据库引擎中发现错误答案缺陷。为解决这些问题，我们提出 GenDB-V，一个使 AI 智能体能够合成针对硬件和工作负载进行性能特化、并经过形式化验证以确保正确性的数据库引擎的系统。GenDB-V 支持 SQL 模板的特化实现，以及接受受支持 SQL 子集内任意查询的通用引擎。首先，我们开发 SQLSpec 以形式化 SQL 语义，并确定性地构造固定的、与实现无关的合成目标。其次，我们通过存储—执行协同优化、性能优先探索，以及将底层执行桥接到 SQLSpec 语义的三层模块化证明，实现快速代码与形式化证明的联合合成。第三，我们在隔离流水线中针对固定合成目标验证合成代码和证明，证明 SQL 正确性和程序安全性。我们在 TPC-H 和 SEC-EDGAR 上评估 GenDB-V。对于经过验证的模板实现，GenDB-V 相比 DuckDB 和 Umbra 实现 22.0-61.3 倍的几何平均加速。对于经过验证的通用引擎，GenDB-V 在 TPC-H 上也实现 1.27-3.4 倍的加速。GenDB-V 还比基于测试的 LLM 合成方法取得更好的性能，而我们的审计和测试在该方法的实现中暴露了 28 个模板中 16 个的 incorrect answers。
| 学科： | 数据库（cs.DB）；人工智能（cs.AI）；计算与语言（cs.CL）；机器学习（cs.LG） |
| 引用为： | arXiv:2611.02779 [cs.DB] |
| （或 arXiv:2611.02779v1 [cs.DB] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2611.02779 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Jiale Lao [查看电子邮件]
[v1]
2026 年 11 月 2 日星期一 08:56:44 UTC（155 KB）
来源：arXiv cs.CL · arxiv.org