AI 中文总结
Logos是一款结合Rocq机械化语义与LLM指导的SQL重写验证工具，解决了现有工具的不足，在389个查询对的评估中解决率达86.9%，优于基线工具SQLSolver。
AI 中文摘要
SQL重写验证必须考虑重复行、可观测行顺序以及带类型的值语义。现有验证工具尚未将任意有限基数数据库实例的证明与嵌套的、区分并列项的top-k的有序列表语义相结合。无界系统主要针对包（bag）进行推理，或通过语法导向的限制处理排序；而有界系统要么仅支持受限的top-k形式，要么施加确定性排序，而非保留所有由并列项引发的合法结果。对带类型的表达式和聚合语义、可观测运行时错误以及完整性约束的支持也仍不完整。在Rocq中，我们对带类型SQL核心的组合逻辑语义进行了机械化，该语义包含顺序敏感型算子，捕获了所支持片段中所有可能的有序列表和可观测SQL错误。据我们所知，这是首个将嵌套的、区分并列项的top-k与从包等价到有序列表等价的基于闭包的提升相结合的机械化SQL语义，既实现了包理论推理的合理复用，又在顺序敏感型和关联型上下文中保持了组合性。该形式化还提供了面向PostgreSQL的标量和聚合评估的可执行语义，以及对完整性约束的明确说明。基于此语义，我们提出了Logos——一个用于无界SQL重写等价性的LLM指导型Rocq验证工具。其智能体使用经过验证的SQL专用引理库来构建针对具体查询的Rocq证明。我们的评估覆盖了来自Apache Calcite优化器测试、TPC-H和TPC-DS重写以及WeTune实际应用工作负载的389个查询对。Logos解决了其中86.9%的查询对，而最强基线工具SQLSolver的解决率为64.0%。
英文摘要
SQL rewrite verification must account for duplicate rows, observable row order, and typed value semantics. Existing verifiers have yet to combine proofs over database instances of arbitrary finite cardinality with an ordered-list semantics for nested, tie-sensitive top-k. Unbounded systems reason primarily over bags or handle ordering through syntax-directed restrictions, whereas bounded systems either support only restricted top-k forms or impose a deterministic ordering rather than retain all legal tie-induced outcomes. Support for typed expression and aggregate semantics, observable runtime errors, and integrity constraints also remains partial. In Rocq, we mechanize a compositional logical semantics for a typed SQL core with order-sensitive operators, capturing all possible ordered lists and observable SQL failures in the supported fragment. To our knowledge, this is the first mechanized SQL semantics to combine nested, tie-sensitive top-k with a closure-based lifting from bag equivalence to ordered-list equivalence, enabling sound reuse of bag-theoretic reasoning while preserving compositionality across order-sensitive and correlated contexts. The formalization further provides executable semantics for PostgreSQL-oriented scalar and aggregate evaluation and an explicit account of integrity constraints. Building on this semantics, we present Logos, an LLM-guided Rocq verifier for unbounded SQL rewrite equivalence. Its agent uses a verified SQL-specific lemma library to construct query-specific Rocq proofs. Our evaluation covers 389 query pairs from Apache Calcite optimizer tests, TPC-H and TPC-DS rewrites, and WeTune's real-application workloads. Logos solves 86.9% of them, compared with 64.0% for SQLSolver, the strongest baseline.
Comments13 pages, 4 figures, and 3 tables
