PaperlayerView exact revision on arXiv

Source-linked AI summary

Atlas: Efficient Verifiable Semantic Search

Nikolay Avramov, Hidde Lycklama, Alexander Viand, Anwar Hithnawi

arXiv:2609.11841v1cs.CR

TL;DR

Semantic-search clients must currently trust providers to execute the intended algorithm over the intended index, while HNSW’s data-dependent traversal is difficult to verify efficiently. Atlas provides a zero-knowledge proof for HNSW search using offline preprocessing, fixed-size-state restructuring, and timestep-tagged batching, achieving scalable proving with plaintext-HNSW recall and strong RAG results.

  • Problem

    Provider-controlled semantic search can deviate from the intended index or execution, while HNSW’s data-dependent traversal is difficult to encode in zero-knowledge proofs.

  • Method

    Atlas proves complete HNSW search execution against a committed private index using offline consistency preprocessing, fixed-size-state restructuring, and timestep-tagged batching.

  • Results

    Atlas preserves plaintext-HNSW recall, proves SIFT1M queries in 0.8 seconds and 100-million-vector queries in 2.0 seconds, and achieves higher RAG answer quality at lower proving cost than prior verifiable retrieval systems.

  • Takeaways & Limitations

    Atlas demonstrates verifiable graph-based semantic search at scale while revealing nothing about the index beyond the result.

  • Takeaways & Limitations

    The threat model assumes a provider publishes a binding commitment to its index, and soundness is relative to that committed index rather than database well-formedness.

Abstract

from arXiv · show

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.

1 Introduction

Atlas addresses the difficulty of proving graph-based semantic search by adapting HNSW to zero-knowledge proofs while preserving its retrieval quality and efficiency. It achieves scalable proving and maintains strong recall in large-scale benchmarks and RAG pipelines.

  • Challenge: HNSW’s data-dependent branching, priority queues, and early exits make its traversal difficult to encode in fixed zero-knowledge constraint systems.Prior verifiable systems instead use cluster-based indices, whose regular structure sacrifices recall because unreachable neighbors outside selected clusters cannot be recovered.
  • Motivation: Atlas proves HNSW search against a committed index without revealing the index, addressing trust in provider-controlled semantic retrieval.The system targets applications including search, recommendation, and retrieval-augmented generation.
  • Approach: Atlas shifts database-dependent consistency checks offline, so per-query proving scales with traversal length rather than database size.HNSW visits only O(logN) of N nodes, but naive consistency checks would otherwise scan the entire committed index.
  • Approach: Atlas restructures HNSW into a fixed-size-state procedure and merges traversal-step arguments using timestep-tagged batching.The restructuring preserves HNSW’s result, while batching avoids separate auxiliary polynomials and identities for every step.
  • Evaluation: 0.8 seconds proves a SIFT1M query, while BIGANN-100M takes 2.0 seconds and Atlas preserves plaintext-HNSW recall in end-to-end RAG.The proven search remains within 0.8 recall@1 points of plaintext HNSW at 95th-percentile budgets, and exceeds 0.9 recall@1 at deployable configurations.

2 Background

The background introduces zk-SNARKs and the polynomial arguments used to encode computation traces, multiset relations, selections, vectors, and unions. These abstractions provide the constraint-system building blocks for Atlas.

  • 2.1 zkSNARKs from Polynomial IOPs: zk-SNARKs let a prover demonstrate correct computation on private inputs with a short, non-interactive proof without revealing the witness.They combine polynomial interactive oracle proofs with polynomial commitment schemes.
  • 2.1 zkSNARKs from Polynomial IOPs: Polynomial interactive oracle proofs encode execution traces as polynomial evaluations and enforce correctness through identities over an evaluation domain.The constraints must hold at every point of the domain, equivalently through divisibility by its vanishing polynomial.
  • 2.2 Arguments: Permutation arguments prove that two evaluation sequences contain the same multiset, while lookup arguments prove that query values occur in a table.Lookup permits repeated or unused table entries through witness-supplied multiplicities.
  • 2.3 Extensions: Vector inputs compress tuples across several trace polynomials into field elements using a verifier challenge, with negligible collision probability.This allows permutation and lookup interfaces to accept multi-polynomial tuples.
  • 2.3 Extensions: Selector polynomials restrict arguments to chosen trace regions, and unions combine values from multiple polynomials or subsets.Selectors evaluate to one on a selected subset and zero elsewhere; unioning multiplies the corresponding product polynomials.

3 Related Work

Prior verifiable retrieval systems mainly prove searches over regular cluster-based indices, while concurrent zkRAG proves HNSW directly with different disclosure and encoding choices. Atlas complements verifiable inference by addressing retrieval verification.

  • Verifiable Semantic Search: VeriRAG and V3DB prove searches over IVF cluster-based indices whose fixed structure encodes compactly but can lower recall.Clusters are selected by centroid distance alone, so a nearer neighbor outside the searched clusters may be missed.
  • Verifiable Semantic Search: zkRAG also proves HNSW search but reveals the number of steps at every layer, whereas Atlas uses a single fixed bound and reveals no query-dependent information beyond the result.The two systems also differ in how they verify beam-search priority queues.
  • Private ANN Search: Private ANN systems hide queries or access patterns while assuming faithful execution, making their trust model different from Atlas’s provider-verification setting.Compass adds integrity under an inverted trust model in which the client owns the data.
  • Verifiable ML Inference: Verifiable inference systems prove model computations and can be combined with Atlas to verify both retrieval and the downstream RAG response.The two lines of work address complementary pipeline stages.

4 System Overview

Atlas lets clients verify HNSW semantic-search results against a committed provider index while preserving privacy, soundness, and sublinear per-query efficiency. Its proof reexecutes the data-dependent search, using fixed-budget traversal and commitment-consistency checks to make the process verifiable.

  • 4 System Overview: Atlas enables a client to verify that a semantic-search query was answered correctly against a provider-maintained database.The system’s goals are privacy, soundness relative to the committed index, and sublinear per-query cost.
  • Threat Model: The provider’s threat model includes stale or altered indices, truncated traversals, biased rankings, forged proofs, and clients seeking graph or embedding information.The provider first publishes a binding commitment to the index, while index well-formedness is treated as orthogonal.
  • 4.1 Our Approach: Atlas proves a complete HNSW-SEARCH execution, including visited nodes, distance comparisons, and intermediate algorithm state, rather than relying on a succinct certificate.The proof establishes that the returned embeddings are the result of running HNSW-SEARCH on the private committed graph.
  • 4.1 Our Approach: Lookup arguments verify that traversed edges and embeddings match committed tables without requiring a full dataset scan during each query.The setup commits separately to the embedding table and upper- and bottom-layer edge tables.
  • 4.1 Our Approach: Atlas flattens upper-layer traversal, replaces data-dependent termination with fixed greedy and beam step budgets, and proves traversal steps jointly.The greedy phase selects the nearest neighbor at each step, while the bottom-layer beam search extends the candidate set.

5 Design

Atlas addresses HNSW’s data-dependent termination and evolving beam-search state by restructuring the algorithm into fixed-size traversals and encoding the remaining control flow with compact polynomial constraints. It further reduces proving overhead by merging per-timestep arguments into single timestep-tagged arguments while preserving the original search behavior.

  • Design overview: Atlas separates HNSW’s proof challenge into algorithmic restructuring and algebraic constraint encoding.The restructuring confines non-inherent data dependence; the remaining behavior is expressed as polynomial constraints.
  • Unifying greedy search: Atlas unifies the L upper-layer greedy traversals into one graph with drop-down edges, and the resulting walk reproduces each per-layer search at local minima.The unified traversal uses lexicographic distance-and-layer ordering to select intra-layer moves or descend when appropriate.
  • Fixed-size traversals: Fixed budgets replace query-dependent termination: Atlas pads the unified upper traversal and bottom search, with 95th-percentile budgets costing less than one recall@1 point.A search exceeding its budget terminates early with its current candidate set.
  • Correctness: Candidate-selection invariance shows that changing neighbor insertion order does not change the node extracted from the candidate set at any iteration.This supports treating each restructured traversal step as a deterministic batched operation for proving.
  • Constraint design: Beam-search state is represented by prover-supplied witness flags, so each branch becomes a value substitution under identical constraints at every timestep.The construction avoids materializing the query-dependent candidate and visited sets.
  • Timestep-tagged batching: Timestep-tagged arguments merge the per-step membership and equality claims into one invocation, avoiding separate auxiliary polynomials and identities for every traversal step.A shared tag polynomial identifies each trace region while the argument spans the full trace.

6 Evaluation

Atlas preserves high retrieval quality while making verifiable HNSW search practical across large datasets and end-to-end RAG workloads. Its proving cost scales mainly with search configuration and embedding dimension, and it compares favorably with prior verifiable systems.

  • 6.2 Accuracy: Recall@1 stays within 0.8 points of FAISS at every integer-dataset configuration when the budget is fixed at the 95th percentile.This percentile budget shortens the proof trace by 13% to 57% relative to the maximum.
  • 6.2 Accuracy: The 95th-percentile beam-step count rises from 38 on SIFT1M to only 44 on BIGANN-100M at (M,ef) = (16,32).The beam-step budget depends primarily on ef and only logarithmically on corpus size.
  • 6.2 Accuracy: Quantization alone can reduce recall@1 by 5.2 points on GIST1M, from 92.6% to 87.4% at (M,ef) = (32,64).This loss is measured at maximum budget, where fixed-step search matches unbounded HNSW.
  • 6.3 Performance: Atlas proves queries in 0.80 seconds on SIFT1M and 1.98 seconds on BIGANN-100M while targeting recall@1 above 0.9.At 10M and 50M vectors, proving takes 1.22 and 1.99 seconds, respectively.
  • 6.3 Performance: Embedding dimension substantially increases proving cost: GIST1M requires 36.66 seconds and a 75.5 kB proof at d = 960.Verification time rises from under 71 milliseconds for d ≤128 to 1.94 seconds on GIST1M.
  • 6.3 Performance: Atlas’ proving cost is lower than prior verifiable search systems at every recall level, including 2.8× faster than zkRAG at matched parameters.With multithreading, Atlas also reaches V3DB’s recall levels 10× to 45× faster.
  • 6.3 Performance: In RAG, Atlas reaches 73.6 F1 on SQuAD and 45.6 on KILT-NQ at 13.3 seconds per query, while projection to d = 128 cuts proving time 3× with a 3.5–6.1 F1 loss.Atlas also exceeds VeriRAG’s F1 at a fraction of its proving time.

A Extended Background Material

The extended material describes cq, a lookup argument that converts a product check into a logarithmic-derivative sum check. Preprocessing caches table-dependent commitments so per-query proving depends on the query side.

  • A Extended Background Material: cq converts equality of products into equality of reciprocal sums through a logarithmic-derivative check at a random challenge.The reduction is sound by the Schwartz–Zippel lemma.
  • A Extended Background Material: cq precomputes the table-side contribution, making per-query proving cost scale with the query side rather than the table size.The protocol is designed for tables far larger than the query.
  • A Extended Background Material: Setup stores KZG commitments to cached quotient polynomials derived from the table, at O(N logN) cost depending only on the table.These commitments later support sparse query-side combinations.
  • A Extended Background Material: The protocol checks well-formedness of B, well-formedness of A, and equality of their sums.The final sum equality is verified with a univariate sumcheck whose quotient costs O(nlogn).

B.1 Equivalence of the Unified Greedy Search

The unified greedy search restructures layered HNSW traversal into one graph while preserving the original greedy walk and its termination result. Its total traversal combines intra-layer steps with one drop-down per layer.

  • B.1 Equivalence of the Unified Greedy Search: The unified graph labels each layer’s vertices and edges separately, adding drop-down edges between corresponding copies.This converts the layered traversal into a single invocation of greedy search over Gupper.
  • B.1 Equivalence of the Unified Greedy Search: The unified search terminates at the same result node as layered HNSW greedy search.The proof argues this by reproducing each layer’s walk and descending only after reaching that layer’s local minimum.
  • B.1 Equivalence of the Unified Greedy Search: Because corresponding vertices share embeddings, a drop-down edge cannot beat a strictly closer intra-layer neighbor under the lexicographic rule.At a layer’s local minimum, ties favor the lower-layer copy, forcing descent.
  • B.1 Equivalence of the Unified Greedy Search: Each layer contributes its original greedy steps plus one drop-down transition to the next lower layer.The resulting traversal count is Tg = ∑L ℓ=1 T*ℓ + L.

B.2 Proof of Lemma 1

Lemma 1 shows that bounded insertion preserves the exact top-ef set: after all insertions, the maintained window equals the ef closest elements.

  • B.2 Proof of Lemma 1: The final window equals the ef closest elements after bounded insertions and evictions.If the candidate union has at most ef elements, no eviction occurs; otherwise, the furthest element is removed without discarding any member of the target top-ef set.

B.3 Proof of Lemma 2

Lemma 2 establishes that the two candidate-processing executions remain equivalent despite temporary evictions. Their differing temporary candidates cannot alter which node is extracted or when termination occurs.

  • B.3 Proof of Lemma 2: The two executions select the same nodes and maintain the same retained window at every iteration.The induction starts from the identical entry-point state and applies Lemma 1 after each batch of insertions.
  • B.3 Proof of Lemma 2: Temporarily admitted then evicted candidates are farther than the current window and trigger termination before extraction.This leaves both executions extracting the same next node.

B.4 Proof of Theorem 3

Theorem 3 argues that the batched procedure reproduces the sequential SEARCH-LAYER execution. It preserves both the selected-node sequence and the maintained window, yielding the same final output when the budget is sufficient.

  • B.4 Proof of Theorem 3: The batched merge produces the same selected-node sequence and maintained window as sequential insertion.The selection rule matches SEARCH-LAYER extraction, while Lemma 1 makes the batched merge equivalent to sequential insertion.

C Preprocessing

Atlas pays the embedding- and edge-table commitment cost once per index, with preprocessing scaling nearlinearly with domain size. On evaluated datasets, one polynomial costs 9.6 seconds for SIFT1M and GIST1M and 167 seconds for BIGANN-10M.

  • C Preprocessing: Preprocessing is a one-time cost per committed index for the embedding and edge tables.The reported cost covers generating one column’s cached quotients for each committed polynomial.
  • C Preprocessing: Preprocessing grows nearlinearly with domain size at roughly ten microseconds per table entry.Figure 4 reports preprocessing time per committed polynomial across domain sizes from 2^15 to 2^27, accelerated on an H100 GPU through icicle.
  • C Preprocessing: 9.6 seconds per polynomial is reported for SIFT1M and GIST1M, versus 167 seconds for BIGANN-10M.
Loading 2609.11841v1…