Atlas proves graph-based semantic search results quickly and privately
Atlas: Efficient Verifiable Semantic Search
Cryptography and Security
Summary
Semantic search helps computers find results based on meaning, but usually you must trust the search provider to be honest about how they found answers. The authors created Atlas, a system that lets providers prove they did the search correctly without revealing their data. Atlas uses clever math to make these proofs fast, even on huge datasets, while keeping search quality the same. This can help users trust recommendations or search results without giving up privacy or performance.
What this means in practice
- •For search engine developers: Provide verifiable proofs that search results come from the intended data and algorithm to increase user trust without revealing sensitive data.
- •For language model integrators: Ensure retrieval-augmented generation uses proven correct search results to guarantee end-to-end answer quality in AI applications.
Authors
Nikolay Avramov, Hidde Lycklama, Alexander Viand, Anwar Hithnawi
Abstract
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.