圈内内参｜这期聊一篇11月2号挂上arXiv的论文，Jiale Lao和Immanuel Trummer写的《Stop Handcrafting Your Engine! GenDB-V: Towards AI-Generated and Formally Verified Database Systems》。结论先放一句：这篇论文最该被记下的不是它声称的22到61倍加速，是它顺手做的一次审计——28个SQL模板，基于测试的LLM合成方法有16个会返回错误答案。加速数字可以争、也值得吵，16/28这个数据点暂时看不出怎么被推翻。
论文要做的事其实很明确：不打算在“快”和“对”里选一个，AI合成加上形式化验证，两条线一起走。合成出来的代码针对特定硬件和工作负载做优化，同时给它做形式化验证。产出分两类，一类是面向特定SQL模板的专用实现，另一类是能接受受支持SQL子集内任意查询的通用引擎。两类产出的加速数字后面会摆出来，差距很说明问题。
SQLSpec组件是整篇论文的机制核心。论文说它用来形式化SQL语义，以确定性的方式构造出一个固定的合成目标，这个目标和具体实现无关。合成出来的代码不管长什么样，要对齐的是SQLSpec定义的那层语义，不是某个参考实现的输出。设计动机不复杂：如果合成目标绑定具体实现，AI生成的代码只需要模仿那个实现的输出。但模仿输出不等于语义正确——参考实现本身可能就有bug，模仿它的代码会把这个bug一起继承过去。SQLSpec把语义从实现里抽出来，合成目标就成了“符合这层形式化语义”，不是“和DuckDB输出一致”。这一步把“对”的定义从参考实现里拿出来，变成一个独立于任何引擎实现的东西。
合成流程分三条线：存储和执行协同优化，搜索策略偏性能优先，底层执行和SQLSpec语义之间用三层模块化证明衔接。合成完的代码和证明在隔离流水线里对着同一个合成目标做校验——这一步同时确认SQL语义正确性和程序安全性。注意这个设计：校验不是在开发环境顺手做的，是在隔离流水线里做，因为合成出来的代码不可信，证明本身也不可信，都得在受控环境里跑一遍。
加速数字部分我直接说。论文在TPC-H和SEC-EDGAR两个基准上做了评估。经过验证的模板实现，相对DuckDB和Umbra，几何平均加速在22.0到61.3倍这个区间——这是论文数据，未独立复核。注意这个区间对应的是特定SQL模板的专用实现，不是通用引擎。到了通用引擎这一档，加速变成1.27到3.4倍，还是在TPC-H上。两个数字之间的差距说明的不是意外，是设计取舍：专用实现只需要处理一组固定的查询形状，优化空间比通用引擎大得多。
至于22到61倍这个绝对值，我不太想展开。对标系统是DuckDB和Umbra，这俩的优化目标和工作负载假设跟GenDB-V不是一个路数，直接对比的公平性需要独立复现才能验证。SEC-EDGAR这个基准的切分和对照系统配置，公开版本里我还没来得及细看。（分析，非事实）在独立复现结果出来之前，22到61倍先当论文声称放着，不当既成事实。
下面这段才是我把这篇论文翻出来记的原因。论文干了一件事：拿一个基于测试的LLM合成方法做对照，审计它生成的实现。结果：28个模板里16个实现会给出错误答案。这意味着——基于测试的合成方法在超过一半的模板上蒙混过了测试，实际语义是错的。不是LLM生成的代码偶尔有个bug，是测试这个兜底机制在这个场景下系统性失效了。
原因不复杂。测试用例是人写的，覆盖不了所有语义边界。AI生成的代码可以专门针对测试用例做优化，测试过得很漂亮，实际查询跑出来是错的结果还不知道。这跟大模型刷榜的逻辑一模一样，只不过换成引擎代码之后，错的结果不是榜单排名，是用户拿到一个错误的查询结果。这个审计数据比任何论证都硬：不是抽象地说“测试覆盖不足”，是直接给了一个失败率超过一半的实测数字。
论文把这个审计结果摆出来，用意很清楚：光靠测试兜底不够，得把形式化验证放进合成流水线。这个论点形式化验证社区说了很多年，不算新。但此前缺的是这样一个具体的、可核验的对照——不是“测试有局限”的推演，是同一批查询模板下，测试方法系统性地漏掉了错误答案。16/28这个数字，在我看来是这篇论文最值钱的地方，比22倍、61倍值钱得多。
（观点）AI合成加形式化验证在工程上能不能走通，现在没法判断。能记下来的是：在2026年11月这个时间点，有一个实验室级的结果同时证明了两件事——AI合成的数据库引擎在特定形状的查询上确实可以做到非常快，以及不把正确性验证放进合成流水线，测试兜底兜不住。这两件事以前是分开讨论的，现在被放进了同一篇论文。
几个值得盯的信号，不下注，列出来一起看：一、论文代码后续有没有公开，有没有团队去做独立复现——这比任何分析都能验证加速数字的成色。二、那个16/28的审计结果，会不会有其他团队对不同的LLM合成方法做比对。如果其他方法的失败率也在同一量级，这个方向的问题就严重了。三、通用引擎路径的加速数字（1.27到3.4倍）能不能在独立复现中保持。保不住，这条路线图的工程价值要重新算。四、SQLSpec这个组件后续会不会被其他合成系统沿用——被沿用，说明“形式化语义作为合成目标”这个设计真的解决了别人的问题，不是因为这篇论文提了它它才被提。
这些信号都可核验，不用谁拍脑袋下注。本期到这，有更准确信源或复现结果的同学欢迎补充。