← 研踪 PaperTrailarXiv:2610.20527 · v3
JetStream: Generating Verified Query Accelerators for Existing Database Systems
首次提交 2026-10-15 01:25
版本更新 2026-11-05 00:52
雷达观测 2026-11-05 12:13
摘要
Recent work has shown that LLMs can synthesize highly instance-optimized database systems for fixed workloads, but to date these systems only replace the DBMS's native storage and assume static data: users must migrate their data, often give up ad-hoc queries, lose acceleration once the data changes, and lack formal correctness guarantees. We present JetStream, which instead generates query-specific accelerators that extend an existing DBMS. Given a set of parameterized query templates, a staged agentic workflow synthesizes accelerators that run directly over the DBMS's native tables and may maintain custom auxiliary state, while the host DBMS remains responsible for storage, transactions, recovery, and all the other queries. A fixed, engine-neutral substrate keeps auxiliary state transactionally consistent under writes, while generated backend adapters handle engine-specific hooks. JetStream generates two kinds of accelerators: tested accelerators, which may use any optimization and are validated by differential testing, and verified accelerators, which trade some performance for a machine-checked proof that every answer satisfies a trusted specification derived from the SQL. On TPC-H at SF=20, JetStream achieves a $584\times$ geomean read speedup over DuckDB ($89\times$ verified) and retains $139\times$ ($46\times$ verified) under a continuous update stream of 10,000 modified rows per second.
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v3 · 2026-11-05 00:52 · 最新观测版本
JetStream: Generating Verified Query Accelerators for Existing Database Systems
Recent work has shown that LLMs can synthesize highly instance-optimized database systems for fixed workloads, but to date these systems only replace the DBMS's native storage and assume static data: users must migrate their data, often give up ad-hoc queries, lose acceleration once the data changes, and lack formal correctness guarantees. We present JetStream, which instead generates query-specific accelerators that extend an existing DBMS. Given a set of parameterized query templates, a staged agentic workflow synthesizes accelerators that run directly over the DBMS's native tables and may maintain custom auxiliary state, while the host DBMS remains responsible for storage, transactions, recovery, and all the other queries. A fixed, engine-neutral substrate keeps auxiliary state transactionally consistent under writes, while generated backend adapters handle engine-specific hooks. JetStream generates two kinds of accelerators: tested accelerators, which may use any optimization and are validated by differential testing, and verified accelerators, which trade some performance for a machine-checked proof that every answer satisfies a trusted specification derived from the SQL. On TPC-H at SF=20, JetStream achieves a $584\times$ geomean read speedup over DuckDB ($89\times$ verified) and retains $139\times$ ($46\times$ verified) under a continuous update stream of 10,000 modified rows per second.
查看此版本解读 →查看此版本原文 ↗v2 · 2026-11-02 09:45
JetStream: Generating Verified Query Accelerators for Existing Database Systems
Recent work has shown that LLMs can synthesize highly specialized database systems for fixed workloads, but these systems replace the DBMS's native storage and assume static data: users must migrate their data, often give up ad-hoc queries, and lose acceleration once the data changes. We present JetStream, which instead generates query-specific accelerators that extend an existing DBMS. Given a set of parametrized query templates, a staged agentic workflow synthesizes accelerators that run directly over the DBMS's native tables and may maintain custom auxiliary state, while the DBMS remains responsible for storage, transactions, recovery, and all other queries. A fixed, engine-neutral substrate handles engine-specific hooks and keeps auxiliary state transactionally consistent under writes. JetStream generates two kinds of accelerators: tested accelerators, which may use any optimization and are validated by differential testing, and verified accelerators which trade some performance for a machine-checked proof that every answer satisfies a trusted specification derived from the SQL. On TPC-H at SF=20, JetStream achieves a $315 \times$ geomean read speedup over DuckDB ($93 \times$ verified) and retains $120 \times$ under a continuous update stream of 10,000 modified rows per second.
查看此版本解读 →查看此版本原文 ↗