# Atlas: Efficient Verifiable Semantic Search

arXiv: https://arxiv.org/abs/2609.11841 · HTML: https://mlsanity.com/paper/2609.11841/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in RAG robustness and adaptive retrieval, one of 15 directions in Retrieval-augmented generation.
- Builds on 14 of its 43 references that are in the map.
- First posted on arXiv 10 Sep 2026.

## Placed in

- Retrieval-augmented generation / [RAG robustness and adaptive retrieval](https://mlsanity.com/rag/rag-robustness-and-adaptive-retrieval/)

## Builds on (most cited first, 14 of 14)

- [Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2005.11401/) (2020)
- [SQuAD: 100,000+ Questions for Machine Comprehension of Text](https://mlsanity.com/paper/1606.05250/) (2016)
- [TriviaQA: A Large Scale Distantly Supervised Challenge Dataset for Reading Comprehension](https://mlsanity.com/paper/1705.03551/) (2017)
- [Qwen2 Technical Report](https://mlsanity.com/paper/2407.10671/) (2024)
- [M3-Embedding: Multi-Linguality, Multi-Functionality, Multi-Granularity Text Embeddings Through Self-Knowledge Distillation](https://mlsanity.com/paper/2402.03216/) (2024)
- [Efficient and robust approximate nearest neighbor search using Hierarchical Navigable Small World graphs](https://mlsanity.com/paper/1603.09320/) (2016)
- [KILT: a Benchmark for Knowledge Intensive Language Tasks](https://mlsanity.com/paper/2009.02252/) (2020)
- [PoisonedRAG: Knowledge Corruption Attacks to Retrieval-Augmented Generation of Large Language Models](https://mlsanity.com/paper/2402.07867/) (2024)
- [ANN-Benchmarks: A Benchmarking Tool for Approximate Nearest Neighbor Algorithms](https://mlsanity.com/paper/1807.05614/) (2018)
- [zkLLM: Zero Knowledge Proofs for Large Language Models](https://mlsanity.com/paper/2404.16109/) (2024)
- [HERS: Homomorphically Encrypted Representation Search](https://mlsanity.com/paper/2003.12197/) (2020)
- [Artemis: Efficient Commit-and-Prove SNARKs for zkML](https://mlsanity.com/paper/2409.12055/) (2024)
- [V3DB: Audit-on-Demand Zero-Knowledge Proofs for Verifiable Vector Search over Committed Snapshots](https://mlsanity.com/paper/2603.03065/) (2026)
- [Onyx: Cost-Efficient Disk-Oblivious ANN Search](https://mlsanity.com/paper/2604.20401/) (2026)

## Abstract (arXiv)

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.