paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Graphiti: Bridging Graph and Relational Database Queries

Graphiti:桥接图数据库与关系数据库查询
PLDI 9(PLDI)2025匹配度 3/10 · 该论文是程序验证/自动推理方向的工作(将 Cypher 与 SQL 查询等价性归约为 SQL 等价性验证),与用户关注的静态分析/形式化验证在方法论上有交集,且兼具形式化定义(database transformer)与工具实现,符合其口味;但它既不涉及 LLM/Agent 与静态分析的交叉,也不涉及浮点程序分析或贝叶斯程序分析,与研究画像的核心问题没有直接关联。引用 3 inbox
Yang He, Ruijie Fang, Işıl Dillig, Yuepeng Wang
crossref: 2026-09-10

AI 速览

一句话:提出将 Cypher 图查询与 SQL 关系查询的等价性检查归约为 SQL 查询等价性验证的方法与工具 Graphiti。

本文研究如何自动判定 Cypher 图数据库查询与 SQL 关系查询之间的等价性。由于二者基于不同数据模型,作者首先提出 database transformer 概念,用以在模型之间转换数据库实例并定义“模 transformer 的等价性”。基于此,论文提出一种验证方法:通过语法制导翻译将 Cypher 的一个子集嵌入 SQL,进而把原始跨模型等价问题归约为两个 SQL 查询之间的等价性检查,从而复用已有的 SQL 自动推理技术,避免同时推理两种数据模型。作者实现了工具 Graphiti,并用于检查图查询与关系查询的等价性。实验表明,Graphiti 既能证明等价也能发现不等价,并能揭示 Cypher 教程和学术论文中隐藏的细微错误。

问题
如何自动检查 Cypher 图查询与 SQL 关系查询在语义上是否等价,尤其是在两种数据模型之间缺乏统一语义基础的情况下。
方法
引入 database transformer 形式化跨模型等价性,并通过语法制导翻译将 Cypher 子集嵌入 SQL,从而把问题归约为成对 SQL 查询的等价性验证。
评估
实现 Graphiti 工具,在 Cypher 与 SQL 查询上评估,表明其既能验证等价也能反驳等价,并发现教程和论文中的细微错误。
原文摘要(Abstract)

This paper presents an automated reasoning technique for checking equivalence between graph database queries written in Cypher and relational queries in SQL. To formalize a suitable notion of equivalence in this setting, we introduce the concept of database transformers , which transform database instances between graph and relational models. We then propose a novel verification methodology that checks equivalence modulo a given transformer by reducing the original problem to verifying equivalence between a pair of SQL queries. This reduction is achieved by embedding a subset of Cypher into SQL through syntax-directed translation, allowing us to leverage existing research on automated reasoning for SQL while obviating the need for reasoning simultaneously over two different data models. We have implemented our approach in a tool called Graphiti and used it to check equivalence between graph and relational queries. Our experiments demonstrate that Graphiti is useful both for verification and refutation and that it can uncover subtle bugs, including those found in Cypher tutorials and academic papers.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot3124,
  title = {Graphiti: Bridging Graph and Relational Database Queries},
  author = {Yang He and Ruijie Fang and Işıl Dillig and Yuepeng Wang},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {PLDI},
  year = {2025},
  doi = {10.1145/3729319}
}