该论文关注语义检索的可验证性问题。现代应用的推荐系统、网页搜索与大模型 RAG（检索增强生成）都依赖语义检索：服务提供方掌握索引并执行查询，客户端只能被动信任结果确实由约定算法在指定索引上产生。恶意或成本敏感的提供方可能截断检索结果、引入排序偏差，甚至悄悄偏离约定执行流程而不被察觉。可验证检索通过零知识证明消除这一信任假设——在不泄露索引的前提下证明结果确实按照约定算法在已承诺的索引上得出。然而要高效实现这一目标非常困难：大规模检索依赖 HNSW 这一基于图的近似最近邻算法，其数据依赖的遍历路径难以映射到零知识证明固定的约束系统上。已有可验证系统因此退而求其次，采用规则化、基于聚类的索引结构，编码更简单，但牺牲了图检索的召回率。本文提出 Atlas：其核心是一套针对 HNSW 搜索的新型零知识证明，由三项技术构成——(1) 预处理把所有与数据库规模相关的开销转移到离线阶段，使单次查询的证明开销只随遍历过程而非数据库规模增长；(2) 将 HNSW 重构为固定大小状态的流程，并证明该重构返回与原算法相同的结果；(3) 时间步标记批处理，把整个遍历中每一步的论证合并为一个。Atlas 是首个在规模化场景下演示可验证图检索的系统：在 SIFT1M 基准上单查询证明耗时低于一秒，在 1 亿向量规模下为 2.0 秒，同时保持与明文 HNSW 相同的召回率，并且除检索结果本身外不泄露任何索引信息。在完整 RAG 流水线中，Atlas 的可验证检索保持端到端答案质量，且相比此前所有可验证检索系统，在更低证明成本下达到更高答案质量。适合关注可信 AI 基础设施、隐私增强技术、向量数据库与 RAG 安全的研究者与工程师阅读。