Atlas: Efficient Verifiable Semantic Search
arXiv:2609.11841v1 [cs.CR] 10 Sep 2026
Nikolay Avramov1 , Hidde Lycklama1 , Alexander Viand2 , Anwar Hithnawi1 1 University of Toronto 2 Belfort Labs
Abstract
similarity, it can retrieve relevant content even when it has little lexical overlap with the query. Approximate nearestneighbor (ANN) search [1, 29] makes this practical at scale: instead of computing exact nearest neighbors, it returns sufficiently close points, enabling low-latency search over billions of vectors. This ability to retrieve by meaning at massive scale has made semantic search a default mechanism for finding relevant content in modern systems.
Semantic search is a core primitive of modern applications, powering recommender systems, web search, and retrievalaugmented 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
Retrieval-grounded AI systems are only as reliable as the passages they retrieve: production systems have returned incorrect answers after surfacing stale or erroneous content [30], and attackers have exploited the retrieval path, planting documents that hijack generation once retrieved [45]. Semantic search also plays a role in content provenance, where it is used to detect copyrighted material in AI pipelines or attribute generated content to rightholders [6, 24, 25, 33, 41]. In such settings, the incentives to deviate from the intended protocol can be substantial. ANN search likewise underpins recommendation systems for social networks, e-commerce, advertising, and dating platforms [7, 39]. In each of these settings, the search is executed by a third-party provider that controls both the index and the computation, while the client sees only the returned results. This opacity leaves room for failures and/or deliberate deviations. A provider may serve stale results, truncate the search to cut costs, bias the ranking toward preferred outcomes, or quietly depart from the specified algorithm. These risks compound as semantic search is increasingly embedded in automated pipelines spanning multiple services that run on third-party infrastructure, where retrieved results are consumed directly by downstream services with no human oversight. These concerns have already drawn public scrutiny and regulatory interest [10, 42]. Clients therefore need a way to verify semantic-search correctness: a guarantee that the returned set is exactly the one produced by the specified algorithm over an index to which the provider committed in advance.
Introduction
Recommender systems, web search, and retrieval-augmented generation (RAG) for large language models increasingly rely on semantic search [26]. Semantic search embeds items and queries as vectors and returns the nearest items to the query in this space. Because proximity is intended to capture semantic
Zero-knowledge proofs (ZKPs) [13, 14] can, in principle, provide such a guarantee. The provider generates a succinct proof that the returned search result is correct, which the client can verify without learning anything about the database beyond the result itself. Realizing this for semantic search, how1
ever, is challenging. The de facto standard for ANN search at scale is HNSW [29]. HNSW is control-flow heavy by construction: it navigates a layered proximity graph using priority queues, data-dependent branching, and early exits. Such computation maps poorly onto the arithmetic constraint systems underlying modern ZKPs, which require circuits to be fixed in advance and provisioned for worst-case behavior at every step. To overcome this, prior verifiable search systems avoid HNSW and instead build on cluster-based indices [27, 34]. These methods partition the dataset into clusters offline and answer a query by searching the clusters nearest to it. This fixed, data-independent search pattern encodes compactly as polynomial constraints. This data-independence, however, sacrifices recall, as the clusters are selected once and a closer neighbor outside them is unreachable for the remainder of the search. HNSW, by contrast, selects nodes throughout the search, conditioning each step on measured distances to the query, and its candidates therefore keep improving whereas a cluster-based search is confined to its initial selection. Clusterbased systems thus trade retrieval quality for provability, and the adaptivity that quality requires is exactly what a fixed constraint system struggles to capture. In this paper, we present Atlas, an efficient zero-knowledge proof system for HNSW search. Atlas enables a provider to prove that a query was answered correctly against a committed index, while retaining the graph-based traversal on which modern retrieval systems rely. The proven search matches the recall of plaintext HNSW at lower proving cost than all existing verifiable search systems, cluster-based and graph-based alike. Atlas achieves these results through three key ideas. (i) Preserving HNSW’s sublinear per-query cost. HNSW answers a query by visiting only O(log N) of the index’s N nodes. Every visited node and traversed edge, however, must be proven consistent with the committed index. A naive consistency check reads the entire committed index, and the O(log N) search then incurs a linear proving cost. We decouple the consistency check from the traversal and defer its databasedependent cost to a preprocessing phase via cq lookup arguments [8]. The per-query proving cost then scales with the length of the traversal rather than the size of the database, preserving HNSW’s sublinearity. (ii) Restructuring HNSW. We eliminate nearly all data-dependent control flow from HNSW by reformulating search as a procedure over fixed-size state and a fixed number of steps. Concretely, we collapse the multilayer descent into a single graph walk and replace the two interdependent priority queues with one bounded candidate set. This reformulation substantially shrinks the trace to be proven, as each step merges an entire neighborhood into the set in a single batched update rather than one node at a time. These structural changes preserve the search exactly, as we prove the reformulated output equivalent to HNSW’s. The step bound is the only point at which the reformulated search differs from HNSW, with sufficiently large budgets recover-
ing HNSW’s result exactly and smaller ones lowering proving cost at the expense of recall. (iii) Compacting the per-step constraints. A naive encoding instantiates separate permutation and lookup arguments for each traversal step over the corresponding region of the witness. Each instantiation introduces its own auxiliary polynomials and polynomial identities, causing the proving overhead to grow with the step budget. We introduce timestep-tagged arguments, which tag every tuple with a step identifier and merge the per-step arguments of the entire traversal into a single invocation. Evaluation Summary. We implement Atlas and evaluate it on six standard ANN benchmarks, spanning one million to one hundred million vectors and embedding dimensions from 96 to 960, as well as on end-to-end RAG pipelines with learned text embeddings (§6). Atlas proves a query over SIFT1M in 0.8 seconds, with a 16.5 kB proof that the client verifies in 40 milliseconds. Proving cost scales with the beam width and step budget needed to reach a recall target, not with database size, and the 100× larger BIGANN-100M raises proving time only 2.5×, to 2.0 seconds. Truncation to a fixed step budget sacrifices little recall, as at 95th-percentile budgets the proven search stays within 0.8 recall@1 points of plaintext HNSW on integer datasets and every dataset exceeds 0.9 recall@1 at a deployable configuration. In a complete RAG pipeline, Atlas preserves this quality end to end, attaining higher answer quality at lower proving cost than prior verifiable retrieval systems.
2
Background
This section reviews the building blocks of our construction: zk-SNARKs from polynomial interactive oracle proofs (§2.1), the permutation and lookup arguments (§2.2), and the interface extensions used throughout (§2.3).
2.1
zkSNARKs from Polynomial IOPs
A ZKP is a protocol in which a prover convinces a verifier that a statement holds without revealing anything beyond its validity. A zero-knowledge Succinct Non-Interactive Argument of Knowledge (zk-SNARK) is a ZKP that is additionally succinct and non-interactive, producing a single short proof that a computation on private inputs was executed correctly. Concretely, the prover proves knowledge of a witness w for a public statement x of an NP relation R, i.e. (x, w) ∈ R, without revealing w to the verifier. A standard construction of zk-SNARKs combines a Polynomial Interactive Oracle Proof (PIOP) with a Polynomial Commitment Scheme (PCS) [3,12]. In a PIOP, the prover’s messages are polynomials, provided to the verifier as oracles that can be queried at a small number of points. A PCS instantiates the oracles with commitments: the prover sends a short commitment in place of each polynomial and answers each query with an evaluation proof. 2
A PIOP enforces the correctness of a computation as a set of polynomial identities representing its execution trace. We focus on univariate PIOPs, in which the trace is encoded as evaluations of polynomials over a multiplicative subgroup H = {1, ω, ω2 , . . . , ωn−1 } ⊆ F of order n. Each length-n sequence of trace values a0 , . . . , an−1 is interpolated as the unique polynomial p of degree below n with p(ωi ) = ai . The identities take the form g(p1 (X), . . . , pk (X)) = 0, required to hold at every point of H. An identity holds over all of H exactly when its polynomial is divisible by the vanishing polynomial ZH (X) = X n − 1, and the committed quotient serves as the proof, verified at a random evaluation point. Every computation defines its own trace polynomials, but the constraints imposed on them are largely generic and the literature formalizes the recurring ones as self-contained arguments with their own auxiliary polynomials and identities. Many recurring constraints reduce to two relations between multisets of values, enforced by the permutation argument, proving two sequences are reorderings of each other, and the lookup argument, proving every value of one sequence occurs in a second [12, 15]. The copy constraint, a specialized instance of the permutation argument, is the central mechanism connecting the polynomial identities of modern PIOPs by enforcing the consistency of a value’s copies across them [12]. The lookup argument in turn replaces constraints that are expensive to encode arithmetically with membership in a precomputed table, as in range checks [11, 15].
2.2
set of values of a second, the table. Containment is weaker than multiset equality, as a table entry may be used by several queries or by none, and the two products are therefore matched by reweighting the table side. For a query polynomial f (X) and a table polynomial t(X) over H, each table factor is raised to a multiplicity m j ≥ 0, supplied by the prover as a witness subject to ∑ j m j = n: n−1
i=0
2.3
Extensions
Vectors. A trace entry is often a tuple of values across several polynomials, while the product factors range over sin$
gle field elements. A verifier challenge α ← − F compresses each tuple into one element, and two distinct tuples collide at a random α with negligible probability by the Schwartz– Zippel lemma. Both interfaces accept vectors of polynomials ( f1 (X), . . . , fd (X)), entering the identity as the combination
Permutation Argument. The permutation argument proves that two polynomials take the same multiset of values over the evaluation domain. Each polynomial’s evaluations over H form a multiset, and the product encoding turns the equality of the two multisets into an equality of product polynomials. For a(X) and b(X) over H, the argument proves
d
⃗f (X) = ∑ αc−1 fc (X). c=1
Selection. A claim rarely concerns a polynomial’s full domain, and an argument may apply to one region of the trace or to entries the prover designates. Such restrictions are realized through selector polynomials, which evaluate to 1 on a subset of the domain and to 0 elsewhere. A selector is fixed when preprocessed into the constraint system and witness when supplied by the prover, and selectors compose by multiplication. For a subset S ⊆ H, we write f (X)|S for the evaluations of f (X) over S, entering the identity as the composite f (X) S = qS (X) · f (X) + 1 − qS (X) · δ,
n−1
∏ X + a(ωi ) = ∏ X + b(ωi ) . i=0
.
j=0
The inputs to the two arguments extend beyond single trace polynomials. Both identities consume their inputs only through their evaluations, and any polynomial expression over the trace polynomials therefore defines a valid input, with its evaluations as the encoded multiset. We define three such constructions, each extending the interfaces Eq and Mem with a notation for its inputs.
Permutation and lookup arguments reduce claims about multisets to polynomial identities by encoding each multiset as a product over its elements. Concretely, a multiset of field elements defines the polynomial ∏v (X + v), with one factor per occurrence of an element v. A polynomial factors into linear terms in exactly one way, and two multisets are therefore equal exactly when their product polynomials are equal.
m j
The multiplicity m j counts the queries that use table entry j, unused entries take m j = 0, and the identity holds for some choice of multiplicities exactly when every evaluation of f (X) occurs among the evaluations of t(X). Fixing every multiplicity to one instead recovers the permutation argument [15]. We invoke the argument through the interface Mem f (X), t(X) .
Permutation and Lookup Arguments
n−1
n−1
∏ X + f (ωi ) = ∏ X + t(ω j )
i=0
We invoke the argument through the interface Eq(a(X), b(X)), where each polynomial input stands for the multiset of its evaluations over the domain. Lookup Argument. The lookup argument proves that the set of values of one polynomial, the query, is contained in the
where qS (X) is the selector of S and δ is a public default value. 3
Unions. A claim may collect values from several polynomials or several subsets at once, and the corresponding input is the union, in which each part contributes its evaluations. Unioning multiplies the product polynomials, as the product over a union is the product over its parts: X +v = ∏ X +v · ∏ X +v . ∏
knowledge proofs to show that a committed model produced a claimed output [4, 28, 35, 40]. These works are complementary to ours and can be combined to build RAG pipelines. Verifiable inference frameworks can be used to prove the model computations while Atlas provides verifiability for the retrieval step. Together, they enable a client to verify an end-to-end retrieval-augmented response.
3
4
v ∈ f (X)|S ⊎ g(X)|S′
v ∈ f (X)|S
v ∈ g(X)|S′
Related Work
System Overview
Atlas is a system that enables a client to verify that a semantic search query was answered correctly against a providermaintained database. This section introduces the setting, the threat model and security goals, and describes our approach at a high level. The full construction follows in §5.
Verifiable Semantic Search. Existing work on verifiable semantic search largely targets cluster-based indices. VeriRAG [27] and V3DB [34] construct zero-knowledge proofs for search over IVF indices [19, 38], which partition the data into clusters offline and answer a query by exhaustively scanning the clusters nearest to it. This regular structure encodes compactly as fixed polynomial constraints but lowers recall, as the clusters are selected by centroid distance alone, and for a query whose nearest neighbor lies outside them, the search returns a more distant vector. Our evaluation confirms this gap, as the product quantization these systems rely on bounds recall well below deployable targets (§6). Concurrent to our work, Jiang et al. propose zkRAG [21], a zero-knowledge proof that directly encodes the HNSW search algorithm, differing from Atlas’ restructuring in two respects. First, zkRAG preserves the layered graph structure and therefore relies on revealing the number of steps taken at every layer. Atlas’ merged traversal runs under a single fixed bound (§5.1.1) and reveals no query-dependent information beyond the search result. Second, zkRAG verifies the two priority queues of beam search through a specialized PIOP for queue updates. Atlas replaces the two queues with a single bounded set, which we show leaves the search result unchanged (§5.1.2), and efficiently constrains the set’s updates through one batched merge per iteration.
Setting. We consider a standard semantic search service, in which a provider maintains a database D of N vectors. Given an input query q ∈ Rd , the service aims to find the k nearest vectors under a distance measure d(·, ·) such as the ℓ2 distance. To scale to large databases, the provider builds an HNSW graph G, which organizes the dataset into L + 1 layers G0 , . . . , GL , where G0 holds the full dataset and each Gℓ contains a small fraction of the nodes of Gℓ−1 . To resolve a query q, the provider runs HNSW-S EARCH (Algorithm 1): the search starts at a fixed entry point in the top layer, greedily visiting neighboring nodes and proceeding downward when no neighbor at the current layer is closer to q. In the bottom layer, it performs a beam search of width ef and returns topk (W ), the k elements of the final candidate set W nearest to the query, as the result. Throughout, N(u) denotes the neighborhood of node u in the graph. System Goals. A verifiable semantic search system must achieve three properties, (i) privacy, a client learns nothing beyond what the query result reveals, (ii) soundness, a client receives the correct search result with respect to the committed index, and (iii) efficiency, the per-query cost to both provider and client is sublinear in the database size. We state soundness relative to the index rather than the database, as approximate search is inherently index-dependent and a different index can yield a different result set.
Private ANN Search. Private ANN search addresses a setting orthogonal to ours: these systems hide the query from the server but assume it executes the search faithfully. Tiptoe supports cluster-based search using linearly homomorphic encryption [17], HERS performs exhaustive matching over FHE-encrypted representations [9], and Compass performs HNSW search while hiding access patterns with ORAM [44]. Compass additionally provides integrity, but under an inverted trust model: the client owns the database, maintains the index graph itself, and outsources only storage, whereas in our setting the provider controls both and the client learns only results. Onyx extends the ORAM-based design by moving the client logic into a server-side TEE, executing the search inside an enclave [37], obtaining integrity from attestation at the cost of hardware trust.
Threat Model. We consider two parties, a provider that holds the index and answers queries, and a client that issues queries and verifies the responses. Either party may be corrupted by a malicious adversary. A corrupted provider may deviate from the protocol arbitrarily: it may answer from a stale or altered index, truncate the traversal, bias the ranking, or forge a proof for a result. A corrupted client may try to learn as much information as possible from the provider’s response, such as information about the index graph’s structure, edges, or embeddings. The query is sent to the provider in the
Verifiable ML Inference. A recent line of work on verifiable inference, often referred to as zkML, uses zero4
clear. We assume that before serving any query, the provider publishes a binding commitment to its index G that clients can learn. Finally, the search result is bound to the committed index, but claims about the well-formedness of the index are orthogonal1 .
4.1
Algorithm 1: HNSW-S EARCHef ,k (G, q) Input :Multi-layer graph G with layers G0 , . . . , GL and entry point epGL ∈ GL , query vector q, beam width ef , number of results k Output :k nearest neighbors of q found by the search 1 ep ← epGL 2 for ℓ ← L to 1 do 3 W ← S EARCH -L AYER1 (Gℓ , q, ep) 4 ep ← arg minx∈W dist(x, q)
Our Approach
5 W ← S EARCH -L AYERef (G0 , q, ep)
At the core of Atlas is a new zero-knowledge proof construction for the HNSW-S EARCH algorithm. Unlike many graph algorithms, including shortest-path search, HNSW admits no succinct certificate that can be verified in place of recomputing the result. Its traversal is greedy and data-dependent, and the correctness of a result can therefore be established only by reexecuting the search itself. Our proof consequently verifies a complete execution of the search, including the visited nodes, their distance comparisons, and the intermediate algorithm state. More formally, our proof shows that a set of embeddings R is the result of correctly executing the HNSW-S EARCH algorithm for a query q on a private index G committed to by c, i.e., a proof of knowledge for the relation
6 return topk (W )
Online Phase: Consistency. In the online phase, the prover shows that every edge and embedding on the traversed path is consistent with the commitments to G. Lookup arguments are the natural primitive for these consistency checks, as they prove that claimed values appear in a committed table. Most, however, incur prover cost linear in the table size, so the proof costs as much as a full dataset scan and the sublinearity that motivates the index is lost. We therefore specifically choose the cq lookup argument [8, 16], whose per-query prover cost is independent of the table size after a one-time preprocessing of the table. We perform this preprocessing once at index construction, in time O(N log N) matching the cost of constructing G, and the prover’s per-query cost then scales with the traversal’s length rather than the graph’s size.
((c, q, R), G) : R = HNSW-S EARCHef ,k (G, q) R = , ∧ c = Commit(G) where ef and k are public configuration parameters of HNSW. Setup Phase. The prover commits to the index G with three commitments: one to an embedding table, which stores the embeddings of the entire database D, and two to edge tables, one for the upper L layers of the HNSW graph and one for the bottom layer. The i-th row of the embedding table contains a node identifier and its embedding vector ei ∈ FDp , i.e.,
Online Phase: Traversal. We encode HNSW’s traversal in two parts, the greedy search in the upper layers and the beam search in the bottom layer. In the flattened upper graph, each node is referenced by a tuple (u, ℓ) of node identifier and level, as the same node appears at several layers. In place of each layer’s data-dependent termination condition, we bound the traversal by a fixed step budget Tg over the unified graph Gupper and Tb for the beam search in the lowest layer. For the greedy search, the prover shows at each step that the selected node is a neighbor of the current node and the nearest one to the query, with all steps proven jointly by a single batched argument (§5.2.1). Once the traversal reaches the bottom layer, it no longer suffices to identify a single next node, as the beam search must maintain and update a dynamic set of ef candidates. Encoding this dynamic behavior is the main challenge of our construction, and we address it in §5.1.
h i (0) (D−1) idi , ei , . . . , ei . greedy
We split the edge list into two tables, Ted and Tedbeam , as nodes in the upper L layers have M neighbors and nodes in greedy layer 0 have 2M. Row i in the greedy table Ted contains a tuple of node identifier idi and level ℓi , followed by M tuples of neighbors, i.e., h i (0) (M−1) idi , ℓi , idnb , ℓi , . . . , idnb , ℓi , idi , ℓi − 1 .
5
The final tuple (idi , ℓi − 1) represents a downward edge to the same node one layer below. This flattening of the upper layers into a single graph Gupper enables the optimizations of the search’s dynamic termination that we present in §5.1.
Design
Proving HNSW search in a zkSNARK requires bridging a mismatch between the algorithm’s data-dependent execution and the fixed constraint system that a zkSNARK demands. How long the search runs and how much state it accumulates both vary with the query, and the constraint system must provision for both in advance. We first identify the two sources
1 Existing techniques can be used to show the well-formedness, i.e., that its edges connect genuinely nearby vectors, or that its construction followed any particular distribution.
5
the evolving state, as each admission can evict W ’s furthest element (line 14) and tighten the threshold for every neighbor after it. A direct proof would therefore have to unroll the loop into one step per neighbor, each carrying its own copy of W , C, and v and encoding every branch the update could take. With this, the cost of expanding a single node would scale as a product of the neighborhood size and the worst-case queue sizes. Through our restructuring of the algorithm state, we process each neighborhood in a single batched update instead of a chain of sequential insertions.
Algorithm 2: S EARCH -L AYERef (Gℓ , q, ep) Input :layer graph Gℓ , query vector q, entry point set ep, beam width ef Output :ef nearest neighbors of q found at this layer 1 v ← ep; C ← ep; W ← ep 2 while |C| > 0 do 3 c ← arg minx∈C dist(x, q); C ← C \ {c} 4 f ← arg maxx∈W dist(x, q) 5 if dist(c, q) > dist( f , q) then 6 break 7 8 9 10 11 12 13 14
for e ∈ NGℓ (c) do if e ∈ / v then v ← v ∪ {e} f ← arg maxx∈W dist(x, q) if dist(e, q) < dist( f , q) or |W | < ef then C ← C ∪ {e}; W ← W ∪ {e} if |W | > ef then W ← W \ {arg maxx∈W dist(x, q)}
5.1
Restructuring HNSW
In this subsection, we reformulate the HNSW algorithm to support more efficient dynamic termination and reduce the complexity of proving beam search. Concretely, we fix the number of search steps, resolving the data-dependent termination of Challenge 1, and collapse the interdependent sets of Challenge 2 into a single set of fixed size ef . First, we organize the L + 1 layers into two graphs, merging the L per-layer greedy traversals into a single traversal by encoding layer transitions as edges, removing the need for a separate encoding per layer. Second, we replace the beam phase algorithm with an equivalent procedure whose internal state is only a single bounded set, turning each iteration into one batched update rather than a chain of sequential insertions. We prove that the restructured search (Algorithm 3) produces the same output as the original (Algorithm 1).
15 return W
of this mismatch, then resolve it in two stages. The first stage (§5.1) is algorithmic and confines the data dependence that is not inherent to the search. The second stage (§5.2) is algebraic and encodes what remains as compact polynomial constraints. Challenge 1: Data-dependent Termination. HNSW search is inherently dynamic. While on average the search terminates within log N steps, the actual number of search steps at each layer varies and is not known in advance. The S EARCH L AYER algorithm (Algorithm 2) returns when the nearest unexplored node is further from the query than the furthest node in the result set (line 6). This termination condition depends on the query and the index, and a fixed constraint system must therefore encode the worst-case traversal of every layer. The proving cost of every query is then that of L worst-case layer traversals. We collapse the upper L layers into a unified graph representation Gupper , turning their L traversals into one. We then bound the total number of steps of the greedy and beam search phases, in place of encoding L worst-case layer traversals.
5.1.1
Unifying Greedy Search
To avoid padding every layer’s traversal to its worst-case length (Challenge 1), we reorganize the multi-layer graph G into two components, the bottom graph G0 and an upper graph Gupper that merges the L layers of the greedy search. The starting point of the search in each layer is the end node of the previous layer, and the downward transition can therefore be represented as an edge from (v, ℓ) to (v, ℓ−1), making the layer boundary disappear into the edge set. This enables us to replace the L separate calls to S EARCH -L AYER1 (Gℓ , q, ep) (line 3) with a single call to S EARCH -L AYER′1 (Gupper , q, ep). S EARCH -L AYER′ is defined in the same way as S EARCH -L AYER but compares nodes by the pair (d(v, q), ℓ) lexicographically, i.e., the walk moves to a strictly closer neighbor whenever one exists and otherwise breaks distance ties in favor of the lower layer. We define the unified upper graph Gupper as the union of all per-layer edge sets together with the drop-down edges {((v, ℓ), (v, ℓ−1)) : v ∈ Gℓ , ℓ ≥ 1}. The single invocation S EARCH -L AYER′1 (Gupper , q, {(ep, L)}) terminates at (v∗1 , 0), the node reached by the original greedy phase (lines 1–4 of Algorithm 1), after Tg = ∑Lℓ=1 Tℓ∗ + L steps, where Tℓ∗ counts the greedy steps at layer ℓ. We state and prove this equivalence as Theorem 4 in §B.1. Since (v, ℓ) and (v, ℓ−1) share the
Challenge 2: Beam Search State Tracking. Where greedy search maintains only a single node as its frontier, beam search holds up to ef nodes at the same time. As a result, the choice of which nodes to explore next depends not only on the local neighborhood of the current node, but on all ef −1 other candidates as well: a node may be dropped from consideration because closer candidates exist in an entirely different region of the graph. The algorithm tracks this exploration with three data structures (line 1): a result set W of at most ef elements, and a candidate set C and visited set v that both grow with the traversal (lines 9, 12). Each neighbor of an expanded node is first checked against the visited set v (line 8) and then admitted into both W and the candidate queue C if it improves on W ’s furthest element. The admission depends on 6
same embedding, d((v, ℓ−1), q) = d((v, ℓ), q), and the lexicographic comparison therefore selects the drop-down edge only when no intra-layer neighbor is strictly closer to q, i.e., exactly when S EARCH -L AYER1 (Gℓ , q, ·) would terminate. The walk on Gupper thus reproduces each per-layer search and descends at its local minimum. We pad each of the two remaining traversals to a fixed budget, the walk in Gupper to Tg steps and the search in G0 to Tb steps. The restructuring leaves only these two bounds to provision, in place of a worst-case traversal for each of the L layers, and both are set from the observed distribution of total step counts. A search exceeding its budget terminates early with its current candidate set, which at 95th-percentile budgets costs less than one recall@1 point on the integer datasets (§6). 5.1.2
a query point. Inserting the elements of A into W in any order, with the furthest element from q evicted whenever |W | > ef , as in lines 7–14 of Algorithm 2, always yields topef (W ∪ A), the ef elements of W ∪ A nearest to q. Invariance of the search result under C. The orderindependence of W does not immediately imply the same property for the candidate set C. A neighbor enters C only if it is close enough to be in W at the moment it is processed, and the admission threshold, namely the distance of W ’s current worst element, changes as the neighborhood is processed. Different insertion orders therefore expose each neighbor to different thresholds, and a node admitted under one order may be rejected under another. For example, let W have capacity ef = 2 and hold nodes with distances {5, 8}, and let the current node’s neighbors be represented by distances {3, 7, 9}. If 3 is processed first, it evicts 8 and the threshold drops to 5, so 7 is rejected and only 3 is added to C. If 7 is processed first, it is added to C, only to be evicted from W when 3 arrives. Both orders yield the same final W , holding {3, 5}, but different candidate sets: C = {3} versus C = {3, 7}. However, this difference never results in a different output of S EARCH -L AYER. First, any node for which the two executions disagree is only included in W temporarily and is subsequently removed; therefore, its distance is greater than that of every node in the final set W . Second, C is kept in ascending order of distance, and S EARCH -L AYER terminates as soon as the extracted node is further than W ’s worst element (line 6). A disputed node is therefore selected only after every closer candidate, and when its turn comes, it triggers termination rather than expansion. The extra elements of C are redundant, as both executions process the same nodes in the same order.
Single-set Beam Phase
Beam search is more complex than greedy because the algorithm maintains multiple candidates simultaneously, tracked by two priority queues W and C, and each neighbor must be evaluated against the evolving state of both. Inserting a node into the result set W can change its worst element and, with it, the insertion threshold for the next node. The 2M neighbors of each selected node must therefore be processed sequentially, requiring O(M · ef ) constraints per iteration. The candidate set C compounds this issue, as its size has no fixed bound and must be allocated for the worst case. We eliminate both obstacles by reformulating the beam search around a single bounded set that can be updated efficiently, with a flag marking the elements already processed. The reformulation rests on two observations: (i) the state of W after processing a neighborhood does not depend on the order in which neighbors are inserted, and (ii) although the contents of C do depend on insertion order, this difference never influences the search result. Using the two observations, we replace the sequential neighbor insertions of each step with a single merge of the 2M neighbors into the bounded set, and the queue C with a flag. In the following, we discuss and prove both observations, then present the restructured beam search.
Lemma 2 (Candidate-Selection Invariance). Two executions of S EARCH -L AYER (Algorithm 2) on the same (G, q, ep, ef ), that differ only in the order in which neighbors are inserted at line 7, extract the same node from C at line 3 at every iteration. We prove Lemmas 1 and 2 in §§B.2 and B.3. The two lemmas show that the two-queue structure is unnecessary: neither the sequential insertion order nor the unbounded queue C affects the search result. The result set W ’s final state is order-independent, and C is only required to track which candidates in W have not yet been processed. As a result, we can replace C with a flag on the elements of W that indicates whether they have been processed (Phase 2 of Algorithm 3). At each iteration, the nearest unprocessed element is selected, and its entire neighborhood is merged into the set in a single batch by taking the union of the current candidates and the selected node’s neighbors, sorting by distance, and keeping the nearest ef . We provide a formal description of the restructured version in Algorithm 3. The sequential per-
Order Independence of the Result Set. At each iteration of S EARCH -L AYER (Algorithm 2), the neighborhood exploration loop (line 7) inserts neighbors into W sequentially, evicting the furthest element when |W | > ef (line 14). Although the intermediate states of W vary with the insertion order, its final state is always topef (W ∪ neighbors), the ef elements nearest the query among W and the neighbors combined. The neighborhood can therefore be processed as a single batched operation, whose constraint cost scales additively (O(M + ef )) rather than multiplicatively (O(M · ef )). Lemma 1 (Order Independence of W ). Let W be a set of at most ef elements, let A be a set of new elements, and let q be 7
5.2.1
neighbor insertions are replaced by one batched merge per step, and the unbounded queue C is eliminated entirely.
Trace Encoding. The greedy search traverses the unified upper graph of §5.1, at each step moving from the current node to its neighbor nearest to the query, for a fixed budget of Tg steps. Concretely, the trace is encoded in witness polynomials over a shared evaluation domain, and the walk occupies Tg regions of B = M + 1 consecutive points, one region per step. The first point of region t is the selected point, at which the polynomials encode the node selected at step t, and the remaining M points are the neighbor points, encoding the selected node’s neighborhood in the graph. The selected points across the segment form the position set Selg and the neighbor points the set Nbg , each with a preprocessed selector polynomial, qSelg and qNbg . For a position set S, we write S(t) for its positions in region t, and S− for S without the last point of each region. The polynomials id(X), ℓ(X), and d(X) encode the identifier, layer, and claimed squared distance to the query of the node at every point, and e1 (X), . . . , eD (X) its embedding. Each step of the walk explores the selected node’s neighborhood, computes every node’s distance to the query, and selects the nearest neighbor. We prove the sequence with three constraint sets, edge consistency for the explored neighborhoods, distance verification for the computed distances, and candidate selection for the nearest neighbor.
Theorem 3 (Beam Search Equivalence). Let ep ∈ G0 , q ∈ Rd , and ef be an entry point, query, and beam width, and let T ∗ be the number of iterations of S EARCH -L AYERef (G0 , q, ep) (Algorithm 2). For any budget Tb ≥ T ∗ , Phase 2 of Algorithm 3 returns the same final set. We prove Theorem 3 in §B.4. Algorithm 3: HNSW-S EARCH -R ESTRUCTef ,k,Tg ,Tb (G, q)
Input :graph G with unified upper graph Gupper , layer-0 graph G0 , and entry point epGL , query vector q, beam width ef , number of results k, step budgets Tg and Tb Output :k nearest neighbors of q found by the search // Phase 1: greedy search on Gupper 1 c ← (epGL , L) 2 for t ← 1 to Tg do 3 c ← arg minn∈NG
upper (c)
dist(n, q)
4 (ep0 , ·) ← c
// Phase 2: batched beam search on G0 5 W ← {(ep0 , dist(ep0 , q), 0)} 6 visited ← {ep0 } 7 for t ← 1 to Tb do 8 9
if {(n, d, p) ∈ W : p = 0} = 0/ then continue
10
(nsel , dsel , ·) ← arg min(n,d,p)∈W, p=0 d W ← W \ {(nsel , dsel , 0)} ∪ {(nsel , dsel , 1)} S ← W ∪{(e, dist(e, q), 0) : e ∈ NG0 (nsel )\visited} visited ← visited ∪ NG0 (nsel ) W ← topef (S)
11 12 13 14
Edge Consistency. The neighbor points of each region encode the selected node’s neighborhood, supplied by the prover as evaluations of id(X) and ℓ(X). Each claimed neighborhood must therefore be proven equal to the selected node’s edge list in the committed graph. The edge table Ted stores a node’s full edge list as a single entry, while the trace encodes the list across the region’s M neighbor points. We assemble each region’s edge list into one tuple through replicated polynomials id( j) (X) and ℓ( j) (X) for j ∈ [M], copy-constrained at every point of a region to the values of id(X) and ℓ(X) at the region’s j-th neighbor point, and write ⃗a(X) for the assembled vector (id(X), ℓ(X), id(1) (X), ℓ(1) (X), . . . , id(M) (X), ℓ(M) (X)). A single membership argument enforces that every region’s assembled list is an entry of the edge table: Mem ⃗a(X) Selg , Ted .
15 return topk (W )
5.2
Greedy Search
Constraint Design
The restructured algorithm of §5.1 makes each traversal step a single batched operation, which is significantly more efficient to prove. A remaining difficulty is the search’s branching, which depends on which nodes have been considered and which candidates have been processed. The algorithm tracks this state in sets of query-dependent size and contents. In this section, we express the search as polynomial constraints, with this state supplied by the prover as witness flags, so each branch reduces to a value substitution, every timestep runs identical constraints, and neither set is ever materialized. We present the constraints of the greedy search first, as the simpler of the search’s two phases. We then discuss beam search as an extension of the greedy constraints.
Throughout, f (X) S denotes the restriction of f (X) to the position set S, as defined in §2.3. Distance Verification. Every node’s distance to the query is supplied by the prover as an evaluation of d(X), and each claimed value must be proven equal to the true distance. A node’s distance is determined by its embedding, and correctness is enforced in two parts, an embedding consistency lookup tying each node’s embedding to the committed dataset and a polynomial identity tying each claimed distance to the embedding. The lookup proves every point’s identifier and 8
embedding to be an entry of the embedding table Temb : Mem (id(X), e1 (X), . . . , eD (X)) Selg ∪Nbg , Temb .
the tag-extended tuples. Tuples match only when their tags agree, and a query therefore matches only the table entries of its own timestep. For the neighborhood membership, the tagged argument proves all Tg claims at once: Mem (τ(X) − 1, id(X)) Selg , (τ(X), id(X)) Nbg .
The identity D 2 d(X) − ∑ qi − ei (X) i=1
Nbg
=0
The query side’s tag is shifted by one, tagging the selected point of region t + 1 with t to group each selected node with the neighborhood it was selected from.
constrains each claimed distance to the squared ℓ2 distance between the public query (q1 , . . . , qD ) and the proven embedding.
5.2.2
Candidate Selection. Selecting the nearest neighbor amounts to two claims, that the selected node is drawn from the preceding step’s neighborhood and that no neighbor is nearer to the query. We enforce the first claim through a membership constraint, proving that the selected node of each step is a member of the preceding step’s neighborhood. Concretely, both are encoded in id(X): the selected node at region t + 1’s selected point and the neighborhood at region t’s neighbor points. We instantiate a membership argument of id(X) into itself, with the selected positions as the query and the neighbor positions as the table: Mem id(X) (t+1) , id(X) (t) . (1) Selg
Beam Search
Trace Encoding. The beam phase operates on the single candidate set of §5.1, at each step processing the nearest unprocessed candidate and merging its neighborhood into the set, for a fixed budget of Tb steps (Phase 2 of Algorithm 3). Concretely, the search is laid out across Tb regions of Bb = max(ef , 2M) + 1 consecutive evaluation points, one region per step. A region must hold the step’s candidate set of ef entries and the selected candidate’s neighborhood of 2M entries, and Bb therefore fits the longer of the two alongside the selected point. As in the greedy segment, the first point of region t is the selected point, encoding the candidate processed at step t, with its identifier and distance carried by id(X) and d(X). The two lists share the region’s points through separate pairs of polynomials. The polynomials idcan (X) and dcan (X) encode one candidate’s identifier and distance per point over the first ef points, and idnb (X) and dnb (X) one neighbor’s identifier and distance per point over the first 2M points. The candidate positions across the segment form the position set Canb , the neighbor positions Nbb , and the selected points Selb , each with a preprocessed selector polynomial. We discuss the constraints that enforce the correctness of the two operations, candidate selection and candidate set update.
Nbg
The argument enforces that the identifier at each selected point equals one of those at the preceding region’s neighbor points. To constrain the selected node to be the nearest to the query among all neighbors, it suffices to show that the difference between each neighbor’s distance and the selected node’s distance is nonnegative. We introduce a helper polynomial dsel (X), equal at every point of region t to the selected distance of region t + 1 through a copy constraint. A membership argument into the range table Trange , a preprocessed table of the nonnegative integers {0, . . . , 2r − 1}, enforces that every difference is nonnegative: Mem (d(X) − dsel (X)) Nbg , Trange . (2)
Candidate Selection. We reuse the nearest-neighbor selection constraints of the greedy search to select the next candidate. In particular, the membership argument (Equation (1)) applies with the selected point as the query and the region’s candidate entries as the table, proving the selected candidate a member of the step’s candidate set, and the minimality check (Equation (2)) applies with idcan (X) and dcan (X) in place of id(X) and d(X). The difference is that the choice now depends on the processed status, as only unprocessed candidates must be selected. We therefore extend the constraints to exclude processed candidates from the selection. The prover supplies the processed flag as a polynomial proc(X), equal to 0 at candidates not yet processed and 1 at processed candidates. We use the flag to substitute d∞ for every processed candidate’s distance, defining the substituted distance d˜can (X): d˜can (X) − dcan (X) · (1 − proc(X)) − d∞ · proc(X) Can = 0,
Timestep-Tagged Argument. The membership arguments of candidate selection are instantiated once per timestep, as (t+1) each is restricted to a different pair of position sets, Selg (t) against Nbg . The Tg separate instances result in significant prover overhead, each requiring auxiliary polynomials and identities of its own. The pattern appears throughout the rest of the constraint design, as membership and equality claims are typically local to a timestep, each naively requiring a separate argument restricted to its region. We reduce this overhead by collapsing the per-timestep instances of each claim into a single argument over the full trace, which we refer to as a timestep-tagged argument. Concretely, we extend every tuple with a shared preprocessed tag polynomial τ(X), equal to t over region t, and prove the single argument over
b
where d∞ is a public constant that exceeds every achievable squared ℓ2 distance. The minimality check then applies with 9
d˜can (X) in place of dcan (X):
We introduce a helper polynomial dworst (X), equal at every point of region t to the last retained distance of region t + 1 through a copy constraint. A membership argument into the range table enforces that every difference is nonnegative: Mem (drest (X) − dworst (X)) Nb , Trange .
Mem (d˜can (X) − dsel (X)) Can , Trange . b
Every processed candidate’s distance thus exceeds every unprocessed one’s, and processed candidates never influence the selection. The flag itself remains an unconstrained witness, and the last remaining step is enforcing its consistency with the trace, which we describe in §5.2.3.
b
Under the sorted order, dworst (X) holds the furthest retained distance, and every discarded entry therefore lies at least as far from the query as every candidate of step t + 1. Previously considered neighbors must not re-enter the candidate set, as the set could otherwise hold several copies of the same node. We reuse the witness-flag mechanism of candidate selection, with a considered flag per neighbor supplied as the polynomial cons(X), equal to 1 exactly at the neighbors considered at an earlier step. The identity d˜nb (X) − 1 − cons(X) · dnb (X) − cons(X) · d∞ =0
Candidate Set Update. Following the restructuring of §5.1, the candidate set update merges the selected candidate’s entire neighborhood into the candidate set in one batched operation. Concretely, at each step t, the two lists are merged and sorted by distance, the ef nearest entries become the candidate set of step t + 1, and the remaining entries are discarded. We enforce the correctness of the merge, sort, and truncation through three respective arguments: an equality argument enforcing that the input candidate and neighbor lists contain the same entries as the output candidate and discarded lists, a sorting argument enforcing that every region’s candidate entries are in ascending order of distance, and a truncation argument enforcing that every discarded entry is at least as far from the query as the furthest retained one. On the input side, the equality argument takes region t’s candidate and neighbor tuples. On the output side, it takes region t + 1’s candidate entries together with region t’s discarded entries. The retained entries live in the candidate polynomials themselves, as the candidate entries of region t + 1, while the discarded entries are encoded by two further polynomials, idrest (X) and drest (X), over the neighbor positions Nbb . Applying timestep tagging (§5.2.1), we tag the output side’s candidate entries with τ(X) − 1, forcing the input tuples of step t to match the candidate entries of region t + 1:
Nbb
constrains the substituted distance d˜nb (X) to the true distance at unconsidered neighbors and to d∞ at considered ones, and d˜nb (X) replaces dnb (X) on the input side of the equality argument. Considered neighbors thus exceed every retained distance and are routed into the discarded entries by the truncation, never re-entering the candidate set. The considered flag is likewise an unconstrained witness, and we prove its consistency with the trace in the following. 5.2.3
Flag Verification
A further source of complexity in proving the correctness of the beam search is that its choices at each timestep depend on which nodes were considered and which candidates processed at earlier timesteps. Concretely, at each timestep the nearest unprocessed node in the candidate set is selected, and the unconsidered neighbors of the selected node are added to the set. Following the standard treatment of data-dependent control flow in constraint systems [20,31], the prover supplies two flags as part of the witness, a processed flag per candidate for the selection and a considered flag per neighbor for the insertion. The flags must be proven consistent with the trace, since otherwise the prover can arbitrarily influence the search result, for example by falsely flagging a node as considered to exclude it from the result. The difficulty in enforcing the correctness of the flags is that their true values depend on the execution’s history, which naively requires verifying every timestep against all preceding ones, adding substantial prover overhead. In this section, we show how to constrain the flags using a global property of the trace, rather than applying constraints at each individual timestep.
Eq (τ(X), idcan (X), dcan (X), proc(X) + sel(X)) Can
b
⊎ (τ(X), idnb (X), dnb (X), 0) Nb , b
(τ(X) − 1, idcan (X), dcan (X), proc(X)) Can
b ⊎ (τ(X), idrest (X), drest (X), procrest (X)) Nb . b
The edge consistency and distance verification constraints of §5.2.1 apply over the neighbor positions, while the candidate positions require no additional constraints of their own. As the equality argument matches each identifier and its distance as one tuple, every candidate entry originates as a verified neighbor entry of an earlier timestep. The sorting argument enforces that every region’s candidate entries are in ascending order of distance. We enforce nonnegativity of each difference dcan (ωX) − dcan (X) through a range check over Can− b: Mem (dcan (ωX) − dcan (X)) Can− , Trange .
Processed Flags. For the processed flags, consistency with the trace reduces to consistency between adjacent timesteps. A candidate’s processed status changes only at its selection, and a correctly initialized flag consistent across adjacent timesteps
b
The truncation argument enforces that every discarded entry is at least as far from the query as the furthest retained one. 10
is therefore consistent with the trace. Concretely, an update constraint enforces that the flag of the candidate selected for processing equals 1, a preservation constraint enforces that every other candidate’s flag is unchanged between adjacent steps, and an initialization constraint enforces that the flag of newly added candidates equals 0. We realize all three constraints by extending the equality argument of the candidate set update. To identify the selected candidate within the argument, we introduce a selection polynomial sel(X), whose evaluations are one-hot within each region, 1 at the candidate selected for processing and 0 at all others. The argument relates tuples of tag, identifier, and distance, and we extend every tuple with the processed flag as a fourth component:
full set of encountered nodes at every timestep, increasing the evaluation domain’s size from linear in the number of timesteps, O(M · Tb ), to quadratic, O(M · Tb2 ). The set grows by a neighborhood of 2M per timestep, contributing 2M · t evaluations at timestep t and 2M · Tb (Tb + 1)/2 in total. Instead of proving state transitions, we design constraints that enforce the flags’ consistency directly against the trace and avoid resizing the evaluation domain. It suffices to enforce, at every timestep t, that every node flagged considered = 1 and no node flagged considered = 0 appears in a neighborhood of an earlier timestep t ′ < t. The 1-direction is directly enforced through a membership argument against the neighborhoods of all timesteps. A naive enforcement, however, instantiates one argument per timestep, each against the prefix of the trace preceding the timestep. The Tb arguments are each defined over the evaluation domain of size O(M · Tb ), resulting in prover overhead quadratic in Tb . We collapse the Tb per-prefix arguments into a single argument against the full trace through timestep-tagging (§5.2.1). As every trace entry is tagged with its timestep, the prefix preceding timestep t consists exactly of the entries tagged t ′ < t, and membership in the prefix is membership in the full trace under the tag condition. The neighbor positions flagged considered form the witness set Consb , with the selector cons(X) · qNbb (X). The prover supplies as a witness the timestep t ′ (X) at which each node was considered, and a single membership argument over Consb against the full trace, with a range check enforcing t ′ < t, enforces the 1-direction: Mem (idnb (X), t ′ (X)) Cons , (idnb (X), τ(X)) Nb , b b Mem (τ(X) − t ′ (X) − 1) Cons , Trange .
Eq (τ(X), idcan (X), dcan (X), proc(X) + sel(X)) Can
b
⊎ (τ(X), idnb (X), dnb (X), 0) Nb , b
(τ(X) − 1, idcan (X), dcan (X), proc(X)) Can
b ⊎ (τ(X), idrest (X), drest (X), procrest (X)) Nb . b
We set the candidates’ flag component to proc(X) + sel(X) on the input side, updating the selected candidate’s flag to 1 while every other flag is unchanged, enforcing the update and preservation constraints.2 We fix the neighbor tuples’ flag component to 0, enforcing the initialization constraint. It remains to constrain sel(X) to the correct one-hot encoding of the selected candidate. To do so, it suffices to enforce (1) that sel(X) equals 1 at the selected candidate’s point and (2) that sel(X) equals 0 at every other candidate point. We enforce (1) by extending the selected-candidate membership argument of candidate selection with a third tuple component: Mem (τ(X), id(X), 1) Sel , (τ(X), idcan (X), sel(X)) Can . b
b
While the 1-direction is a set membership claim, the 0direction is a non-membership claim, which cannot be efficiently established through lookups alone. Set membership is an existential claim that a membership argument enforces through a witness attesting the queried value’s occurrences in the table (e.g. the multiplicities m j in LogUp). Enforcing the 0-direction would instead require negating the existential (NP) claim, turning it into a universal (coNP) one that must hold for all witnesses. Existing zkSNARKs are defined for existential (NP) relations, and non-membership is therefore typically reduced to an existential claim through one of two approaches, each scaling the evaluation domain’s size quadratically in the number of timesteps. The first approach replaces non-membership in a set with membership in the set’s complement with respect to a fixed universe of elements. In our setting, the universe consists of all 2M · Tb nodes encountered in the trace, and materializing it at each of the Tb timesteps requires 2M · Tb2 evaluations. The second approach is to keep the set sorted and establish non-membership of a value by supplying the gap between consecutive entries in which the value lies. In our setting, the considered set grows by 2M nodes per timestep, and restating it in sorted order at each
b
Tuples match componentwise, and the constant 1 on the query side forces the matched candidate entry, the selected candidate’s, to equal 1 in its sel(X) component. To enforce (2), we introduce the identity sel(X) · (idsel (X) − idcan (X)) Can = 0, b
where idsel (X) is copy-constrained to the selected candidate’s identifier at every candidate point of the region. At every candidate point, one of the two factors equals 0, and sel(X) equals 0 at every candidate other than the selected one. Considered Flags. While the processed state of a timestep is local to the timestep’s candidate set, the considered state spans all nodes encountered at earlier timesteps. Extending the transition-based verification of the processed flags to the considered flags would therefore require materializing the 2 The selected candidate’s flag is necessarily 0 before the update, as the candidate-selection constraints of §5.2.2 enforce that the selected candidate is unprocessed.
11
timestep results in 2M · Tb (Tb + 1)/2 evaluations in total. We instead identify a global property of the trace that suffices for the 0-direction and can be enforced over the existing evaluation domain. In an execution of the algorithm, a node is not considered until its first appearance on the trace. The node identifiers flagged considered = 0 are therefore distinct on the trace. We name the property the uniqueness of unconsidered nodes and enforce it directly, in place of the per-timestep non-membership checks. Enforcing the uniqueness of unconsidered nodes reduces to a standard sorting argument, at a constant number of additional polynomials and constraints. The sorting argument encodes the considered = 0 node identifiers in sorted order, encoding the flag–identifier pairs (cons(X), idnb (X)) as two witness polynomials (s(X), u(X)), sorted by flag first and identifier within each flag value. At positions outside Nbb , the prover sets the flag to 1, and the corresponding pairs sort into the tail of the column. The prover supplies s(X) and u(X) as witnesses, an equality argument enforces that their evaluations are a reordering of the pairs, a polynomial identity enforces that s(X) is nondecreasing, and a range check enforces strict monotonicity between adjacent entries of u(X) over the s(X) = 0 prefix: Eq (cons(X), idnb (X)), (s(X), u(X)) , (s(ωX) − s(X)) · (s(ωX) − s(X) − 1) H − = 0, Mem (u(ωX) − u(X) − 1) (1−s(X))(1−s(ωX))·q − , Trange .
systems retrieve over. GIST1M consists of 960-dimensional GIST image descriptors, representative of high-dimensional retrieval workloads. Together, the integer and floating-point datasets let us separate the cost of the fixed-step approximation from that of quantization. Implementation. We implement Atlas in Rust on top of the halo2-axiom library [2], over the BN254 curve. We extend the library with an implementation of the cq lookup argument [8] and accelerate the cq preprocessing on the GPU using the icicle library [18]. We build each HNSW index with FAISS v1.14.2 at efConstruction = 800, except for BIGANN-50M and BIGANN-100M, where we use efConstruction=200. We use FAISS as the plaintext reference for retrieval quality. Embeddings are quantized to 8-bit field elements, and all distances are squared ℓ2 . We run all experiments on a machine with an AMD EPYC 9654 96core processor, 768 GB of RAM, and an NVIDIA H100 GPU. Proving and verification run on the CPU; preprocessing is accelerated on the GPU. The comparison of systems in Figure 3 runs on hardware chosen to match the published environment of each system as closely as possible, as stated inline. Metrics. For each benchmark, we evaluate on its standard query set and measure retrieval quality as recall@1, the fraction of queries for which the search returns the true nearest neighbor. The ground truth is the nearest neighbor in the original, unquantized embedding space. The reported recall therefore reflects the loss from both quantization and truncation. We report proving time, proof size, and verification time per query, along with the distributions of greedy and beam steps each search takes, which indicate the recall cost of any given choice of Tg and Tb .
H
As the considered = 0 identifiers occupy the prefix of u(X), distinctness of adjacent entries implies distinctness of all entries, and strict monotonicity enforces the uniqueness.
6
Evaluation
We evaluate whether Atlas makes verifiable HNSW search practical without sacrificing retrieval quality. Concretely, this section answers three questions: (i) does Atlas preserve the recall of plaintext HNSW (§6.2)? (ii) what is the cost of verifiability, and how do proving time, proof size, and verifier time scale with corpus size and embedding dimension (§6.3)? and (iii) how does Atlas compare against other verifiable semantic search systems (§6.3)?
6.1
6.2
Accuracy
Atlas proves a fixed-budget search over quantized embeddings, and we evaluate the impact of the two approximations on retrieval quality. For each configuration, we compute the queries using the FAISS library and record the number of greedy and beam steps each query takes. We then evaluate the quality of Atlas’ search with the step budget fixed at different quantiles of this distribution. Figure 1 reports recall@1 at each budget against the unbounded float32 FAISS baseline.
Experimental Setup
Datasets. We evaluate on SIFT1M together with three larger prefixes of SIFT1B, the BIGANN datasets of 10M, 50M, and 100M vectors. These share SIFT1M’s 128dimensional integer descriptors and let us measure cost as the index grows from one million to one hundred million vectors. We also evaluate on Deep10M and GIST1M, two floatingpoint datasets that exercise different regimes. Deep10M consists of 96-dimensional neural network features, representative of the learned embeddings that semantic search and RAG
Cost of Truncation. Recall is preserved when truncating the search well below the maximum observed steps, implying the budget does not need to cover the longest-running queries. Fixing the budget at the 95th percentile shortens the proof trace by 13% to 57% relative to the maximum. Recall@1 stays within 0.8 points of FAISS at every integer-dataset configuration, and several configurations match the baseline within query-set noise. The budget itself is tied to the search parameters rather than the corpus, as the beam steps depend 12
Recall@1 (%)
Recall@1 (%)
Recall@1 (%)
(M, ef) = (8, 16) (M, ef) = (16, 32) 100 99 98 95 90 80 60 40 100 99 98 95 90 80 60 40 100 99 98 95 90 80 60 40
(M, ef) = (32, 64) FAISS, unbounded
SIFT1M
20
20
20
40
60
80
BIGANN-50M
40
40
60
Deep10M
60
80
80
beam step budget Tb
100
100
100
100 99 98 95 90 80 60 40 100 99 98 95 90 80 60 40 100 99 98 95 90 80 60 40
p95 budget
BIGANN-10M
20
40
20
40
20
SIFT1M BIGANN-10M Deep10M BIGANN-50M BIGANN-100M GIST1M
16 26 16 32 16 40 16 40 16 48 64 128
ef Tg
Tb Prove (s) Verify (ms) Proof (kB)
6 26 14 33 21 54 20 50 21 59 9 127
0.80 1.22 1.83 1.99 1.98 36.66
40 50 58 71 70 1940
16.5 16.5 14.5 16.5 16.5 75.5
80
100
Table 1: Prover performance of Atlas at the smallest configuration reaching recall@1 above 0.9 on each dataset, with the step budgets (Tg , Tb ): proving time, verification time, and proof size per query.
60
80
100
60
80
100
SIFT1M in 0.80 seconds, and BIGANN takes 1.22, 1.99, and 1.98 seconds at 10M, 50M, and 100M vectors, respectively. The corpus size affects proving cost only through the search configuration, as a larger corpus requires a larger ef to reach the recall target, which rises from 26 to 48 while M = 16 remains fixed (Table 1). The proving times at 50M and 100M vectors coincide, as the traces of both configurations fit within the same evaluation domain.
GIST1M
beam step budget Tb
Figure 1: Recall@1 of the proven fixed-budget search across beam step budgets Tb , measured at the p50, p95, and maximum budget of each configuration.
Scaling with Embedding Dimension. Beyond the search configuration, proving cost depends on the embedding dimension d, as every distance computation in the trace sums over d coordinates, each represented by a separate polynomial. For GIST1M (d = 960), Atlas proves a query in 36.66 seconds with a 75.5 kB proof, a cost that combines the high dimension with the largest configuration required to reach the recall target (Table 1). Verification time depends on d as well, taking less than 71 milliseconds on every dataset with d ≤ 128 but reaching 1.94 seconds on GIST1M. Dimensionality-reduction techniques make the projected dimension another tunable parameter that trades answer quality for proving cost, which we quantify in our RAG evaluation below.
primarily on ef and the corpus size contributes only logarithmically through the layer count. At (M, ef ) = (16, 32), the 95th-percentile beam step count rises from 38 on SIFT1M to only 44 on the hundredfold larger BIGANN-100M. Cost of Quantization. On the floating-point datasets Deep10M and GIST1M, whose real-valued embeddings are converted to 8-bit integers, quantization introduces an additional recall loss. We isolate this loss by measuring at the maximum budget, where the fixed-step search is equivalent to unbounded HNSW. The remaining gap stems from quantization alone and reaches 5.2 recall@1 points on GIST1M at (M, ef ) = (32, 64) (87.4% against 92.6%).
6.3
M
60
BIGANN-100M
40
Dataset
Comparison to Verifiable Search Systems. Atlas’ proving cost is lower than that of prior verifiable search systems at every recall level (Figure 3). We first compare against zkRAG [21], concurrent work that likewise proves HNSW search and reports only single-threaded prover times. For the same parameters, (M, ef ) = (32, 64), and the same number of processed level-0 nodes (Nexp = 212 ), Atlas proves a query 2.8× faster, in 18.6 seconds on one thread of a Xeon 8151 against zkRAG’s 51.5 seconds on one thread of a Xeon 6126, two processors within 10% in single-core performance. The speedup comes alongside a stronger guarantee, as zkRAG’s proof reveals the number of steps taken at every layer while Atlas’ reveals nothing beyond the result. Atlas’ prover further benefits from multithreaded acceleration, with 16 threads reducing proving time 6.6×, from 18.6 to 2.8 seconds. In the multithreaded setting, Atlas also outperforms V3DB [34], an IVF-PQ system, reaching every recall level V3DB attains between 10× and 45× faster, as product quantization caps
Performance
We evaluate the cost of verifiability for recall@1 above 0.9, as this is a standard target for practical retrieval. For each dataset, we fix the configuration to the smallest setting that achieves the target recall and report proving time, proof size, and verification time per query in Table 1. Atlas’ constraint system is determined by the parameters d, ef , M, Tg , and Tb , and proving cost therefore depends on the configuration required to reach the target recall. Scaling with Dataset Size. At a fixed recall target, proving time increases only modestly as the dataset grows from one to one hundred million vectors. Atlas proves a query on 13
d = 1024
d = 128 (PCA)
VeriRAG
SQuAD-Val
TriviaQA-Val
50
50
20 10 5
20 10 5
M = 32 M = 16
2 1
M=8
M=5
20
30
40
50
60
70
2 1 80
M=8
M=5
20
30
TriviaQA-Train
40
50
60
70
20 10 5
M = 32 M = 16
2 1
M=8
M=5
20
30
40
50
F1 [%]
70
80
zk-opt
5 2
M = 5, ef = 10
M = 32
M=5
0
10
M=8
20
M = 16, ef = 32 M = 8, ef = 16
M = 6, ef = 12
Atlas: Tb = ef 20
30
M = 16
2 1 60
M = 32, ef = 64
10
0.5
50
20 10 5
Nexp = 212
high-acc
1
KILT-NQ
50
zkRAG, 1 thread (Xeon 6126) V3DB (dual EPYC, 256 cores)
20
M = 32 M = 16
Prover time [s]
Prover time [s]
50
Prover time [s]
Atlas, 1 thread (Xeon 8151) Atlas, 16 threads (EPYC)
VeriRAG, F1 unreported
40
50
60
Recall@1 [%]
70
80
90
100
Figure 3: Recall@1 versus per-query proving time on SIFT1M, log scale. 30
F1 [%]
40
50
corpus size, while VeriRAG’s grows directly with the corpus, from 6.6 seconds on SQuAD to 56.0 on TriviaQA-Train and 96.2 on KILT.
Figure 2: F1 versus per-query proving time on SQuAD, TriviaQA-Val, TriviaQA-Train, and KILT-NQ at 256-token chunks, log scale.
References V3DB’s recall@1 at 0.50, a ceiling Atlas exceeds in 0.64 seconds against V3DB’s 29.2 seconds.
[1] Martin Aumüller, Erik Bernhardsson, and Alexander Faithfull. ANN-Benchmarks: A benchmarking tool for approximate nearest neighbor algorithms. Information Systems, 87:101374, 2020.
Application: End-to-end Verifiable RAG. We build a complete RAG pipeline with Atlas and measure how answer quality and proving cost vary with the search configuration. We instantiate Atlas’ proven fixed-budget HNSW search as the retrieval component, and the remaining components follow VeriRAG’s evaluation setting, with BGE-M3 [5] for embedding and Qwen2-7B [43] for generation. We evaluate on SQuAD [36], TriviaQA [22], and KILT [32] at 256token chunks, reporting F1 over the full validation sets for M = 5 to M = 32 with ef = 2M (Figure 2). Unlike the percentile budgets of §6.2, these experiments fix a single corpusindependent budget Tg = Tb = ef . At M = 32, Atlas reaches 73.6 F1 on SQuAD, 70.0 on TriviaQA-Val, 71.6 on TriviaQATrain, and 45.6 on KILT-NQ, at 13.3 seconds of prover time per query. Projecting the embeddings to d = 128 with principal component analysis reduces proving time 3×, to 4.3 seconds, at a cost of 3.5 to 6.1 F1 points across the datasets. We compare against VeriRAG on a 24-core Xeon Platinum 8175M, comparable to the 24-core Xeon Gold 5220 used in their evaluation. Atlas exceeds VeriRAG’s F1 at a fraction of its proving time, reaching 60.3 F1 in 2.5 seconds on SQuAD against VeriRAG’s 46.9 in 6.6, and 51.3 in 3.2 seconds on TriviaQA-Val against 41.1 in 38.7. The gap follows from the retrieval quality bottleneck of IVF-PQ, as the cluster-based index recovers fewer of the most relevant passages and degrades the context the generator receives (§3). Atlas’ proving cost further depends on the search configuration rather than the
[2] Axiom. halo2. https://github.com/axiom-cry pto/halo2, 2022. Fork of the halo2 zero-knowledge proving library. [3] Benedikt Bünz, Ben Fisch, and Alan Szepieniec. Transparent SNARKs from DARK compilers. In Advances in Cryptology – EUROCRYPT 2020, volume 12105 of Lecture Notes in Computer Science, pages 677–706. Springer, 2020. [4] Bing-Jyue Chen, Suppakit Waiwitlikhit, Ion Stoica, and Daniel Kang. ZKML: An optimizing system for ML inference in zero-knowledge proofs. In Proceedings of the Nineteenth European Conference on Computer Systems (EuroSys), 2024. [5] Jianlv Chen, Shitao Xiao, Peitian Zhang, Kun Luo, Defu Lian, and Zheng Liu. M3-Embedding: Multi-linguality, multi-functionality, multi-granularity text embeddings through self-knowledge distillation. In Findings of the Association for Computational Linguistics, ACL 2024, pages 2318–2335. Association for Computational Linguistics, 2024. [6] Copyleaks. AI content & text authenticity detection. https://copyleaks.com/, 2026. Accessed: 2026-0609. 14
[7] Databricks. Mosaic AI vector search. https://docs .databricks.com/aws/en/generative-ai/vect or-search, 2025. Accessed: 2026-06-09.
[18] Ingonyama. ICICLE: A GPU library for zeroknowledge acceleration. https://github.com/i ngonyama-zk/icicle, 2023.
[8] Liam Eagen, Dario Fiore, and Ariel Gabizon. cq: Cached quotients for fast lookups. Cryptology ePrint Archive, Paper 2022/1763, https://eprint.iacr.or g/2022/1763, 2022.
[19] Hervé Jégou, Matthijs Douze, and Cordelia Schmid. Product quantization for nearest neighbor search. IEEE Transactions on Pattern Analysis and Machine Intelligence, 33(1):117–128, 2011.
[9] Joshua J. Engelsma, Anil K. Jain, and Vishnu Naresh Boddeti. HERS: Homomorphically encrypted representation search. IEEE Transactions on Biometrics, Behavior, and Identity Science, 4(3):349–360, 2022.
[20] Kunming Jiang, Fraser Brown, and Riad S. Wahby. CoBBl: Dynamic constraint generation for SNARKs. In 2025 IEEE Symposium on Security and Privacy (SP), pages 3347–3363. IEEE, 2025.
[10] European Parliament and Council. Regulation (EU) 2022/2065 of 19 October 2022 on a single market for digital services (Digital Services Act). https://eur-l ex.europa.eu/eli/reg/2022/2065/oj/eng, 2022. Accessed: 2026-06-09.
[21] Yanze Jiang, Xinyang Yang, Xuanming Liu, Yanpei Guo, and Jiaheng Zhang. zkRAG: Efficiently proving RAG retrieval in zero knowledge. Cryptology ePrint Archive, Paper 2026/709, https://eprint.iacr.org/2026/7 09, 2026.
[11] Ariel Gabizon and Zachary J. Williamson. plookup: A simplified polynomial protocol for lookup tables. Cryptology ePrint Archive, Paper 2020/315, https: //eprint.iacr.org/2020/315, 2020.
[22] Mandar Joshi, Eunsol Choi, Daniel S. Weld, and Luke Zettlemoyer. TriviaQA: A large scale distantly supervised challenge dataset for reading comprehension. In Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics, ACL 2017, pages 1601–1611. Association for Computational Linguistics, 2017.
[12] Ariel Gabizon, Zachary J. Williamson, and Oana Ciobotaru. PLONK: Permutations over Lagrange-Bases for Oecumenical Noninteractive Arguments of Knowledge. Cryptology ePrint Archive, Paper 2019/953, https://eprint.iacr.org/2019/953, 2019.
[23] Aniket Kate, Gregory M. Zaverucha, and Ian Goldberg. Constant-size commitments to polynomials and their applications. In Advances in Cryptology – ASIACRYPT 2010, volume 6477 of Lecture Notes in Computer Science, pages 177–194. Springer, 2010.
[13] Shafi Goldwasser, Silvio Micali, and Charles Rackoff. The knowledge complexity of interactive proof-systems. In Proceedings of the Seventeenth Annual ACM Symposium on Theory of Computing (STOC ’85), pages 291–304, 1985.
[24] Christopher Benjamin Kuhn and Tamay Aykut. Outputbased attribution for content, including musical content, generated by an artificial intelligence (AI). https: //patents.google.com/patent/US12567396, 2026. U.S. Patent No. 12,567,396, assignee Sureel Inc.
[14] Jens Groth. On the size of pairing-based non-interactive arguments. In Advances in Cryptology – EUROCRYPT 2016, volume 9666 of Lecture Notes in Computer Science, pages 305–326. Springer, 2016. [15] Ulrich Haböck. Multivariate lookups based on logarithmic derivatives. Cryptology ePrint Archive, Paper 2022/1530, https://eprint.iacr.org/2022/1530, 2022.
[25] Christopher Benjamin Kuhn, Tamay Aykut, Diego Ponce De Leon Vera, Paul Pauls, and Christoph Burgmair. Adjusting attribution for content generated by an artificial intelligence (AI). https://patents. google.com/patent/US12554767, 2026. U.S. Patent No. 12,554,767, assignee Sureel Inc.
[16] Hossein Hafezi, Gaspard Anthoine, Matteo Campanelli, and Dario Fiore. SoK: Lookup table arguments. Cryptology ePrint Archive, Paper 2025/1876, https: //eprint.iacr.org/2025/1876, 2025.
[26] Patrick Lewis, Ethan Perez, Aleksandra Piktus, Fabio Petroni, Vladimir Karpukhin, Naman Goyal, Heinrich Küttler, Mike Lewis, Wen-tau Yih, Tim Rocktäschel, Sebastian Riedel, and Douwe Kiela. Retrieval-augmented generation for knowledge-intensive NLP tasks. In Advances in Neural Information Processing Systems (NeurIPS), 2020. arXiv:2005.11401.
[17] Alexandra Henzinger, Emma Dauterman, Henry Corrigan-Gibbs, and Nickolai Zeldovich. Private web search with Tiptoe. In Proceedings of the 29th ACM Symposium on Operating Systems Principles (SOSP), pages 396–416, 2023. 15
[27] Chenqi Lin, Yubo Cui, Zhelei Zhou, Cheng Hong, Yufei Wang, Zhaohui Chen, and Meng Li. VeriRAG: Efficient zero-knowledge proofs for verifiable retrievalaugmented generation. Cryptology ePrint Archive, Paper 2026/637, https://eprint.iacr.org/2026/6 37, 2026.
[36] Pranav Rajpurkar, Jian Zhang, Konstantin Lopyrev, and Percy Liang. SQuAD: 100,000+ questions for machine comprehension of text. In Proceedings of the 2016 Conference on Empirical Methods in Natural Language Processing, EMNLP 2016, pages 2383–2392. The Association for Computational Linguistics, 2016.
[28] Hidde Lycklama, Alexander Viand, Nikolay Avramov, Nicolas Küchler, and Anwar Hithnawi. Artemis: Efficient commit-and-prove SNARKs for zkML. arXiv preprint arXiv:2409.12055, https://arxiv.org/ab s/2409.12055, 2024.
[37] Deevashwer Rathee, Jean-Luc Watson, Zirui Neil Zhao, G. Edward Suh, and Raluca Ada Popa. Onyx: Costefficient disk-oblivious ANN search. arXiv preprint arXiv:2604.20401, https://arxiv.org/abs/2604.2 0401, 2026.
[29] Yu A. Malkov and Dmitry A. Yashunin. Efficient and robust approximate nearest neighbor search using hierarchical navigable small world graphs. IEEE Transactions on Pattern Analysis and Machine Intelligence, 42(4):824–836, 2020.
[38] Josef Sivic and Andrew Zisserman. Video Google: A text retrieval approach to object matching in videos. In Proceedings of the 9th IEEE International Conference on Computer Vision (ICCV), pages 1470–1477, 2003.
[30] Microsoft. Inconsistent and hallucinatory responses from Copilot studio agent. Microsoft Q&A forum post, https://learn.microsoft.com/en-us/answers/ questions/5654951/inconsistent-and-halluci natory-responses-from-copi, 2025.
[39] Snowflake. Cortex search. https://docs.snowflake .com/en/user-guide/snowflake-cortex/cortex -search/cortex-search-overview, 2025. Accessed: 2026-06-09.
[31] Alex Ozdemir, Fraser Brown, and Riad S. Wahby. CirC: Compiler infrastructure for proof systems, software verification, and more. In 2022 IEEE Symposium on Security and Privacy (SP), pages 2248–2266. IEEE, 2022.
[40] Haochen Sun, Jason Li, and Hongyang Zhang. zkLLM: Zero knowledge proofs for large language models. In Proceedings of the 2024 ACM SIGSAC Conference on Computer and Communications Security (CCS), pages 4405–4419, 2024.
[32] Fabio Petroni, Aleksandra Piktus, Angela Fan, Patrick S. H. Lewis, Majid Yazdani, Nicola De Cao, James Thorne, Yacine Jernite, Vladimir Karpukhin, Jean Maillard, Vassilis Plachouras, Tim Rocktäschel, and Sebastian Riedel. KILT: a benchmark for knowledge intensive language tasks. In Proceedings of the 2021 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, NAACL-HLT 2021, pages 2523–2544. Association for Computational Linguistics, 2021.
[41] Sureel. Sureel: Protection, control & monetization for creators, media rights owners & AI companies. https: //www.sureel.ai, 2026. Accessed: 2026-06-09. [42] U.S. Congress. S.5339 — Platform Accountability and Transparency Act, 117th Congress (2021–2022). https: //www.congress.gov/bill/117th-congress/se nate-bill/5339, 2022. Sponsor: Sen. Christopher A. Coons. Accessed: 2026-06-09.
[33] ProRata.ai. ProRata.AI: AI-powered search, advertising, and attribution. https://prorata.ai/, 2026. Accessed: 2026-06-09.
[43] An Yang, Baosong Yang, Binyuan Hui, et al. Qwen2 technical report. CoRR, abs/2407.10671, 2024.
[34] Zipeng Qiu, Wenjie Qu, Jiaheng Zhang, and Binhang Yuan. V3DB: Audit-on-demand zero-knowledge proofs for verifiable vector search over committed snapshots. arXiv preprint arXiv:2603.03065, https://arxiv.or g/abs/2603.03065, 2026.
[44] Jinhao Zhu, Liana Patel, Matei Zaharia, and Raluca Ada Popa. Compass: Encrypted semantic search with high accuracy. In 19th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 915– 938. USENIX Association, 2025.
[35] Wenjie Qu, Yijun Sun, Xuanming Liu, Tao Lu, Yanpei Guo, Kai Chen, and Jiaheng Zhang. zkGPT: An efficient non-interactive zero-knowledge proof framework for LLM inference. In 34th USENIX Security Symposium (USENIX Security 25), pages 2045–2063. USENIX Association, 2025.
[45] Wei Zou, Runpeng Geng, Binghui Wang, and Jinyuan Jia. PoisonedRAG: Knowledge corruption attacks to retrieval-augmented generation of large language models. In 34th USENIX Security Symposium (USENIX Security 25), pages 3827–3844. USENIX Association, 2025. 16
A
Extended Background Material
3. Sum equality. ∑x∈H B(x) = ∑x∈K A(x), verified via a univariate sumcheck. The sumcheck quotient QC costs O(n log n).
Log-Derivative Reduction. Verifying the product relation of §2.2 is expensive, particularly when the table is large. Haböck [15] observed that taking the logarithmic derivative d of both sides (i.e. applying dX log(·)) converts the product of linear factors into a sum of their reciprocals. The product equality holds if and only if the resulting sums are equal. By the Schwartz–Zippel lemma, equality of the two sums reduces
B B.1
to their equality at a random challenge γ ← − F: j
N−1 m(ω ) 1 ∑ γ + f (ωi ) = ∑ γ + t(ωK j ) H i=0 j=0 K
(3)
where m(X) is the polynomial over K encoding the multiplicities. This reduction from a product to a sum is the basis of the cq lookup argument [8]. The cq Protocol. cq [8] is a lookup argument designed for tables far larger than the query. It precomputes the table-side sum of the log-derivative identity, and its per-query proving cost therefore scales with the size of the query side alone. Concretely, cq realizes the log-derivative check (3) as a polynomial protocol over KZG commitments [23].
i.e., each layer contributes a labeled copy of its edges, and drop-down edges connect every node to its copy one layer below. Then the single invocation of greedy search S EARCH -L AYER′1 (Gupper , q, {(ep, L)}) terminates at (v∗1 , 0). The total number of traversal steps taken by S EARCH -L AYER′ is Tg = ∑Lℓ=1 Tℓ∗ + L.
Preprocessing. During setup, KZG commitments to the Lagrange basis polynomials {LKj (X)}N−1 j=0 over K are computed. j
For each table entry t(ωK ), a cached quotient q j (X) is derived from LKj (X) and t(X) such that QA (defined below) can later be expressed as a linear combination of the q j . KZG commitments to the q j are computed and stored. This costs O(N log N) and depends only on the table.
Proof. By downward induction on ℓ. At layer ℓ ≥ 1, the neighbors of the current node (v, ℓ) in Gupper are its intra-layer neighbors and the drop-down (v, ℓ−1). Since (v, ℓ) and (v, ℓ−1) share the same embedding, d((v, ℓ−1), q) = d((v, ℓ), q), so under the lexicographic comparison of S EARCH -L AYER′ the drop-down cannot be the greedy choice while any strictly closer intra-layer neighbor exists. S EARCH -L AYER′ therefore reproduces S EARCH -L AYER1 (Gℓ , q, ·) step by step until reaching the local minimum v∗ℓ , taking exactly Tℓ∗ steps. At that point all intra-layer neighbors have distance ≥ d(v∗ℓ , q), and since ties are broken in favor of the lower layer, the drop-down is the greedy choice and the walk descends to (v∗ℓ , ℓ−1). Repeating at each layer down to ℓ = 1, the walk reaches (v∗1 , 0), which has no outgoing edges, so the search terminates there. In total, the walk takes Tℓ∗ intra-layer steps at each layer plus one drop-down per layer, giving Tg = ∑Lℓ=1 Tℓ∗ + L steps.
Proving. The prover constructs two rational functions encoding each side of (3): K j · L j (X) . j j=0 γ + t(ωK )
n−1
LiH (X) , i i=0 γ + f (ωH )
B(X) = ∑
Equivalence of the Unified Greedy Search
Theorem 4 (Equivalence of Gupper ). Let G be a multi-layer graph with layers G0 , G1 , . . . , GL , each a graph Gℓ with vertex set V (Gℓ ) and edge set E(Gℓ ), let q ∈ Rd be a query, and let ep be an entry point in GL . Let v∗1 be the result of the greedy search of the HNSW algorithm as in lines 1–4 of Algorithm 1, and let Tℓ∗ denote the number of greedy steps taken at layer ℓ. Define Gupper = (Vupper , Eupper ) by Vupper = (v, ℓ) : ℓ ∈ [L], v ∈ V (Gℓ ) ∪ (v, 0) : v ∈ V (G1 ) , Eupper = ((u, ℓ), (w, ℓ)) : ℓ ∈ [L], (u, w) ∈ E(Gℓ ) ∪ ((v, ℓ), (v, ℓ−1)) : ℓ ∈ [L], v ∈ V (Gℓ ) ,
$
n−1
Equivalence Proofs
N−1 m
A(X) = ∑
The prover commits to m(X) = ∑ j m j LKj (X), the multiplicity polynomial. Since only n of the N multiplicities are nonzero, the commitment is computed as a sparse linear combination of the preprocessed Lagrange basis commitments in O(n) scalar multiplications. The prover also commits to B(X), computed over H in O(n log n). The protocol verifies three polynomial identities:
B.2
1. Well-formedness of B. B(X)(γ + f (X)) − 1 = QB (X) · ZH (X), ensuring B(ωiH ) = γ+ f 1(ωi ) for all i. The quotient
Proof of Lemma 1
Proof. Let T = topef (W ∪ A) and let Wfinal denote W after all insertions. If |W ∪A| ≤ ef , no eviction occurs and Wfinal = W ∪ A = T . Otherwise, eviction occurs when an insertion brings |W | to ef + 1 and removes the furthest element. Any e ∈ T has at most ef − 1 elements closer to q in all of W ∪ A, so among the ef +1 elements in W at the moment of eviction, at least one is further than e, and e is never the one removed. Therefore T ⊆ Wfinal , and as |Wfinal | = ef = |T |, Wfinal = T .
H
QB costs O(n log n). 2. Well-formedness of A. A(X)(γ +t(X))−m(X) = QA (X)· mj j ZK (X), ensuring A(ωK ) = j for all j. The commitγ+t(ωK )
ment to QA is computed as a sparse linear combination of the preprocessed cached quotient commitments in O(n) [8]. 17
B.3
Proof of Lemma 2
C
Committing the embedding and edge tables is a one-time cost per index. Figure 4 reports the preprocessing time per committed polynomial, the generation of one column’s cached quotients, across domain sizes from 215 to 227 , accelerated on the H100 GPU through icicle [18]. The cost grows nearlinearly with the domain size, at roughly ten microseconds per table entry. For the evaluated datasets, one polynomial costs 9.6 seconds on the million-node SIFT1M and GIST1M, 167 seconds for BIGANN-10M and Deep10M, and 716 and 1411 seconds for BIGANN-50M and BIGANN-100M, whose tables fit within the 220 , 224 , 226 , and 227 domains. The RAG corpora of §6.3, chunked at 256 tokens, span ∼20k chunks for SQuAD, ∼250k for TriviaQA-Val, ∼2M for TriviaQATrain, and ∼30M for KILT-NQ, which fit within the 215 , 218 , 221 , and 225 domains. At these sizes, a committed polynomial costs 0.33 seconds for SQuAD, 2.4 seconds for TriviaQAVal, 19.6 seconds for TriviaQA-Train, and 339 seconds for KILT-NQ.
Proof. At t = 0, W0 = C0 = {ep} in both executions. At each subsequent step, Wt agrees by Lemma 1, so the same neighbors are processed and the same nodes enter both C and W . Let Ct ,Ct′ denote the candidate sets in the two executions. Ct △Ct′ consists of nodes that were admitted into W temporarily and then evicted, so for any e ∈ Ct △Ct′ , d(e, q) > maxw∈Wt d(w, q), and e triggers termination at line 6 before being extracted, leaving the same node to be extracted at line 3 in both executions.
B.4
Proof of Theorem 3
Proof sketch. We show that the selected node and the state of W agree at every iteration across both algorithms. By Lemma 2, the sequence of selected nodes in S EARCH -L AYER is invariant under insertion order. Phase 2 reproduces this sequence: the selection rule arg min{di : pi = 0} picks the same node that S EARCH -L AYER would extract from C (line 3), and the batched merge produces the same W as sequential insertion by Lemma 1. Since the selected node and W agree at every iteration, the final output is identical. Once every candidate in W is processed, S EARCH -L AYER’s next extracted node is further than W ’s furthest element and the search terminates, while Phase 2 finds no unprocessed candidate and leaves W unchanged, so any budget Tb ≥ T ∗ yields the same final set.
BIGANN-50M KILT-NQ BIGANN-10M, Deep10M
Per-polynomial setup [s]
103 102 101 100
BIGANN-100M
TQA-Train SIFT1M, GIST1M TQA-Val SQuAD
215
217
219
221
223
Evaluation domain size
225
Preprocessing
227
Figure 4: One-time cq preprocessing per committed polynomial across evaluation domain sizes N, measured on the H100, with the evaluated datasets marked at their domains. The dashed line is 10−5 · N seconds. 18