{"id":"7238c987-0c09-4c6b-ab1c-4fbaabd6e85a","arxiv_id":"2505.17623","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Range-Arithmetic verifies outsourced DNN inference by checking matrix multiplication with sum-check and handling fixed-point rounding and ReLU with Bulletproofs range proofs, achieving logarithmic communication and quadratic verifier work.","lead":"Range-Arithmetic is a protocol that lets a verifier check a neural network inference run by an untrusted party, using only logarithmic communication. It handles fixed-point rounding and ReLU activation directly in finite-field arithmetic, which earlier approaches required expensive Boolean or high-degree encodings for.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The matrix-multiplication sum-check cannot be instantiated as written: Algorithm 1 Step 6 passes m-length generators to Algorithm 5, whose polynomial-commitment final evaluation needs nm- and mk-length generators for the MLE commitments, so the protocol aborts before rounding or ReLU.","rationale":"The paper's headline contribution is an end-to-end protocol for verifiable DNN inference with fixed-point rounding and ReLU. The arithmetic verification layer (Algorithm 1, Steps 6-8) is the foundation on which the rounding and ReLU extensions are built. If that layer cannot be instantiated from the published pseudocode, the central claim is not reproducible. My trace shows a concrete dimension mismatch: Algorithm 5 is presented as a generic routine with g,h ∈ G^{2^v}, but the calls it makes to Algorithm 3 require lengths determined by the full MLE coefficient vectors of the two operands (nm and mk), not by the sum-check variable count (log m). Since the paper provides no alternative mechanism for the verifier to evaluate ã(r1,·) or b(·,r2) from PA/PB with only m-length generators, the protocol as written cannot be executed. The reader's identified concern (the Algorithm 1 Step 11 / Algorithm 6 interface mismatch) is a real bug in the same spirit, but it concerns the rounding layer; the generator-length mismatch occurs earlier and affects even the plain matrix multiplication verification. I therefore regard it as the single most load-bearing issue. The fixes are localized (pass correctly sized generator prefixes and specify the range-proof bit-widths), so the appropriate verdict remains conditional acceptance, matching the reader's assessment, pending correction of the pseudocode.","tokens_in":19253,"tokens_out":32604,"duration_ms":307394,"concrete_test":"Set n=m=k=2 and run Algorithm 1 Step 6 exactly as written, passing g[:2] and h[:2] to Algorithm 5. In Algorithm 5 Step 13, Algorithm 3 must compute the Lagrange vector b of length 4 for evaluation point (r1,r); since h[:2] has only two generators, the operation P=P1×h^b is undefined and the protocol aborts. Re-running with g[:4],h[:4] allows the evaluation to complete. This single trace distinguishes a fixable typo from a fundamental design error; if the authors' implementation uses full-length generators, the pseudocode must still be corrected to make the claimed protocol reproducible.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Algorithm 1 Step 6 invokes Algorithm 5 with generator vectors g[:m] and h[:m], but Algorithm 5's final evaluation (Steps 13-14) uses Algorithm 3 to evaluate f^(1)(y1,·)=ã(r1,·) and f^(2)(·,y2)=b(·,r2) from the commitments PA and PB. Those commitments are to the full multilinear extensions, with nm and mk coefficients respectively (Section 3.1.1, Step 5 note). Algorithm 3 requires g,h ∈ G^{2^v}, where 2^v is the coefficient count of the polynomial evaluated (Section 2.3); evaluating ã(r1,r) therefore needs generator vectors of length nm, and evaluating b(r,r2) needs length mk. With g[:m] of length m, the Lagrange basis vector in Algorithm 3 Step 1 has length nm, while Algorithm 2's inner-product argument is only defined for vectors of length m, so the final check cannot be executed. This breaks the matrix-multiplication sum-check before any rounding or ReLU is introduced, and it undermines the claimed O(log n) communication and O(n^2) verifier work for the arithmetic layer. The same dimension mismatch appears in Algorithm 8, where Algorithm 6 is called with G^{nk} generators but no per-element bit-length is specified, and in Algorithm 1 Step 11, where the vector passed to Algorithm 6 (C+2^{s-1}) does not match the commitment (E+2^{s-1}).","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes Range-Arithmetic, a framework for verifiable deep-learning inference in which an untrusted prover convinces a verifier of the correctness of fixed-point matrix multiplication with rounding and of ReLU activations. The core idea is to verify arithmetic layers with a sum-check protocol over matrix products and to verify the non-arithmetic rounding and ReLU steps with aggregated range proofs, thereby avoiding Boolean encodings, high-degree polynomials, and large lookup tables. The paper claims O(n^3) prover work, O(n^2) verifier work, and O(log n) communication for n x n matrix multiplication with rounding, while also supporting ReLU. Experimental results on matrix multiplication and an MNIST case study are reported. The paper includes a standalone theorem (Theorem 3.1) characterizing fixed-point rounding by a congruence and two range conditions, with an appendix proof.","tokens_in":19528,"tokens_out":11805,"duration_ms":78908,"significance":"If the proposed protocol were correct and complete, it would be a useful contribution to verifiable ML: replacing Boolean-circuit encodings of rounding and ReLU with arithmetic range proofs is a natural and potentially practical idea. The rounding theorem itself is cleanly stated and proven, and the sum-check reduction for matrix products is standard. The manuscript, however, does not contain a formal completeness or soundness proof for the full composed protocol, and several concrete composition errors mean the protocol, as written, cannot be instantiated. The central algorithmic claim therefore currently rests on an incorrect or underspecified description rather than on a verified construction. With Major revisions that fix the generator dimensions, the range-proof interfaces, and the bit-length parameters, the underlying approach could be salvageable.","major_comments":[{"comment":"The matrix-multiplication sum-check cannot be instantiated with the generator vectors supplied. Algorithm 1 Step 6 invokes Algorithm 5 with g[:m] and h[:m], but Algorithm 5's final steps call Algorithm 3 to evaluate f^(1) = ã(r1, ·) and f^(2) = b̃(·, r2) from the commitments PA and PB, which are commitments to the full multilinear extensions of A and B with nm and mk coefficients. Algorithm 3 requires g, h ∈ G^{2^v} where 2^v is the coefficient count of the polynomial being evaluated (Section 2.3), so evaluating ã(r1, ·) requires generator vectors of length nm and evaluating b̃(·, r2) requires length mk. With g[:m] of length m, the inner-product argument in Algorithm 2 is undefined for the longer Lagrange basis vectors, and the protocol aborts before any rounding or ReLU step. This is a load-bearing error: the claimed O(log n) communication and O(n^2) verifier work for the arithmetic layer are not established by the described algorithms.","section":"Section 3.1.3, Algorithm 1 Step 6; Algorithm 5 Steps 13-14; Section 2.3"},{"comment":"The range-proof calls pass a public vector that does not match the commitment. In Step 11, the commitment argument is PC / P_{C'}^{2^s} × g^{2^{s-1}}, which binds to E + 2^{s-1} where E = C - 2^s C', but the stated vector is C + 2^{s-1}; thus the range proof would not prove the intended bound -2^{s-1} ≤ e_i < 2^{s-1}. In Step 12, the commitment binds to C' + 2^{t+1} (via PC' × g^{2^{t+1}}), but the stated vector is C + 2^{t+1}; even after correcting this typo to C' + 2^{t+1}, the bit-length is wrong: the condition -2^{t+1} ≤ c'_i < 2^{t+1} is equivalent to 0 ≤ c'_i + 2^{t+1} < 2^{t+2}, so the range proof needs bit-length t+2, not t+1. These inconsistencies mean the rounding verification as written does not actually verify the stated bounds.","section":"Section 3.1.3, Algorithm 1 Steps 11-12"},{"comment":"The ReLU range proof is not instantiable as described. Algorithm 8 Step 3 calls Algorithm 6 with generators g, h ∈ G^{nk} and the vector Y, but Algorithm 6 requires a bit-length parameter n such that each claimed element v_j is in [0, 2^n - 1]. No bit-length is specified, and the statement 'all elements of Y are positive' is undefined for arbitrary finite-field elements; a range proof can only certify bounds on integer representatives. Since the fixed-point format (s, t) is not given as an input to Algorithm 8, the prover and verifier cannot agree on the range that must be proven. This gap affects the soundness of the ReLU verification.","section":"Section 3.2, Algorithm 8 Step 3; Section 2.5"},{"comment":"The aggregated range proof is internally inconsistent and under-specified. The interface states P = g^{v_{[:m]}} with g ∈ G^{mn}, but Step 8 runs the inner-product argument on (g[:m], h[:m], u, P × P', q(z), v, z^m), which requires P to be a commitment to v using the first m generators, while Step 12 uses the full g and h'. Furthermore, the construction omits blinding factors that are essential in the Bulletproofs protocol it cites, and the notation g^{v_{[:m]}} is ambiguous when g has mn entries and v has m entries. Because the composed scheme's soundness depends on this sub-protocol, the paper must provide a precise and correct instantiation of the range proof, not merely cite Bulletproofs.","section":"Section 2.5 and Algorithm 6"}],"minor_comments":[{"comment":"The vector in the input tuple should read C' + 2^{t+1}, not C + 2^{t+1}, for the commitment to match.","section":"Algorithm 1 Step 12"},{"comment":"The check 'gi-1(ri-1)' references an undefined object; it should presumably be f_{i-1}(r_{i-1}) = f_i(0) + f_i(1), and the notation should be made consistent with Algorithm 4.","section":"Algorithm 5 Step 7"},{"comment":"The arguments of the identity-matrix MLE \tilde I are written as (x, s) in Equation (5) and (s, x) in Equation (6); the ordering should be fixed and consistently defined, especially since Algorithm 7 Step 15 evaluates \tilde I(s_1, ..., s_v, r_1, ..., r_v).","section":"Section 3.2, Equations (5)-(6)"},{"comment":"The axis labels in Figure 2 contain garbled Unicode fragments (e.g., '/uni00000019/uni0000000f/uni0000001b'), which must be repaired for the figure to be legible.","section":"Figure 2"},{"comment":"The experimental section reports times but does not report proof sizes, and it does not compare against the analytic complexity table in Table 1; stating that 'communication overhead grows logarithmically' in Figure 4 would be more convincing if the proof-size values were given.","section":"Section 4"}],"recommendation":"major_revision","confidential_remarks":"The paper has a potentially useful idea, but the protocol description is not executable as written, and the composability of the sum-check and range-proof layers is broken by generator-dimension mismatches. I believe the issues are fixable in a revised manuscript, but the revision must include a complete, consistent specification of Algorithm 5's use of polynomial commitments, a corrected Algorithm 1 with matching public vectors and bit-lengths, and a properly parameterized Algorithm 6/8 for the ReLU range proofs. A formal soundness statement for the full protocol should also be added."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nRead the Range-Arithmetic paper. Bottom line: the core idea is real and worth refereeing, but the protocol as written is not instantiable. The dimension mismatch in the polynomial commitment calls is a load-bearing flaw.\n\nWhat is new: the rounding verification via splitting into a rounded value and an error term, each range-proven, and the ReLU check via a^2 = y^2 plus a non-negativity range proof, are original constructions. The rounding theorem (Thm 3.1) is proved correctly. If the protocol can be fixed, the complexity claims—O(n^3) prover, O(n^2) verifier, O(log n) communication—would be a clear advance over prior ZKML work.\n\nWhere the paper breaks: Algorithm 1 Step 6 passes g[:m], h[:m] to Algorithm 5, but Algorithm 5's final evaluation step calls Algorithm 3 to evaluate the full MLEs of A and B, which have nm and mk coefficients. Algorithm 3 needs 2^v generators for a v-variate polynomial; with m-length generators, the inner-product argument in Algorithm 2 is only defined for vectors of length m, so the final check cannot be executed. The matrix multiplication proof aborts before rounding or ReLU is even considered. The same class of bug appears in Step 11, where the range-proof vector is C+2^{s-1} but the commitment is to E+2^{s-1}, and in Algorithm 8, where the bit-length for the non-negativity range proof is unspecified.\n\nThese are spec bugs, not conceptual ones. The framework is plausible; a careful rewrite with consistent generator lengths and matching vectors/commitments could fix it. But as is, the claims cannot be verified from the text. The experiments also compare to a single non-ReLU baseline, so the headline performance claims are not fully supported.\n\nWho should read it: ZKML and verifiable-computing researchers, especially those working on fixed-point and activation verification. The paper deserves a serious referee, but the referee should be asked to check the protocol instantiation line by line; I'd expect a major revision or reject before the claims can be trusted.\n\nRecommendation: send to peer review, but flag the generator/vector mismatches as blocking. If the authors supply a corrected protocol (and ideally a full worked example), it could be a useful contribution.","headline":"Genuinely new fusion of sum-check and range proofs for rounding/ReLU, but the protocol as written has blocking dimension mismatches in the polynomial commitment calls.","tokens_in":20112,"tokens_out":5540,"would_cite":false,"duration_ms":39157,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"By rewriting rounding and ReLU as interval-checked arithmetic, this paper establishes that outsourced DNN inference can be verified with O(log n) communication and O(n^2) verifier work.","keywords":["verifiable computing","sum-check protocol","range proof","fixed-point arithmetic","ReLU activation","outsourced inference","interactive proofs","deep learning verification"],"falsifier":"Run the main verification protocol with the range-proof step wired as written in Algorithm 1: Step 11 calls Algorithm 6 with the public vector $C + 2^{s-1}$ while the commitment is to $E + 2^{s-1}$. Then attempt a cheating prover that chooses a wrong $C'$ but satisfies the range check on the public vector; if the verifier accepts, the rounding proof is unsound. A shorter direct check is to compare the input names in Algorithm 1 Step 11 against Algorithm 6's stated interface and see whether the committed value and the ranged vector coincide.","tokens_in":19019,"feed_emoji":"🔐","tokens_out":12086,"duration_ms":78391,"temperature":0.7,"pith_summary":"This paper is trying to establish that the two operations that make deep learning awkward to verify inside a proof system—rounding after fixed-point matrix multiplication, and the ReLU activation—can be checked with plain finite-field arithmetic. The trick is a bounded-decomposition characterization of rounding: a product entry $a$ is correctly rounded to $a'$ exactly when $a \\equiv e + 2^s a' \\pmod{p}$ with the discarded part $e$ in $[-2^{s-1}, 2^{s-1})$ and the rounded value in $[-2^{t+1}, 2^{t+1})$, and those interval conditions are enforced by an aggregated range proof. Arithmetic equality $C = AB$ is verified by a sum-check protocol, and the same range-proof tool, plus a second sum-check, takes care of ReLU. Because the construction stays inside finite fields, the authors claim it avoids Boolean circuit encodings, high-degree polynomials, and large lookup tables, while giving prover work $O(n^3)$, verifier work $O(n^2)$, and communication $O(\\log n)$ for $n \\times n$ matrix multiplication with rounding. A reader should care because if this holds, outsourced DNN inference becomes verifiable at a cost close to the cost of running the inference itself.","feed_headline":"Verifying rounded neural nets now needs O(log n) communication","feed_subtitle":"A sum-check-and-range-proof scheme checks fixed-point rounding and ReLU without Boolean circuits or lookup tables.","key_machinery":"The load-bearing object is an exact characterization of fixed-point rounding as two interval constraints on a field decomposition: $a \\equiv e + 2^s a' \\pmod{p}$ with $e \\in [-2^{s-1}, 2^{s-1})$ and $a' \\in [-2^{t+1}, 2^{t+1})$. This identity converts a non-arithmetic operation---truncation of low-order bits---into membership of two committed vectors in intervals, which is exactly what an aggregated range proof (Algorithm 6, built from an inner-product argument that gives logarithmic communication) can certify. The arithmetic layer is carried by the sum-check protocol (Algorithm 5) with polynomial commitments, which verifies $\\sum_{\\ell} \\tilde{a}(r_1, \\ell) \\tilde{b}(\\ell, r_2) = \\tilde{c}(r_1, r_2)$ at a random point; since the left side is a sum over a product of multilinear extensions, both factors can be evaluated from commitments. ReLU reuses the same range proof for nonnegativity of $Y = |A|$ and a second sum-check for the identity $\\tilde{a}^2(x) = \\tilde{y}^2(x)$ evaluated at a random point. The composition of these two tools---range proofs for interval membership and sum-check for arithmetic equality---is what carries the whole verifiable-inference argument.","core_discovery":"The central claim is that verifiable fixed-point DNN inference reduces to a bounded-decomposition identity plus two standard proof tools. For a fixed-point number with $s$ fractional bits, the paper shows that knowing a field element $a'$ and an error $e$ such that $a \\equiv e + 2^s a' \\pmod{p}$, with $-2^{s-1} \\le e < 2^{s-1}$ and $-2^{t+1} \\le a' < 2^{t+1}$, is equivalent to knowing that $a' = R(a)$, the fixed-point rounding of $a$. Matrix multiplication $C = AB$ is checked by a sum-check over the multilinear extensions of $A$, $B$, and $C$ at a random point, relying on the standard random-point polynomial identity lemma to make a single point check certify the whole product; the interval conditions on every entry of $E = C - 2^s C'$ and on $C'$ itself are then checked in aggregate by a range proof. ReLU is handled by committing to $Y = |A|$, proving all entries of $Y$ are nonnegative with the same range proof, and using a second sum-check to prove $a_i^2 = y_i^2$ entrywise, so that $B = (A+Y)/2$ must equal $\\mathrm{ReLU}(A)$. The paper claims these pieces compose layer by layer without preprocessing and give $O(n^3)$ prover cost, $O(n^2)$ verifier cost, and $O(\\log n)$ communication for $n \\times n$ rounded matrix multiplication, with ReLU support that prior sum-check-based methods lack.","pith_inferences":["If the soundness claims hold, the same bounded-decomposition trick should generalize to other piecewise-linear activations such as leaky ReLU or clipped ReLU by adding extra interval constraints, though the paper does not develop these cases.","The claimed costs assume the range-proof sub-protocol is instantiated on the value that the commitment actually binds; the paper never reconciles the mismatch between the vector named in Algorithm 1 Step 11 and the committed error vector, so a working implementation must settle that before the performance numbers are meaningful.","The protocol as presented is interactive, and converting it to a non-interactive proof would require care with how the sum-check challenges and range-proof challenges are generated; the paper only describes the interactive form.","Because verification costs per layer are $O(n^2)$, total verification cost for a deep network roughly follows the sum of the layer dimensions rather than the depth-weighted computation count, which is good news for deep but narrow networks."],"forward_implications":["Fixed-point matrix multiplication followed by rounding can be verified without Boolean circuits or large lookup tables, with communication $O(\\log n)$ and verifier work $O(n^2)$.","The same machinery verifies ReLU layers, so a multilayer network can be checked layer by layer, each layer's commitment feeding into the next.","The prover's cost stays a constant multiple of the cost of one matrix multiplication, so producing a proof is comparable in expense to running the inference once.","The protocol is compatible with finite-field-based proof systems and needs no preprocessing or R1CS-style sparse circuit encodings, per the paper.","In the reported MNIST case study with four fully connected layers and fixed-point arithmetic, the prover spends roughly 230 ms and the verifier roughly 154 ms, while communication grows only logarithmically with matrix size."],"supporting_citations":[{"why":"Supplies the inner-product argument and the aggregate range-proof structure that enforce the interval bounds on the rounding error and on ReLU outputs; without it the protocol would need linear communication.","marker":"[5]"},{"why":"The state-of-the-art integer-scaling method for fixed-point matrix multiplication that the paper takes as its baseline for complexity and runtime comparisons.","marker":"[7]"},{"why":"Provides the sum-check protocol and multilinear extension machinery used to verify the arithmetic equality C = AB at a random point.","marker":"[23]"},{"why":"Cited for the communication complexity of the sum-check protocol, which underlies the claimed O(log n) communication.","marker":"[2]"},{"why":"The polynomial identity lemma that gives soundness to checking polynomial equality at a random point; every sum-check-based check in the paper relies on it.","marker":"[22]"}],"fun_headline_variants":["Range proofs check DNN rounding and ReLU in O(log n) comms","Verifiable deep learning without Boolean circuits or lookups","Sum-check and range proofs shrink verifier cost for DNNs","Untrusted inference now verifiable via range arithmetic","Fixed-point rounding and ReLU proven in log communication"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The soundness of the whole protocol rests on the range-proof step being applied to the same vector that the commitment argues about; if the rounding step passes one vector to the range proof while committing to another, the interval check no longer constrains the actual rounding error.","fun_headline_variants_meta":{"raw":{"variants":["Range proofs check DNN rounding and ReLU in O(log n) comms","Verifiable deep learning without Boolean circuits or lookups","Sum-check and range proofs shrink verifier cost for DNNs","Untrusted inference now verifiable via range arithmetic","Fixed-point rounding and ReLU proven in log communication"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000201,"raw_usage":{"total_tokens":1438,"prompt_tokens":1062,"completion_tokens":376,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":678,"completion_tokens_details":{"reasoning_tokens":292}},"tokens_in":678,"tokens_out":376,"duration_ms":3218,"temperature":1.0,"reasoning_tokens":292,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T14:44:35.957188+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the main verification protocol with the range-proof step wired as written in Algorithm 1: Step 11 calls Algorithm 6 with the public vector $C + 2^{s-1}$ while the commitment is to $E + 2^{s-1}$. Then attempt a cheating prover that chooses a wrong $C'$ but satisfies the range check on the public vector; if the verifier accepts, the rounding proof is unsound. A shorter direct check is to compare the input names in Algorithm 1 Step 11 against Algorithm 6's stated interface and see whether the committed value and the ranged vector coincide.","supporting_citations":[{"cited_title":"Bulletproofs: Short proofs for confidential transactions and more","cited_arxiv_id":null,"evidence_quote":"Supplies the inner-product argument and the aggregate range-proof structure that enforce the interval bounds on the rounding error and on ReLU outputs; without it the protocol would need linear communication."},{"cited_title":"More optimizations to sum-check proving","cited_arxiv_id":null,"evidence_quote":"The state-of-the-art integer-scaling method for fixed-point matrix multiplication that the paper takes as its baseline for complexity and runtime comparisons."},{"cited_title":"Proofs, arguments, and zero-knowledge","cited_arxiv_id":null,"evidence_quote":"Provides the sum-check protocol and multilinear extension machinery used to verify the arithmetic equality C = AB at a random point."},{"cited_title":"The sum-check protocol over fields of small characteristic","cited_arxiv_id":null,"evidence_quote":"Cited for the communication complexity of the sum-check protocol, which underlies the claimed O(log n) communication."},{"cited_title":"Fast probabilistic algorithms for verification of polynomial identities.Journal of the ACM (JACM), 27(4):701–717, 1980","cited_arxiv_id":null,"evidence_quote":"The polynomial identity lemma that gives soundness to checking polynomial equality at a random point; every sum-check-based check in the paper relies on it."}],"review_version":1}