论文提出可形式化验证的 AI 合成数据库引擎 GenDB-V。
资讯摘要
论文提出 GenDB-V，让 AI 智能体针对特定硬件与工作负载合成数据库引擎，并对其做形式化验证以保证正确性。系统先用 SQLSpec 形式化 SQL 语义并构造与实现无关的合成目标，再通过存储—执行协同优化、性能优先探索和三层模块化证明，联合合成快速代码与形式化证明，最后在隔离流水线中验证。作者报告在 TPC-H 与 SEC-EDGAR 上，经验证的模板实现相对 DuckDB 和 Umbra 取得 22.0–61.3 倍几何平均加速，通用引擎在 TPC-H 上加速 1.27–3.4 倍。
要点速读
- 论文提出 GenDB-V，用 AI 智能体合成面向硬件与工作负载的数据库引擎，并做形式化验证。
- SQLSpec 形式化 SQL 语义，三层模块化证明把底层执行与 SQL 语义衔接起来。
- 作者报告模板实现相对 DuckDB、Umbra 加速 22.0–61.3 倍，通用引擎在 TPC-H 上加速 1.27–3.4 倍。
中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/11/4 08:00:28（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。