发表机构
University of Toronto（多伦多大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
Atlas提出首个可验证的基于图的语义搜索系统，通过零知识证明确保查询结果正确性，在SIFT1M和1亿向量规模下实现亚秒级和2秒的证明时间，同时保持召回率并保护索引隐私。
AI 中文摘要
语义搜索是现代应用的核心原语，为推荐系统、网络搜索以及语言模型的检索增强生成提供支持。服务提供商控制索引和查询执行，使得客户端只能信任结果来自对预期索引运行的正确算法。提供商可能为了降低成本而截断搜索、偏置结果，或以其他方式在未被察觉的情况下偏离规定的执行。可验证性可以通过证明结果遵循对已提交索引的约定算法来消除这种信任假设。高效地实现这一点很困难，因为大规模检索依赖于HNSW，这是一种基于图的算法，其数据相关的遍历路径难以映射到零知识证明的固定约束系统上。因此，先前的可验证系统针对规则的、基于聚类的索引进行设计，这些索引更易于编码，但牺牲了基于图的搜索的召回率。我们提出了Atlas，一个允许提供商证明查询已针对其已提交的索引正确回答而不泄露索引的系统。其核心是针对HNSW搜索的新型零知识证明，基于三种技术构建：预处理将所有数据库相关的成本转移到离线阶段，使得每次查询的证明开销随遍历路径而非数据库规模增长；将HNSW重构为固定大小状态的流程，并证明该流程返回相同结果；以及时间步标记的批处理，将整个遍历的每一步论证合并为一个。Atlas首次展示了大规模可验证的基于图的搜索，在SIFT1M基准上不到一秒即可证明一个查询，在1亿向量上仅需2.0秒，同时保持明文HNSW的召回率，并且除结果外不泄露任何关于索引的信息。在完整的RAG流水线中，Atlas的可验证检索保持了端到端的答案质量，并且以比所有先前的可验证检索系统更低的证明成本达到更高的质量。
英文摘要
Semantic search is a core primitive of modern applications, powering recommender systems, web search, and retrieval-augmented generation for language models. The provider controls the index and query execution, leaving clients to trust that results come from the right algorithm over the intended index. A provider may truncate search to cut cost, bias results, or otherwise deviate from the specified execution undetected. Verifiability can remove this trust assumption by proving that results follow the agreed algorithm over a committed index. Realizing this efficiently is hard, as retrieval at scale relies on HNSW, a graph-based algorithm whose data-dependent traversal maps poorly onto the fixed constraint systems of zero-knowledge proofs. Prior verifiable systems therefore target regular, cluster-based indices that are easier to encode, sacrificing the recall of graph-based search. We present Atlas, a system that lets a provider prove a query was answered correctly against its committed index without revealing the index. At its core is a new zero-knowledge proof for HNSW search, built on three techniques: preprocessing that shifts all database-dependent cost offline, so per-query proving scales with the traversal rather than the database; a restructuring of HNSW into a fixed-size-state procedure that we prove returns the same result; and a timestep-tagged batching that merges the per-step arguments of the entire traversal into one. Atlas is the first to demonstrate verifiable graph-based search at scale, proving a query in under a second on the SIFT1M benchmark and in 2.0 seconds at 100 million vectors, while maintaining the recall of plaintext HNSW and revealing nothing about the index beyond the result. In a complete RAG pipeline, Atlas' proven retrieval preserves end-to-end answer quality, and reaches higher quality at lower proving cost than all prior verifiable retrieval systems.
Comments18 pages
