Certified but Private: Scalable Zero-Knowledge Proofs for Neural Network Guarantees

# Certified but Private: Scalable Zero-Knowledge Proofs for Neural Network Guarantees
Source: [https://arxiv.org/html/2608.17070](https://arxiv.org/html/2608.17070)
###### Abstract

With the growing deployment of machine learning models, formal guarantees of the robustness and fairness of these models have become increasingly important in safety\-critical and legal\-compliance settings\. However, model parameters are often commercial secrets that cannot be disclosed to auditors or end users\. To this end, we present PANDA, a scalable system that uses zero\-knowledge proofs \(ZKPs\) to prove the robustness and fairness properties of a model without revealing its private parameters\. PANDA is built on top of CROWN, an efficient robustness certification framework that is used in many state\-of\-the\-art formal verification tools for neural networks\. The core contribution of PANDA is a novel algorithm for proving linear relaxation bounds for non\-linear activation layers, yielding simple, lightweight proofs\. Remarkably, our system can generate proofs of local robustness for neural networks with more than 2\.9M parameters in 5 minutes, and can verify them in 10 seconds\. Prior ZKP\-based robustness system rely on exponential\-time algorithms that cannot scale to nontrivial networks\. In contrast, PANDA scales polynomially in the number of neurons in a network, allowing us to support neural networks 4 orders of magnitude larger than previous approaches with significantly reduced prover overhead\.

## 1Introduction

A machine learning \(ML\) model is*robust*if small perturbations to its input do not cause large or unpredictable changes in its output\. As ML systems are increasingly deployed in safety\-critical settings such as healthcare, autonomous driving, and financial decision\-making, scalable methods for formally verifying robustness are becoming ever more important\. Beyond the model owners’ own interest in reliability, regulators and downstream customers are increasingly demanding formal robustness guarantees\[[15](https://arxiv.org/html/2608.17070#bib.bib22),[10](https://arxiv.org/html/2608.17070#bib.bib23)\]\. For example, a hospital may train a clinical model that predicts patient risk levels from reported symptoms\. A user deciding whether to deploy the model naturally requires assurance that the model is robust: small perturbations to a patient’s reported symptoms, such as a typo or synonym, should not change the patient’s predicted risk level\.

Formally, consider a classification model that takes as input a vector𝒙\\boldsymbol\{x\}, which may encode an image, and outputs a predicted label\. A standard notion oflocal robustnessrequires that, for a given input𝒙0\\boldsymbol\{x\}\_\{0\}, all sufficiently close \(with respect to a parameterε\\varepsilon\) inputs receive the same prediction\. This property can be formalized as:

∀𝒙\.‖𝒙−𝒙0‖<ε⇒Classification⁡\(𝒙\)=Classification⁡\(𝒙0\)\.\\forall\\boldsymbol\{x\}\.\\ \\\|\\boldsymbol\{x\}\-\\boldsymbol\{x\}\_\{0\}\\\|<\\varepsilon\\Rightarrow\\mathrm\{Classification\}\(\\boldsymbol\{x\}\)=\\mathrm\{Classification\}\(\\boldsymbol\{x\}\_\{0\}\)\.\(1\)
One approach to proving local robustness properties is to provide users or third\-party auditors with full access to the model parameters\. However, modern ML models constitute valuable intellectual property\. Networks are trained on proprietary datasets, and exposing model parameters can enable sophisticated white\-box attacks\[[20](https://arxiv.org/html/2608.17070#bib.bib27)\]and leak information about the training data\[[9](https://arxiv.org/html/2608.17070#bib.bib28)\]\. In the medical setting above, the hospital cannot disclose the model weights, as this may reveal protected health information about patients and violate HIPAA regulations\.

The tension between verifiability and model confidentiality can be resolved by usingzero\-knowledge proofs\(ZKPs\)\[[8](https://arxiv.org/html/2608.17070#bib.bib12)\], a cryptographic primitive that enables a prover to convince a verifier that a statement holds without revealing any information beyond the statement’s validity\. A growing line of work called zkML has used ZKPs to hide model parameters in ML\-related computation\[[22](https://arxiv.org/html/2608.17070#bib.bib16),[6](https://arxiv.org/html/2608.17070#bib.bib29)\]\. However, most of it has focused on privacy\-preserving ML inference and training integrity, leaving local robustness comparatively underexplored\. Existing work that considers the related notion of fairness\[[31](https://arxiv.org/html/2608.17070#bib.bib17)\]can only support models with≈\\approx100 parameters, far too small for real\-world applications\.

Recent developments in formal verification have enabled fast robustness certification of deep neural networks \(DNNs\), but these tools reveal information about the model\[[4](https://arxiv.org/html/2608.17070#bib.bib2),[7](https://arxiv.org/html/2608.17070#bib.bib1)\]\. A natural idea is to compose a robustness certification algorithm with a ZKP to hide model parameters and inherit the efficiency and scalability of the underlying algorithm\. However, this composition introduces several technical challenges: ZKPs natively operate with linear functions and must be adapted to handle non\-linear activation functions\. In addition, ZKPs are not typically compatible with floating\-point arithmetic\. Finally, performing computation within ZKPs introduces a significant overhead in the proving time, which can act as a barrier to scaling to large real\-world DNNs\. This leads us to the following problem statement:

Can we verify local robustness properties of large neural networks in zero\-knowledge?

We answer this question in the affirmative\. In this paper, we propose PANDA \(Proofs of Automated Neural\-network Derived Affine bounds\), a system that combines ZKPs with the CROWN verification algorithm\[[32](https://arxiv.org/html/2608.17070#bib.bib3)\]to produce publicly verifiable proofs of a neural network’s local robustness\. CROWN is an efficient linear bound propagation method that underlies many state\-of\-the\-art neural network verification systems\[[30](https://arxiv.org/html/2608.17070#bib.bib5),[29](https://arxiv.org/html/2608.17070#bib.bib4),[3](https://arxiv.org/html/2608.17070#bib.bib6)\]\. By integrating CROWN into a zero\-knowledge framework, PANDA enables model owners to certify robustness properties while keeping the underlying model parameters private\.

To the best of our knowledge, PANDA is the most efficient and scalable ZKP system for proving local robustness of private neural networks to date\. PANDA supports networks containing up to 2\.9 million parameters, exceeding the scale of prior approaches by more than 4 orders of magnitude, while requiring a proving time of 5 minutes and a verification time of 10 seconds\. Moreover, the prover runtime is polynomial in the number of neurons in the network, enabling practical certification for substantially larger models than previously possible\.

PANDA is also the first privacy\-preserving local robustness certification system to support DNNs with transcendental activation functions such as sigmoid and tanh\. We introduce a novel method for verifying linear relaxations of activation functions over continuous intervals by evaluating four pointwise inequalities, yielding a ZK\-friendly check\.

Technical highlights\. We propose acertification algorithmwhich enables verifying the correctness of computation without performing the entire computation trace within a ZKP, drastically improving the efficiency of PANDA\. In particular, the CROWN algorithm requires finding a pair of linear lower and upper bounds that sandwich the activation function over a given interval\. CROWN selects appropriate bounds through a costly iterative search\[[32](https://arxiv.org/html/2608.17070#bib.bib3)\]\. We observe that this search can be performed outside of the ZKP in order to reduce the prover overhead, and then the computed lower and upper bounds can be verified using a simple system of constraints, which we name theFour\-Point Relaxation Gadget\(Section[5](https://arxiv.org/html/2608.17070#S5)\)\. This principle is a through\-line of PANDA: the prover first performs the CROWN algorithm outside of a ZKP, and then certifies its results through a reduced system of constraints within the ZKP\.

Instead of using a general\-purpose ZKP backend, we design acustomized backendthat make use of different cryptographic primitives for proving different operations\. This enables PANDA to achieve greater prover efficiency than previous work and scale to larger networks\.

## 2Preliminaries

Azero\-knowledge proof\(ZKP\) allows a prover𝒫\\mathcal\{P\}to convince a verifier𝒱\\mathcal\{V\}that a public statementxxis true, without revealing any further information aboutwhyit is true\. Private information explaining the “why” is called the witnessww\. For instance, a public statementxxmay be that an ML model is locally robust at a given point, whereas the private witnesswwcontains the private model weights and auxiliary values produced in computation\.𝒫\\mathcal\{P\}usesxxandwwto outputs a proofπ\\pi, which𝒱\\mathcal\{V\}checks alongsidexxand either accepts or rejects\.

Acommit\-and\-proveZKP system enables𝒫\\mathcal\{P\}to first produce a commitmentcwc\_\{w\}to the witnesswwwhich ishiding\(cwc\_\{w\}reveals nothing aboutww\) andbinding\(𝒫\\mathcal\{P\}cannot find a different witnessw′≠ww^\{\\prime\}\\neq wcorresponding tocwc\_\{w\}\)\. The commitmentcwc\_\{w\}is part of the public statementxx, and𝒫\\mathcal\{P\}’s claim is that𝒫\\mathcal\{P\}knows a witnesswwwhose commitment iscwc\_\{w\}and thatwwis a valid witness forx\.x\.

PANDA is a commit\-and\-prove ZKP system which uses three underlying cryptographic primitives:

1. 1\.Apolynomial commitment scheme,Πcom\\Pi\_\{\\textsc\{com\}\}, which consists of three algorithms: - •Commit\(run by𝒫\\mathcal\{P\}\) takes as input a polynomialffand outputs a commitmentcfc\_\{f\}toffwhich ishidingandbinding\. - •Eval\(run by𝒫\\mathcal\{P\}\) takes as inputff, a pointxx, and a valueyy, and outputs a proofπ\\pi, also called anopening, claiming thaty=f⁡\(x\)y=f\(x\)\. - •Verify\(run by𝒱\\mathcal\{V\}\) takes as inputcf,x,y,π,c\_\{f\},x,y,\\pi,and either accepts or rejects\. Πcom\\Pi\_\{\\textsc\{com\}\}iscompleteifVerifyaccepts whenevercf←Commit​\(f\)c\_\{f\}\\leftarrow\\textsc\{Commit\}\(f\),y=f⁡\(x\)y=f\(x\), andπ←Eval​\(f,x,y\)\\pi\\leftarrow\\textsc\{Eval\}\(f,x,y\)\. We sayΠcom\\Pi\_\{\\textsc\{com\}\}isevaluation\-bindingif a malicious𝒫\\mathcal\{P\}cannot produce an accepting proofπ\\piforx,yx,yify≠f⁡\(x\)y\\neq f\(x\)\. We sayΠcom\\Pi\_\{\\textsc\{com\}\}iszero\-knowledgeifπ\\pireveals no information aboutf\.f\.
2. 2\.AZKP for matrix arithmetic,Πarith\\Pi\_\{\\textsc\{arith\}\}\. We can encode matrices or vectors as polynomials using interpolation and then useΠcom\\Pi\_\{\\textsc\{com\}\}for commitments to matrices or vectors\. - •The private witnesswwis a list of matrices \(e\.g\.,𝐀,𝐁,𝐂,𝐃\\mathbf\{A,B,C,D\}\)\. - •The public statementxxis a list of commitments to these matrices \(e\.g\.cA,cB,cC,cDc\_\{A\},c\_\{B\},c\_\{C\},c\_\{D\}\) and a claimed arithmetic relation between them \(e\.g\.𝐀=𝐁𝐂\+𝐃\\mathbf\{A=BC\+D\}\)\. - •𝒫\\mathcal\{P\}proves to𝒱\\mathcal\{V\}that𝒫\\mathcal\{P\}knows matrices inwwwhose commitments match those inxxand satisfy this matrix arithmetic equality\.
3. 3\.AZKP for table lookups,Πlookup\\Pi\_\{\\textsc\{lookup\}\}\(also known as alookup argument\)\. - •The private witnesswwis alookup vector𝒂\\boldsymbol\{a\}\.111We present a simplified abstract interface\. The concrete lookup arguments we use embed auxiliary information pertaining to𝒂\\boldsymbol\{a\}and𝒕\\boldsymbol\{t\}in the witnesswwwhich is committed and appended to the public statementxx\. - •The public statementxxis a commitmentcac\_\{a\}to𝒂\\boldsymbol\{a\}as well as atable vector𝒕\\boldsymbol\{t\}\. - •𝒫\\mathcal\{P\}proves to𝒱\\mathcal\{V\}that𝒫\\mathcal\{P\}knows a vector𝒂\\boldsymbol\{a\}whose commitment iscac\_\{a\}and such that each entry of𝒂\\boldsymbol\{a\}is in the table𝒕\\boldsymbol\{t\}\.

Πarith\\Pi\_\{\\textsc\{arith\}\}andΠlookup\\Pi\_\{\\textsc\{lookup\}\}each contain two algorithms:

- •Prove\(run by𝒫\\mathcal\{P\}\) takes as inputwwandxxand outputs a proofπ\\pi\. As a subroutine,𝒫\\mathcal\{P\}produces openings of masked versions of the witnesses viaΠcom\.Eval\\Pi\_\{\\textsc\{com\}\}\.\\textsc\{Eval\}\.
- •Verify\(run by𝒱\\mathcal\{V\}\) takes as inputxxandπ\\piand accepts or rejects\. As a subroutine,𝒱\\mathcal\{V\}callsΠcom\.Verify\\Pi\_\{\\textsc\{com\}\}\.\\textsc\{Verify\}to check the opening proofs \(which are contained inπ\\pi\)\.

We say that a ZKP iscompleteif, wheneverwwis a valid witness forxx,Verifyaccepts the proofπ\\pigenerated byProve\. A ZKP issoundif wheneverxxis an invalid statement, no computationally bounded prover can forge a proofπ\\pithat causesVerifyto accept\. A ZKP iszero\-knowledgeifπ\\pireveals no information aboutwwbeyond the fact thatwwexists\.

Πlookup\\Pi\_\{\\textsc\{lookup\}\}can be used forrange proofZKPs, which prove that each element of a vector𝒂\\boldsymbol\{a\}lies within an interval\[l,r\]\.\[l,r\]\.This is done simply by setting the table vector𝒕=\(l,l\+1,…,r\)\.\\boldsymbol\{t\}=\(l,l\+1,\\dots,r\)\.We often write one\-sided range proofs as𝒂≥0\\boldsymbol\{a\}\\geq 0, wherel=0l=0andrris chosen implicitly as the maximum attainable value of elements in𝒂\\boldsymbol\{a\}, dependent on the quantization\.

Πlookup\\Pi\_\{\\textsc\{lookup\}\}can also provenon\-linear function evaluations; that is, for a set of points\{\(xi,yi\)\}i∈\[n\]\\\{\(x\_\{i\},y\_\{i\}\)\\\}\_\{i\\in\[n\]\}and a non\-linear functionff,Πlookup\\Pi\_\{\\textsc\{lookup\}\}proves thatf⁡\(xi\)=yif\(x\_\{i\}\)=y\_\{i\}for eachi∈\[n\]i\\in\[n\]\. This is achieved by setting𝒂=\(\(xi,yi\)\)i∈\[n\]\\boldsymbol\{a\}=\\left\(\(x\_\{i\},y\_\{i\}\)\\right\)\_\{i\\in\[n\]\}and𝒕=\(\(z,f⁡\(z\)\)\)z\\boldsymbol\{t\}=\\left\(\(z,f\(z\)\)\\right\)\_\{z\}, wherezzranges over possible values in the domain\.

Quantization\. Most existing ZKPs are incompatible with floating\-point computation\. Following precedent in prior zkML papers\[[22](https://arxiv.org/html/2608.17070#bib.bib16),[6](https://arxiv.org/html/2608.17070#bib.bib29)\], we performquantizationto translate all computations to finite field arithmetic\. We follow the quantization approach introduced in\[[11](https://arxiv.org/html/2608.17070#bib.bib24)\], where we represent each real numberxxwith aQQ\-bit integerqx∈\[0,2Q\)q\_\{x\}\\in\[0,2^\{Q\}\)satisfyingx⋅Sx≈qxx\\cdot S\_\{x\}\\approx q\_\{x\}for an optimally chosen scaling factorSx≫1\.S\_\{x\}\\gg 1\.

Per\-layer matrices and tensors in the neural network typically share a single scaling factor, and model weights and biases are all initialized with it\. To sum two valuesxxandyy, we first rescale them to share the same scaling factor, then sum the quantized integersqxq\_\{x\}andqyq\_\{y\}\. To multiply two valuesxxandyy, we multiply the quantized integersqxq\_\{x\}andqyq\_\{y\}, and set the scaling factor of the product toSx​SyS\_\{x\}S\_\{y\}\. To rescaleqx≈x⋅Sxq\_\{x\}\\approx x\\cdot S\_\{x\}to some new scaling factorSzS\_\{z\}, we computeqz=⌊Sz​qx/Sx⌋\.q\_\{z\}=\\left\\lfloor S\_\{z\}q\_\{x\}/S\_\{x\}\\right\\rfloor\.

## 3CROWN Algorithm

In this section, we review the CROWN algorithm\[[32](https://arxiv.org/html/2608.17070#bib.bib3)\], a crucial building block for our PANDA zero\-knowledge protocol\. We present each step of the algorithm in a way that enables compatibility with ZKP systems\. The CROWN algorithm is provided in full detail in Appendix[A\.1](https://arxiv.org/html/2608.17070#A1.SS1)\.

### 3\.1Setting and Goal

We consider anmm\-layer feed\-forward networkf:ℝn0→ℝnmf:\\mathbb\{R\}^\{n\_\{0\}\}\\to\\mathbb\{R\}^\{n\_\{m\}\}defined by the recursion

𝒛\(k\)=𝐖\(k\)​𝒉\(k−1\)\+𝒃\(k\)∈ℝnk,𝒉\(k\)=σ⁡\(𝒛\(k\)\)∈ℝnk\\boldsymbol\{z\}^\{\(k\)\}=\\mathbf\{W\}^\{\(k\)\}\\boldsymbol\{h\}^\{\(k\-1\)\}\+\\boldsymbol\{b\}^\{\(k\)\}\\in\\mathbb\{R\}^\{n\_\{k\}\},\\qquad\\boldsymbol\{h\}^\{\(k\)\}=\\sigma\\\!\\left\(\\boldsymbol\{z\}^\{\(k\)\}\\right\)\\in\\mathbb\{R\}^\{n\_\{k\}\}\(2\)fork=1,…,mk=1,\\dots,m, with weight matrices𝐖\(k\)∈ℝnk×nk−1\\mathbf\{W\}^\{\(k\)\}\\in\\mathbb\{R\}^\{n\_\{k\}\\times n\_\{k\-1\}\}, biases𝒃\(k\)∈ℝnk\\boldsymbol\{b\}^\{\(k\)\}\\in\\mathbb\{R\}^\{n\_\{k\}\}, and a coordinate\-wise activation functionσ:ℝnk→ℝnk\\sigma:\\mathbb\{R\}^\{n\_\{k\}\}\\rightarrow\\mathbb\{R\}^\{n\_\{k\}\}for allkk\. The input is𝒉\(0\)=𝒙∈ℝn0\\boldsymbol\{h\}^\{\(0\)\}=\\boldsymbol\{x\}\\in\\mathbb\{R\}^\{n\_\{0\}\}and the output isf⁡\(𝒙\)=𝒛\(m\)∈ℝnm\.f\(\\boldsymbol\{x\}\)=\\boldsymbol\{z\}^\{\(m\)\}\\in\\mathbb\{R\}^\{n\_\{m\}\}\.Theℓth\\ell^\{\\mathrm\{th\}\}layer hasnℓn\_\{\\ell\}neurons, and the output neurons on input𝒙0\\boldsymbol\{x\}\_\{0\}are denotedfc​\(𝒙0\)f\_\{c\}\(\\boldsymbol\{x\}\_\{0\}\)forc∈\{1,…,nm\}\.c\\in\\\{1,\\dots,n\_\{m\}\\\}\.For a classification model, the choice ofccwhich maximizesfc​\(𝒙0\)f\_\{c\}\(\\boldsymbol\{x\}\_\{0\}\)is the*predicted class*of𝒙0\.\\boldsymbol\{x\}\_\{0\}\.

Given an input𝒙0\\boldsymbol\{x\}\_\{0\}, anℓ∞\\ell^\{\\infty\}\-perturbation radiusε\\varepsilon, and a predicted classccof𝒙0\\boldsymbol\{x\}\_\{0\}, the network is*locally robust*at𝒙0\\boldsymbol\{x\}\_\{0\}with respect to a targeted attack classt≠ct\\neq cif

ft​\(𝒙\)≤fc​\(𝒙\),∀𝒙∈𝔹⁡\(𝒙0,ε\),f\_\{t\}\(\\boldsymbol\{x\}\)\\leq f\_\{c\}\(\\boldsymbol\{x\}\),\\qquad\\forall\\boldsymbol\{x\}\\in\\mathbb\{B\}\(\\boldsymbol\{x\}\_\{0\},\\varepsilon\),\(3\)where𝔹⁡\(𝒙0,ε\):=\{𝒙:‖𝒙−𝒙0‖∞≤ε\}\\mathbb\{B\}\(\\boldsymbol\{x\}\_\{0\},\\varepsilon\):=\\\{\\boldsymbol\{x\}:\\\|\\boldsymbol\{x\}\-\\boldsymbol\{x\}\_\{0\}\\\|\_\{\\infty\}\\leq\\varepsilon\\\}\. Such a claim is a special case of the general statement

𝐂⋅f⁡\(𝒙\)≤𝒖,∀𝒙∈𝔹⁡\(𝒙0,ε\),\\mathbf\{C\}\\cdot f\(\\boldsymbol\{x\}\)\\leq\\boldsymbol\{u\},\\qquad\\forall\\boldsymbol\{x\}\\in\\mathbb\{B\}\(\\boldsymbol\{x\}\_\{0\},\\varepsilon\),\(4\)where𝐂∈ℝN×nm,𝒖∈ℝN\\mathbf\{C\}\\in\\mathbb\{R\}^\{N\\times n\_\{m\}\},\\boldsymbol\{u\}\\in\\mathbb\{R\}^\{N\}, obtained by settingN=1,𝒖=0N=1,\\boldsymbol\{u\}=0, and𝐂=𝒆t⊤−𝒆c⊤\\mathbf\{C\}=\\boldsymbol\{e\}\_\{t\}^\{\\top\}\-\\boldsymbol\{e\}\_\{c\}^\{\\top\}, where𝒆i\\boldsymbol\{e\}\_\{i\}is theithi^\{\\mathrm\{th\}\}basis vector\.

Goal of the algorithm\. CROWN certifies statements of the form \([4](https://arxiv.org/html/2608.17070#S3.E4)\) by running an algorithm which computes a vector𝒖′\\boldsymbol\{u\}^\{\\prime\}such that𝐂⋅f⁡\(𝒙\)≤𝒖′\\mathbf\{C\}\\cdot f\(\\boldsymbol\{x\}\)\\leq\\boldsymbol\{u\}^\{\\prime\}, and then ultimately checking that𝒖′≤𝒖\\boldsymbol\{u\}^\{\\prime\}\\leq\\boldsymbol\{u\}entry\-wise\. Crucially, this algorithm computes*linear bounds*on the pre\-activation vector𝒛\(k\)\\boldsymbol\{z\}^\{\(k\)\}for each layerkkas a function of the input𝒙\\boldsymbol\{x\}:

𝐀¯\(k\)​𝒙\+𝒅¯\(k\)≤𝒛\(k\)≤𝐀¯\(k\)​𝒙\+𝒅¯\(k\),∀𝒙∈𝔹⁡\(𝒙0,ε\),\\underline\{\\mathbf\{A\}\}^\{\(k\)\}\\boldsymbol\{x\}\+\\boldsymbol\{\\underline\{d\}\}^\{\(k\)\}\\;\\leq\\;\\boldsymbol\{z\}^\{\(k\)\}\\;\\leq\\;\\overline\{\\mathbf\{A\}\}^\{\(k\)\}\\boldsymbol\{x\}\+\\boldsymbol\{\\overline\{d\}\}^\{\(k\)\},\\qquad\\forall\\boldsymbol\{x\}\\in\\mathbb\{B\}\(\\boldsymbol\{x\}\_\{0\},\\varepsilon\),\(5\)where𝐀¯\(k\),𝐀¯\(k\)∈ℝnk×n0\\underline\{\\mathbf\{A\}\}^\{\(k\)\},\\overline\{\\mathbf\{A\}\}^\{\(k\)\}\\in\\mathbb\{R\}^\{n\_\{k\}\\times n\_\{0\}\}and𝒅¯\(k\),𝒅¯\(k\)∈ℝnk\\boldsymbol\{\\underline\{d\}\}^\{\(k\)\},\\boldsymbol\{\\overline\{d\}\}^\{\(k\)\}\\in\\mathbb\{R\}^\{n\_\{k\}\}\. In the final layermm, CROWN constructs linear bounds on𝐂⋅𝒛\(m\)\\mathbf\{C\}\\cdot\\boldsymbol\{z\}^\{\(m\)\}rather than on𝒛\(m\)\\boldsymbol\{z\}^\{\(m\)\}\.

Outer forward pass, inner backward pass\. CROWN builds \([5](https://arxiv.org/html/2608.17070#S3.E5)\) layer by layer, passing forward fromk=1k=1tok=mk=m\. Computing the bounds at layerkk, however, requires abackward passfrom layerkkdown to the input, using the previously computed bounds for layersℓ<k\\ell<k\. Once this is completed, aconcretizationstep transforms \([5](https://arxiv.org/html/2608.17070#S3.E5)\) into scalar bounds used to derive𝒖′\.\\boldsymbol\{u\}^\{\\prime\}\.

### 3\.2Backward Pass

The backward pass for layerkkbegins with a set of concretized bounds\{𝑳\(ℓ\),𝑼\(ℓ\)\}ℓ<k\\\{\\boldsymbol\{L\}^\{\(\\ell\)\},\\boldsymbol\{U\}^\{\(\\ell\)\}\\\}\_\{\\ell<k\}for layersℓ<k\\ell<k, where each pre\-activation vector𝒛\(ℓ\)\\boldsymbol\{z\}^\{\(\\ell\)\}satisfies the entry\-wise inequality

𝑳\(ℓ\)≤𝒛\(ℓ\)≤𝑼\(ℓ\),∀𝒙∈𝔹⁡\(𝒙0,ε\)\.\\boldsymbol\{L\}^\{\(\\ell\)\}\\;\\leq\\;\\boldsymbol\{z\}^\{\(\\ell\)\}\\;\\leq\\;\\boldsymbol\{U\}^\{\(\\ell\)\},\\qquad\\forall\\boldsymbol\{x\}\\in\\mathbb\{B\}\(\\boldsymbol\{x\}\_\{0\},\\varepsilon\)\.\(6\)These are obtained by recursively calling CROWN for layersℓ=1,…,k−1\\ell=1,\\dots,k\-1\. The goal is to compute the linear bounds of \([5](https://arxiv.org/html/2608.17070#S3.E5)\) for layerkk\. We describe the upper bound case; the lower bound is symmetric\.

Activation relaxation\. A prerequisite is a pair of*linear relaxations*of the activationσ\\sigma\. For every layerℓ<k\\ell<k, CROWN supplies four vectors𝒂¯\(ℓ\),𝒃¯\(ℓ\),𝒂¯\(ℓ\),𝒃¯\(ℓ\)\\boldsymbol\{\\overline\{a\}\}^\{\(\\ell\)\},\\boldsymbol\{\\overline\{b\}\}^\{\(\\ell\)\},\\boldsymbol\{\\underline\{a\}\}^\{\(\\ell\)\},\\boldsymbol\{\\underline\{b\}\}^\{\(\\ell\)\}such that

𝒂¯\(ℓ\)​z\+𝒃¯\(ℓ\)≤σ⁡\(𝒛\(ℓ\)\)≤𝒂¯\(ℓ\)​z\+𝒃¯\(ℓ\),∀𝒛∈\[𝑳\(ℓ\),𝑼\(ℓ\)\]\.\\boldsymbol\{\\underline\{a\}\}^\{\(\\ell\)\}z\+\\boldsymbol\{\\underline\{b\}\}^\{\(\\ell\)\}\\;\\leq\\;\\sigma\(\\boldsymbol\{z\}^\{\(\\ell\)\}\)\\;\\leq\\;\\boldsymbol\{\\overline\{a\}\}^\{\(\\ell\)\}z\+\\boldsymbol\{\\overline\{b\}\}^\{\(\\ell\)\},\\qquad\\forall\\boldsymbol\{z\}\\in\[\\boldsymbol\{L\}^\{\(\\ell\)\},\\,\\boldsymbol\{U\}^\{\(\\ell\)\}\]\.\(7\)The linear relaxations are selected through an intricate procedure detailed in Appendix[A\.2](https://arxiv.org/html/2608.17070#A1.SS2)\.

Invariants\. The backward pass maintains and updates an*affine bound*\(𝐀,𝒅\)\(\\mathbf\{A\},\\boldsymbol\{d\}\)with𝐀∈ℝnk×nℓ\\mathbf\{A\}\\in\\mathbb\{R\}^\{n\_\{k\}\\times n\_\{\\ell\}\}and𝒅∈ℝnk\\boldsymbol\{d\}\\in\\mathbb\{R\}^\{n\_\{k\}\}\. At each depthℓ\\ellfromkkdown to00, the bound satisfies one of two invariants:

Invariant​ℐh\(ℓ\):\\displaystyle\\text\{Invariant \}\\;\\mathcal\{I\}\_\{h\}^\{\(\\ell\)\}\\,:\\quad𝒛\(k\)≤𝐀​𝒉\(ℓ\)\+𝒅,\\displaystyle\\boldsymbol\{z\}^\{\(k\)\}\\;\\leq\\;\\mathbf\{A\}\\,\\boldsymbol\{h\}^\{\(\\ell\)\}\+\\boldsymbol\{d\},\(8\)Invariant​ℐz\(ℓ\):\\displaystyle\\text\{Invariant \}\\;\\mathcal\{I\}\_\{z\}^\{\(\\ell\)\}\\,:\\quad𝒛\(k\)≤𝐀​𝒛\(ℓ\)\+𝒅,\\displaystyle\\boldsymbol\{z\}^\{\(k\)\}\\;\\leq\\;\\mathbf\{A\}\\,\\boldsymbol\{z\}^\{\(\\ell\)\}\+\\boldsymbol\{d\},\(9\)where the inequality is entry\-wise and the bound holds for all𝒙∈𝔹⁡\(𝒙0,ε\)\\boldsymbol\{x\}\\in\\mathbb\{B\}\(\\boldsymbol\{x\}\_\{0\},\\varepsilon\)\. The recursion starts atℐh\(k−1\)\\mathcal\{I\}\_\{h\}^\{\(k\-1\)\}, ends with \([5](https://arxiv.org/html/2608.17070#S3.E5)\) atℐh\(0\),\\mathcal\{I\}\_\{h\}^\{\(0\)\},and alternates between the two invariants as follows:

- •Step 1 at depthℓ\\elltransformsℐh\(ℓ\)⇒ℐz\(ℓ\)\\mathcal\{I\}\_\{h\}^\{\(\\ell\)\}\\Rightarrow\\mathcal\{I\}\_\{z\}^\{\(\\ell\)\}by linear relaxation through the activation\.
- •Step 2 at depthℓ\\elltransformsℐz\(ℓ\)⇒ℐh\(ℓ−1\)\\mathcal\{I\}\_\{z\}^\{\(\\ell\)\}\\Rightarrow\\mathcal\{I\}\_\{h\}^\{\(\\ell\-1\)\}by substitution through the linear map\.

Initialization\.𝒛\(k\)=𝐖\(k\)​𝒉\(k−1\)\+𝒃\(k\)\\boldsymbol\{z\}^\{\(k\)\}=\\mathbf\{W\}^\{\(k\)\}\\boldsymbol\{h\}^\{\(k\-1\)\}\+\\boldsymbol\{b\}^\{\(k\)\}establishesℐh\(k−1\)\\mathcal\{I\}\_\{h\}^\{\(k\-1\)\}by setting𝐀←𝐖\(k\)\\mathbf\{A\}\\leftarrow\\mathbf\{W\}^\{\(k\)\}and𝒅←𝒃\(k\)\.\\boldsymbol\{d\}\\leftarrow\\boldsymbol\{b\}^\{\(k\)\}\.

Step 1:ℐh\(ℓ\)⇒ℐz\(ℓ\)\\mathcal\{I\}\_\{h\}^\{\(\\ell\)\}\\Rightarrow\\mathcal\{I\}\_\{z\}^\{\(\\ell\)\}\. We substitute𝒉\(ℓ\)=σ⁡\(𝒛\(ℓ\)\)\\boldsymbol\{h\}^\{\(\\ell\)\}=\\sigma\(\\boldsymbol\{z\}^\{\(\\ell\)\}\)into \([8](https://arxiv.org/html/2608.17070#S3.E8)\) and apply the linear relaxation \([7](https://arxiv.org/html/2608.17070#S3.E7)\)\. Each entry of𝐀\\mathbf\{A\}uses the upper relaxation\(a¯i\(ℓ\),b¯i\(ℓ\)\)\(\\overline\{a\}^\{\(\\ell\)\}\_\{i\},\\overline\{b\}^\{\(\\ell\)\}\_\{i\}\)when positive and the lower relaxation\(a¯i\(ℓ\),b¯i\(ℓ\)\)\(\\underline\{a\}^\{\(\\ell\)\}\_\{i\},\\underline\{b\}^\{\(\\ell\)\}\_\{i\}\)when negative, since multiplying by a negative number flips the inequality\. Splitting𝐀\\mathbf\{A\}into

𝐀\+=max⁡\(𝐀,0\),𝐀−=min⁡\(𝐀,0\)\\mathbf\{A\}\_\{\+\}=\\max\(\\mathbf\{A\},0\),\\qquad\\mathbf\{A\}\_\{\-\}=\\min\(\\mathbf\{A\},0\)\(10\)yields the following update:

𝒅←𝒅\+𝐀\+​𝒃¯\(ℓ\)\+𝐀−​𝒃¯\(ℓ\),𝐀←𝐀\+​diag​\(𝒂¯\(ℓ\)\)\+𝐀−​diag​\(𝒂¯\(ℓ\)\)\\boldsymbol\{d\}\\leftarrow\\boldsymbol\{d\}\+\\mathbf\{A\}\_\{\+\}\\boldsymbol\{\\overline\{b\}\}^\{\(\\ell\)\}\+\\mathbf\{A\}\_\{\-\}\\boldsymbol\{\\underline\{b\}\}^\{\(\\ell\)\},\\qquad\\mathbf\{A\}\\leftarrow\\mathbf\{A\}\_\{\+\}\\mathrm\{diag\}\(\\boldsymbol\{\\overline\{a\}\}^\{\(\\ell\)\}\)\+\\mathbf\{A\}\_\{\-\}\\mathrm\{diag\}\(\\boldsymbol\{\\underline\{a\}\}^\{\(\\ell\)\}\)\(11\)wherediag⁡\(𝒗\)\\mathrm\{diag\}\(\\boldsymbol\{v\}\)denotes the diagonal matrix with entries of the vector𝒗\\boldsymbol\{v\}on its diagonal\. After the update,\(𝐀,𝒅\)\(\\mathbf\{A\},\\boldsymbol\{d\}\)satisfiesℐz\(ℓ\)\\mathcal\{I\}\_\{z\}^\{\(\\ell\)\}\.

Step 2:ℐz\(ℓ\)⇒ℐh\(ℓ−1\)\\mathcal\{I\}\_\{z\}^\{\(\\ell\)\}\\Rightarrow\\mathcal\{I\}\_\{h\}^\{\(\\ell\-1\)\}\. We substitute𝒛\(ℓ\)=𝐖\(ℓ\)​𝒉\(ℓ−1\)\+𝒃\(ℓ\)\\boldsymbol\{z\}^\{\(\\ell\)\}=\\mathbf\{W\}^\{\(\\ell\)\}\\boldsymbol\{h\}^\{\(\\ell\-1\)\}\+\\boldsymbol\{b\}^\{\(\\ell\)\}, so

𝒅←𝒅\+𝐀​𝒃\(ℓ\),𝐀←𝐀𝐖\(ℓ\)\.\\boldsymbol\{d\}\\leftarrow\\boldsymbol\{d\}\+\\mathbf\{A\}\\boldsymbol\{b\}^\{\(\\ell\)\},\\qquad\\mathbf\{A\}\\leftarrow\\mathbf\{A\}\\mathbf\{W\}^\{\(\\ell\)\}\.\(12\)The affine bound\(𝐀,𝒅\)\(\\mathbf\{A\},\\boldsymbol\{d\}\)has advanced one level and now satisfiesℐh\(ℓ−1\)\\mathcal\{I\}\_\{h\}^\{\(\\ell\-1\)\}\.

Termination\. Iterating down toℓ=1\\ell=1producesℐh\(0\)\\mathcal\{I\}\_\{h\}^\{\(0\)\}, which is exactly equation \([5](https://arxiv.org/html/2608.17070#S3.E5)\) since𝒉\(0\)=𝒙\\boldsymbol\{h\}^\{\(0\)\}=\\boldsymbol\{x\}\. We finally retrieve𝐀¯\(k\)←𝐀\\overline\{\\mathbf\{A\}\}^\{\(k\)\}\\leftarrow\\mathbf\{A\}and𝒅¯\(k\)←𝒅\\boldsymbol\{\\overline\{d\}\}^\{\(k\)\}\\leftarrow\\boldsymbol\{d\}\.

Final layer\. In the final layerk=mk=m, the backward pass must be modified in order to support the claim𝐂​f​\(𝒙\)≤𝒖\\mathbf\{C\}f\(\\boldsymbol\{x\}\)\\leq\\boldsymbol\{u\}\. Notably, invariantsℐh\(ℓ\)\\mathcal\{I\}\_\{h\}^\{\(\\ell\)\}andℐz\(ℓ\)\\mathcal\{I\}\_\{z\}^\{\(\\ell\)\}replace the left\-hand side𝒛\(m\)\\boldsymbol\{z\}^\{\(m\)\}with𝐂​𝒛\(m\)\\mathbf\{C\}\\boldsymbol\{z\}^\{\(m\)\}\. The initialization step is given by𝐀←𝐂⋅𝐖\(m\)\\mathbf\{A\}\\leftarrow\\mathbf\{C\}\\cdot\\mathbf\{W\}^\{\(m\)\}and𝒅←𝐂⋅𝒃\(m\)\\boldsymbol\{d\}\\leftarrow\\mathbf\{C\}\\cdot\\boldsymbol\{b\}^\{\(m\)\}\. Steps 1 and 2 in the backward pass remain the same, and the final concretization yields the desired claim\.

### 3\.3Concretization

Once the backward pass is complete for layerkk, concretization yields the vectors𝑳\(k\),𝑼\(k\)∈ℝnk\\boldsymbol\{L\}^\{\(k\)\},\\boldsymbol\{U\}^\{\(k\)\}\\in\\mathbb\{R\}^\{n\_\{k\}\}by maximizing and minimizing the affine bounds of \([5](https://arxiv.org/html/2608.17070#S3.E5)\) over𝒙∈𝔹⁡\(𝒙0,ε\)\\boldsymbol\{x\}\\in\\mathbb\{B\}\(\\boldsymbol\{x\}\_\{0\},\\varepsilon\)\. The upper bound𝑼\(k\)\\boldsymbol\{U\}^\{\(k\)\}\(and symmetrically the lower bound𝑳\(k\)\\boldsymbol\{L\}^\{\(k\)\}\) is derived as

𝑼\(k\)=max𝒙∈𝔹⁡\(𝒙0,ε\)⁡\(𝐀¯\(k\)​𝒙\+𝒅¯\(k\)\)=𝐀¯\+\(k\)​\(𝒙0\+ε​𝟏\)\+𝐀¯−\(k\)​\(𝒙0−ε​𝟏\)\+𝒅¯\(k\),\\boldsymbol\{U\}^\{\(k\)\}=\\max\_\{\\boldsymbol\{x\}\\in\\mathbb\{B\}\(\\boldsymbol\{x\}\_\{0\},\\varepsilon\)\}\\left\(\\overline\{\\mathbf\{A\}\}^\{\(k\)\}\\boldsymbol\{x\}\+\\boldsymbol\{\\overline\{d\}\}^\{\(k\)\}\\right\)=\\overline\{\\mathbf\{A\}\}^\{\(k\)\}\_\{\+\}\(\\boldsymbol\{x\}\_\{0\}\+\\varepsilon\\mathbf\{1\}\)\+\\overline\{\\mathbf\{A\}\}^\{\(k\)\}\_\{\-\}\(\\boldsymbol\{x\}\_\{0\}\-\\varepsilon\\mathbf\{1\}\)\+\\boldsymbol\{\\overline\{d\}\}^\{\(k\)\},\(13\)where𝟏∈ℝn0\\mathbf\{1\}\\in\\mathbb\{R\}^\{n\_\{0\}\}is the all\-ones vector and

𝐀¯\+\(k\)=max⁡\(𝐀¯\(k\),0\),𝐀¯−\(k\)=min⁡\(𝐀¯\(k\),0\)\.\\overline\{\\mathbf\{A\}\}^\{\(k\)\}\_\{\+\}=\\max\(\\overline\{\\mathbf\{A\}\}^\{\(k\)\},0\),\\qquad\\overline\{\\mathbf\{A\}\}^\{\(k\)\}\_\{\-\}=\\min\(\\overline\{\\mathbf\{A\}\}^\{\(k\)\},0\)\.\(14\)

## 4PANDA Framework

This section presents PANDA, our commit\-and\-prove ZKP for certifying local robustness of neural networks\. We describe the steps used by𝒫\\mathcal\{P\}to convince𝒱\\mathcal\{V\}of a local robustness claim in zero knowledge\. The PANDA algorithm is provided in full detail with pseudocode in Appendix[B](https://arxiv.org/html/2608.17070#A2)\.

Setup\.𝒫\\mathcal\{P\}and𝒱\\mathcal\{V\}agree on the input point𝒙0∈ℝn0\\boldsymbol\{x\}\_\{0\}\\in\\mathbb\{R\}^\{n\_\{0\}\}, the perturbation boundε\\varepsilon, the model architecture, and a public matrix𝐂\\mathbf\{C\}and vector𝒖\\boldsymbol\{u\}which define the local robustness claim of \([4](https://arxiv.org/html/2608.17070#S3.E4)\),

∀𝒙∈𝔹⁡\(𝒙0,ε\),𝐂​f​\(𝒙\)≤𝒖\.\\forall\\boldsymbol\{x\}\\in\\mathbb\{B\}\(\\boldsymbol\{x\}\_\{0\},\\varepsilon\),\\qquad\\mathbf\{C\}f\(\\boldsymbol\{x\}\)\\leq\\boldsymbol\{u\}\.
Initial pass\.𝒫\\mathcal\{P\}runs quantized CROWN on input\(𝒙0,ε\)\(\\boldsymbol\{x\}\_\{0\},\\varepsilon\), producing atranscriptfor each layerkk:

1. \(a\)linear bounds𝐀¯\(k\),𝐀¯\(k\),𝒅¯\(k\),𝒅¯\(k\)\\underline\{\\mathbf\{A\}\}^\{\(k\)\},\\overline\{\\mathbf\{A\}\}^\{\(k\)\},\\boldsymbol\{\\underline\{d\}\}^\{\(k\)\},\\boldsymbol\{\\overline\{d\}\}^\{\(k\)\}of \([5](https://arxiv.org/html/2608.17070#S3.E5)\),
2. \(b\)all intermediate states\(𝐀,𝒅\)\(\\mathbf\{A\},\\boldsymbol\{d\}\)derived in the backward pass of \([8](https://arxiv.org/html/2608.17070#S3.E8)\) and \([9](https://arxiv.org/html/2608.17070#S3.E9)\),
3. \(c\)signed component matrices from equations \([11](https://arxiv.org/html/2608.17070#S3.E11)\) and \([13](https://arxiv.org/html/2608.17070#S3.E13)\),
4. \(d\)concretized scalar bounds𝑳\(k\)\\boldsymbol\{L\}^\{\(k\)\}and𝑼\(k\)\\boldsymbol\{U\}^\{\(k\)\}of \([13](https://arxiv.org/html/2608.17070#S3.E13)\),
5. \(e\)per\-neuron linear relaxation coefficients𝒂¯\(k\),𝒃¯\(k\),𝒂¯\(k\),𝒃¯\(k\)\\boldsymbol\{\\overline\{a\}\}^\{\(k\)\},\\boldsymbol\{\\overline\{b\}\}^\{\(k\)\},\\boldsymbol\{\\underline\{a\}\}^\{\(k\)\},\\boldsymbol\{\\underline\{b\}\}^\{\(k\)\}of \([7](https://arxiv.org/html/2608.17070#S3.E7)\), and
6. \(f\)quantization scaling factorsSxS\_\{x\}for each valuexxin the transcript\.

Commit\.𝒫\\mathcal\{P\}callsΠcom\.Commit\\Pi\_\{\\textsc\{com\}\}\.\\textsc\{Commit\}to commit to the model parameters and all quantities in the CROWN transcript\.

Prove\. The ZKP private witnesswwcontains the model parameters\{𝐖\(k\),𝒃\(k\)\}k=1m\\\{\\mathbf\{W\}^\{\(k\)\},\\boldsymbol\{b\}^\{\(k\)\}\\\}\_\{k=1\}^\{m\}and the CROWN transcript\. The public statementxxcontains all commitments to the witness values together with the robustness claim\(𝒙0,ε,𝐂,𝒖\)\(\\boldsymbol\{x\}\_\{0\},\\varepsilon,\\mathbf\{C\},\\boldsymbol\{u\}\)and the model architecture\.

For each operation performed in the initial pass of quantized CROWN,𝒫\\mathcal\{P\}produces a proofπ\\piusing one of two underlying ZKPs:Πarith\\Pi\_\{\\textsc\{arith\}\}for matrix arithmetic andΠlookup\\Pi\_\{\\textsc\{lookup\}\}for table lookups\.

- •Πarith\\Pi\_\{\\textsc\{arith\}\}is used for𝒫\\mathcal\{P\}to prove correctness of equations \([8](https://arxiv.org/html/2608.17070#S3.E8)\),\([9](https://arxiv.org/html/2608.17070#S3.E9)\),\([11](https://arxiv.org/html/2608.17070#S3.E11)\),\([12](https://arxiv.org/html/2608.17070#S3.E12)\), and \([13](https://arxiv.org/html/2608.17070#S3.E13)\),
- •Πlookup\\Pi\_\{\\textsc\{lookup\}\}is used for𝒫\\mathcal\{P\}to prove correctness of equations \([10](https://arxiv.org/html/2608.17070#S3.E10)\) and \([14](https://arxiv.org/html/2608.17070#S3.E14)\)\.

Proof of activation relaxations\. Existing primitivesΠarith\\Pi\_\{\\textsc\{arith\}\}andΠlookup\\Pi\_\{\\textsc\{lookup\}\}are insufficient to prove equation \([7](https://arxiv.org/html/2608.17070#S3.E7)\)\. In particular,𝒫\\mathcal\{P\}must prove at each neuron that its committed scalarsa¯,b¯,a¯,b¯\\overline\{a\},\\overline\{b\},\\underline\{a\},\\underline\{b\}satisfy

a¯​z\+b¯≤σ⁡\(z\)≤a¯​z\+b¯\\underline\{a\}z\+\\underline\{b\}\\leq\\sigma\(z\)\\leq\\overline\{a\}z\+\\overline\{b\}over areal\-valued interval\[l,u\]\[l,u\]\. While pointwise checks are feasible usingΠlookup\\Pi\_\{\\textsc\{lookup\}\}, such checks do not provide soundness guarantees between points\. We therefore create a novel component to prove such equations, theFour\-Point Relaxation Gadget, which is the subject of Section[5](https://arxiv.org/html/2608.17070#S5)\.

Proof of rescaling\. All quantization operations must also be associated with proofs so that𝒱\\mathcal\{V\}can check𝒫\\mathcal\{P\}does not deviate from the protocol\. As discussed in Section[2](https://arxiv.org/html/2608.17070#S2), a valuexxis represented asqx≈x⋅Sxq\_\{x\}\\approx x\\cdot S\_\{x\}whereqxq\_\{x\}is the quantized integer andSxS\_\{x\}is a scaling factor, also an integer\. Rescaling to a new scaling factorSzS\_\{z\}requires computingqz=⌊Sz​qx/Sx⌋q\_\{z\}=\\left\\lfloor S\_\{z\}q\_\{x\}/S\_\{x\}\\right\\rfloor\.𝒫\\mathcal\{P\}retains the remainderr∈\[0,Sx\)r\\in\[0,S\_\{x\}\)of the rounding operation as an auxiliary witness, and proves that0≤r<Sx0\\leq r<S\_\{x\}usingΠlookup\\Pi\_\{\\textsc\{lookup\}\}\. Finally,𝒫\\mathcal\{P\}proves the identity

Sz⋅qx=Sx⋅qz\+rS\_\{z\}\\cdot q\_\{x\}=S\_\{x\}\\cdot q\_\{z\}\+r\(15\)usingΠarith\\Pi\_\{\\textsc\{arith\}\}, which asserts the correctness of the rounding operation\.

Full protocol\. The pseudocode of the PANDA algorithm is provided in Appendix[B](https://arxiv.org/html/2608.17070#A2)\. The completeness, soundness, and zero\-knowledge properties of PANDA follow directly from the respective properties of the underlying primitivesΠcom,Πarith\\Pi\_\{\\textsc\{com\}\},\\Pi\_\{\\textsc\{arith\}\}, andΠlookup\\Pi\_\{\\textsc\{lookup\}\}\.

Asymptotic runtime\. The runtime of CROWN and PANDA are both polynomial in the number of neurons in the network\. For anmm\-layer neural network withnnneurons per layer, CROWN runs in timeO⁡\(m2​n3\)O\(m^\{2\}n^\{3\}\)\(see Appendix[A](https://arxiv.org/html/2608.17070#A1)\)\. PANDA inherits the same runtime, since we can instantiate the protocol with ZKP systems and a commitment scheme that require linear prover time\. This enables PANDA to scale to significantly larger neural networks than prior works\.

## 5The Four\-Point Relaxation Gadget

A core challenge in converting CROWN to a ZKP system is verifying that per\-neuron linear relaxations in \([7](https://arxiv.org/html/2608.17070#S3.E7)\) are valid over a real interval\. Our construction is designed such that𝒱\\mathcal\{V\}can check pointwise inequalities at onlyfour pointsin order to determine the validity of a linear relaxation\. Throughout this section, we focus on a single neuron with pre\-activation boundsl≤ul\\leq uand fix an activation functionσ\.\\sigma\.

###### Definition 5\.1\(Linear relaxation of an activation function\)\.

A linear relaxation forσ\\sigmaover an interval\[l,u\]\[l,u\]is a pair of affine functions

hL​\(z\)=a¯​z\+b¯,hU​\(z\)=a¯​z\+b¯,h\_\{L\}\(z\)=\\underline\{a\}z\+\\underline\{b\},\\qquad h\_\{U\}\(z\)=\\overline\{a\}z\+\\overline\{b\},\(16\)satisfying

hL​\(z\)≤σ⁡\(z\)≤hU​\(z\),∀z∈\[l,u\]\.h\_\{L\}\(z\)\\;\\leq\\;\\sigma\(z\)\\;\\leq\\;h\_\{U\}\(z\),\\qquad\\forall z\\in\[l,u\]\.\(17\)

![Refer to caption](https://arxiv.org/html/2608.17070v1/figs/relu_relaxation.png)

![Refer to caption](https://arxiv.org/html/2608.17070v1/figs/tanh_relaxation.png)

Figure 1:Linear relaxations of the ReLU \(left\) andtanh\\tanh\(right\) activation functions over the interval\[l,u\]\[l,u\]\(shaded\)\. Each activationσ⁡\(z\)\\sigma\(z\)\(black\) is bounded by affine functionshU​\(z\)h\_\{U\}\(z\)\(dashed green\) andhL​\(z\)h\_\{L\}\(z\)\(dashed red\) over the interval\[l,u\]\[l,u\]\.Figure[1](https://arxiv.org/html/2608.17070#S5.F1)depicts examples of linear relaxations of the ReLU andtanh\\tanhfunctions\.

We design a system such that𝒱\\mathcal\{V\}can verify whether \([17](https://arxiv.org/html/2608.17070#S5.E17)\) holds by checking only a constant number of pointwise inequalities\. Observe that verifying \([17](https://arxiv.org/html/2608.17070#S5.E17)\) over all possiblez∈\[l,u\]z\\in\[l,u\]is impossible \(there are infinitely many suchzz\), whereas checking \([17](https://arxiv.org/html/2608.17070#S5.E17)\) at finitely many sample points does not guarantee that the equation holds between these sample points\.

In Section[5\.1](https://arxiv.org/html/2608.17070#S5.SS1), we focus on S\-shaped activation functions such as sigmoid\(σ⁡\(x\)=exex\+1\)\\left\(\\sigma\(x\)=\\frac\{e^\{x\}\}\{e^\{x\}\+1\}\\right\), tanh\(σ⁡\(x\)=ex−e−xex\+e−x\)\\left\(\\sigma\(x\)=\\frac\{e^\{x\}\-e^\{\-x\}\}\{e^\{x\}\+e^\{\-x\}\}\\right\), and arctan\(σ⁡\(x\)=tan−1⁡\(x\)\)\\left\(\\sigma\(x\)=\\tan^\{\-1\}\(x\)\\right\), which arise naturally in ML applications\. In Section[5\.2](https://arxiv.org/html/2608.17070#S5.SS2), we focus on ReLU activations\(σ⁡\(x\)=max⁡\(0,x\)\)\\left\(\\sigma\(x\)=\\max\(0,x\)\\right\)\.

### 5\.1S\-shaped Activations

We first focus on S\-shaped activations and we show that linear relaxation validity reduces to checks at onlyfourpoints per neuron, independent of interval width\.

###### Assumption 5\.1\(S\-shaped activation\)\.

σ:ℝ→ℝ\\sigma:\\mathbb\{R\}\\to\\mathbb\{R\}isC1C^\{1\}, monotone increasing, bounded, and has a single inflection point atz=0z=0\.

Sigmoid, tanh, and arctan satisfy Assumption[5\.1](https://arxiv.org/html/2608.17070#S5.Thmassumption1)\. The assumption implies thatσ\\sigmais convex on\(−∞,0\]\(\-\\infty,0\]and concave on\[0,∞\)\[0,\\infty\), and that the derivativeσ′\\sigma^\{\\prime\}has a finite maximumB∈ℝB\\in\\mathbb\{R\}, attained atz=0z=0\. It suffices to consider linear relaxation slopesa¯,a¯∈\(0,B\]\\underline\{a\},\\overline\{a\}\\in\(0,B\]\.

###### Lemma 5\.1\.

Letσ\\sigmasatisfy Assumption[5\.1](https://arxiv.org/html/2608.17070#S5.Thmassumption1)\. For anyα∈\(0,B\]\\alpha\\in\(0,B\], there exist two tangency pointsz1≤0≤z2z\_\{1\}\\leq 0\\leq z\_\{2\}such thatσ′​\(z1\)=σ′​\(z2\)=α\\sigma^\{\\prime\}\(z\_\{1\}\)=\\sigma^\{\\prime\}\(z\_\{2\}\)=\\alpha\. Moreover, these points are distinct ifα<B\\alpha<B, and they coincide atz1=z2=0z\_\{1\}=z\_\{2\}=0ifα=B\\alpha=B\.

See proof in Appendix[G](https://arxiv.org/html/2608.17070#A7)\. We refer to the classical Interior Extremum Theorem from calculus in order to provide a simple set of criteria for the validity of candidate linear relaxations\. The proof of the lemma below follows directly from applying this theorem tohU​\(z\)−σ​\(z\)\.h\_\{U\}\(z\)\-\\sigma\(z\)\.

###### Lemma 5\.2\(Four\-point soundness\)\.

Letσ\\sigmasatisfy Assumption[5\.1](https://arxiv.org/html/2608.17070#S5.Thmassumption1), and fix an interval\[l,u\]⊆ℝ\[l,u\]\\subseteq\\mathbb\{R\}\. The upper boundhU​\(z\)=a¯​z\+b¯h\_\{U\}\(z\)=\\overline\{a\}z\+\\overline\{b\}witha¯\>0\\overline\{a\}\>0satisfiesσ⁡\(z\)≤hU​\(z\)\\sigma\(z\)\\leq h\_\{U\}\(z\)for allz∈\[l,u\]z\\in\[l,u\]if and only if

1. \(i\)*Endpoints:*σ⁡\(l\)≤hU​\(l\)\\sigma\(l\)\\leq h\_\{U\}\(l\)andσ⁡\(u\)≤hU​\(u\)\\sigma\(u\)\\leq h\_\{U\}\(u\);
2. \(ii\)*Tangency points:*for everyz∈\[l,u\]z\\in\[l,u\]withσ′​\(z\)=a¯\\sigma^\{\\prime\}\(z\)=\\overline\{a\},σ⁡\(z\)≤hU​\(z\)\\sigma\(z\)\\leq h\_\{U\}\(z\)\.

The dual statement holds for the lower bound with the inequality directions reversed\.

By Lemma[5\.1](https://arxiv.org/html/2608.17070#S5.Thmlemma1),σ′\\sigma^\{\\prime\}has at most two preimages ofa¯\\overline\{a\}, so it suffices to verify the values ofσ\\sigmaandhUh\_\{U\}at no more than four points: the two endpointsl,ul,uand the two tangency pointsz1,z2z\_\{1\},z\_\{2\}\.

The case\-work obstacle\. Encoding Lemma[5\.2](https://arxiv.org/html/2608.17070#S5.Thmlemma2)directly into a ZKP requires case\-work at each tangency pointziz\_\{i\}fori∈\{1,2\}i\\in\\\{1,2\\\}: there must be a range proof asserting that either \(a\)zi≤lz\_\{i\}\\leq l, \(b\)zi≥uz\_\{i\}\\geq u, or \(c\)σ⁡\(zi\)≤hU​\(zi\)\\sigma\(z\_\{i\}\)\\leq h\_\{U\}\(z\_\{i\}\)\. Declaring which case holds for eachziz\_\{i\}, however, leaks information aboutllanduu, which are themselves derived from the private model parameters\. We therefore replace Lemma[5\.2](https://arxiv.org/html/2608.17070#S5.Thmlemma2)with a*case\-free*, sufficient \(but not necessary\) set of criteria for determining whetherhUh\_\{U\}andhLh\_\{L\}are a valid linear relaxation over the interval\[l,u\]\.\[l,u\]\.

###### Theorem 5\.1\(Case\-free four\-point soundness\)\.

Letσ\\sigmasatisfy Assumption[5\.1](https://arxiv.org/html/2608.17070#S5.Thmassumption1)and fix an interval\[l,u\]⊆ℝ\[l,u\]\\subseteq\\mathbb\{R\}\. Letz1≤0≤z2z\_\{1\}\\leq 0\\leq z\_\{2\}be the \(possibly coinciding\) tangency points satisfyingσ′​\(z1\)=σ′​\(z2\)=a¯\\sigma^\{\\prime\}\(z\_\{1\}\)=\\sigma^\{\\prime\}\(z\_\{2\}\)=\\overline\{a\}\. The upper boundhUh\_\{U\}is valid on\[l,u\]\[l,u\]if each of the following criteria is satisfied\.

- \(i\)*Endpoints:*σ⁡\(l\)≤hU​\(l\)\\sigma\(l\)\\leq h\_\{U\}\(l\)andσ⁡\(u\)≤hU​\(u\)\\sigma\(u\)\\leq h\_\{U\}\(u\);
- \(ii\)*Left tangency:*σ⁡\(z1\)≤hU​\(z1\)\\sigma\(z\_\{1\}\)\\leq h\_\{U\}\(z\_\{1\}\);
- \(iii\)*Right tangency:*0≤\(u−z2\)​\(hU​\(z2\)−σ⁡\(z2\)\)0\\leq\(u\-z\_\{2\}\)\\bigl\(h\_\{U\}\(z\_\{2\}\)\-\\sigma\(z\_\{2\}\)\\bigr\);

A symmetric statement holds for the lower boundhLh\_\{L\}and is given in Appendix[H](https://arxiv.org/html/2608.17070#A8)\. Moreover, the linear relaxations selected by CROWN \(given in Appendix[A\.2](https://arxiv.org/html/2608.17070#A1.SS2)\) satisfy these criteria\.

See proof in Appendix[H](https://arxiv.org/html/2608.17070#A8)\. Figure[2](https://arxiv.org/html/2608.17070#S5.F2)provides an example of upper boundshUh\_\{U\}for both casesz2≤uz\_\{2\}\\leq uandz2\>u\.z\_\{2\}\>u\.

![Refer to caption](https://arxiv.org/html/2608.17070v1/figs/tanh_fourpoint_a.png)

![Refer to caption](https://arxiv.org/html/2608.17070v1/figs/tanh_fourpoint_b.png)

Figure 2:Case\-free four\-point soundness \(Theorem[5\.1](https://arxiv.org/html/2608.17070#S5.Thmtheorem1)\) for the activation functionσ⁡\(z\)=tanh⁡\(z\)\.\\sigma\(z\)=\\tanh\(z\)\.The left image depicts\[l,u\]=\[−1\.5,1\.5\]\[l,u\]=\[\-1\.5,1\.5\],z2≤uz\_\{2\}\\leq u, andσ⁡\(z2\)≤hU​\(z2\)\\sigma\(z\_\{2\}\)\\leq h\_\{U\}\(z\_\{2\}\)\. The right image depicts\[l,u\]=\[−1\.5,0\.2\]\[l,u\]=\[\-1\.5,0\.2\],z2\>uz\_\{2\}\>u, andσ⁡\(z2\)\>hU​\(z2\)\.\\sigma\(z\_\{2\}\)\>h\_\{U\}\(z\_\{2\}\)\.Both cases therefore satisfy the criteria given by Theorem[5\.1](https://arxiv.org/html/2608.17070#S5.Thmtheorem1)without requiring case\-specific analysis\.ZKP Algorithm\. We present the Four\-Point Relaxation Gadget \(formal algorithm in Appendix[B](https://arxiv.org/html/2608.17070#A2)\) as a simple set of criteria which𝒫\\mathcal\{P\}proves and𝒱\\mathcal\{V\}verifies\. We encode Theorem[5\.1](https://arxiv.org/html/2608.17070#S5.Thmtheorem1)as a set of ZKP constraints, which invokeΠarith\\Pi\_\{\\textsc\{arith\}\}andΠlookup\\Pi\_\{\\textsc\{lookup\}\}ZKP systems as subroutines\.

For each neuron, and for the upper bound case,𝒫\\mathcal\{P\}takes as private witness the interval endpoints\(l,u\)\(l,u\), the upper bound\(a¯,b¯\)\(\\overline\{a\},\\overline\{b\}\), and the tangency points\(z1,z2\)\(z\_\{1\},z\_\{2\}\)\.𝒫\\mathcal\{P\}evaluatesσ\\sigmaat the witness points and proves the correctness of these evaluations using lookup tablesTσT\_\{\\sigma\}andTσ′T\_\{\\sigma^\{\\prime\}\}\.𝒫\\mathcal\{P\}then proves the conditions of Theorem[5\.1](https://arxiv.org/html/2608.17070#S5.Thmtheorem1)are met\. Algorithm[2](https://arxiv.org/html/2608.17070#alg2)of Appendix[B](https://arxiv.org/html/2608.17070#A2)formally presents the prover for the upper\-bound case, and the lower\-bound case is analogous\.𝒱\\mathcal\{V\}checks the correctness of all proofs\.

### 5\.2ReLU Activations

For ReLU,σ⁡\(z\)=max⁡\(0,z\)\\sigma\(z\)=\\max\(0,z\)is piecewise linear and convex\. CROWN selects lower and upper bounds\(hL,hU\)\(h\_\{L\},h\_\{U\}\)for an interval\[l,u\]\[l,u\]as follows:

- •Upper boundhUh\_\{U\}:select the secant line connecting\(l,σ⁡\(l\)\)\(l,\\sigma\(l\)\)and\(u,σ⁡\(u\)\)\(u,\\sigma\(u\)\), given by hU​\(z\)=σ⁡\(u\)−σ⁡\(l\)u−l​\(z−l\)\+σ⁡\(l\)\.h\_\{U\}\(z\)=\\frac\{\\sigma\(u\)\-\\sigma\(l\)\}\{u\-l\}\(z\-l\)\+\\sigma\(l\)\.
- •Lower boundhL:h\_\{L\}:selecthL​\(z\)=a¯​zh\_\{L\}\(z\)=\\underline\{a\}zfor anya¯∈\{0,1\}\.\\underline\{a\}\\in\\\{0,1\\\}\.Either choice ofaaguarantees a valid linear relaxation\.[32](https://arxiv.org/html/2608.17070#bib.bib3)recommends selectinga¯=𝟏\[\|u\|≥\|l\|\]\.\\underline\{a\}=\\mathbf\{1\}\\left\[\|u\|\\geq\|l\|\\right\]\.

We design a simple algorithm for proving the validity of such a linear relaxation\(hL,hU\)\.\(h\_\{L\},h\_\{U\}\)\.

- •Upper boundhUh\_\{U\}:proveσ​\(l\)=hU​\(l\)\\sigma\(l\)=h\_\{U\}\(l\)andσ​\(u\)=hU​\(u\)\.\\sigma\(u\)=h\_\{U\}\(u\)\.
- •Lower boundhLh\_\{L\}:provea¯​\(a¯−1\)=0\\underline\{a\}\(\\underline\{a\}\-1\)=0\(i\.e\.a¯∈\{0,1\}\\underline\{a\}\\in\\\{0,1\\\}\) and interceptb¯=0\.\\underline\{b\}=0\.

Each of these conditions is proven withΠarith\.\\Pi\_\{\\textsc\{arith\}\}\.For further generality,a¯\\underline\{a\}can be selected within the closed interval\[0,1\]\[0,1\]andΠlookup\\Pi\_\{\\textsc\{lookup\}\}can be used for the proof, thus supportingα\\alpha\-CROWN\[[30](https://arxiv.org/html/2608.17070#bib.bib5)\]\.

## 6Implementation and Evaluations

We implement PANDA in Rust, using the arkworks ecosystem\[[1](https://arxiv.org/html/2608.17070#bib.bib25)\]for ZKP programming\. We use Hyrax\[[28](https://arxiv.org/html/2608.17070#bib.bib14)\]over the elliptic curve BN254 forΠcom\\Pi\_\{\\textsc\{com\}\}, the protocol of[26](https://arxiv.org/html/2608.17070#bib.bib15)forΠarith\\Pi\_\{\\textsc\{arith\}\}, and LogUp\-GKR\[[21](https://arxiv.org/html/2608.17070#bib.bib13)\]forΠlookup\\Pi\_\{\\textsc\{lookup\}\}\. Our implementation uses the non\-zero\-knowledge variants of these protocols for simplicity, but we estimate that the use of zero\-knowledge variants would increase the prover time by only a small constant factor \(e\.g\., see\[[16](https://arxiv.org/html/2608.17070#bib.bib32),[14](https://arxiv.org/html/2608.17070#bib.bib33)\]\)\. In our experiments, we use AMD EPYC 9575F processors\. Each job evaluates one model and runs on one core with 72 GiB of maximum allocated memory\.

In our evaluations, we answer the following questions:

Q1: Scalability\. How does PANDA scale to large networks?

Q2: Support of activation functions\. How does PANDA perform on activations other than ReLU?

Q3: Fidelity\. Is there any mismatch between certification results for PANDA and CROWN?

Q4: Comparison with CROWN\. How much is the cost paid for privacy?

Q5: Comparison with previous work\. How does PANDA perform compared with previous work?

Benchmark suites\. We evaluate PANDA on the MNIST image classification models\[[18](https://arxiv.org/html/2608.17070#bib.bib31)\]from the CROWN evaluation\. In addition, we evaluate PANDA on two application\-focused benchmarks: SafeNLP\[[2](https://arxiv.org/html/2608.17070#bib.bib7)\]from VNN\-COMP 2025\[[13](https://arxiv.org/html/2608.17070#bib.bib9)\]includes medical models that classify medical queries as high or low risk, and robot\-detection models that classify text as originating from a human or robot\. LunarLander\[[17](https://arxiv.org/html/2608.17070#bib.bib10)\]from VNN\-COMP 2022\[[19](https://arxiv.org/html/2608.17070#bib.bib8)\]classifies safe actions to be taken by lunar robots\. Finally, we evaluate on the only publicly available benchmark from FairProof’s suite\[[31](https://arxiv.org/html/2608.17070#bib.bib17)\]\.

Evaluations\. We run 100 tests per model, except for FairProof \(one test is run\) and MNIST \(the 100 images are filtered to those correctly classified by the model\)\. Only images which CROWN first certifies are tested with PANDA\. We use 8 bits of quantization for FairProof and 14 bits for all other evaluations\. Our results are summarized in Table[1](https://arxiv.org/html/2608.17070#S6.T1), with full benchmarks in Table[3](https://arxiv.org/html/2608.17070#A4.T3)and a component\-wise breakdown of prover time in Appendix[E](https://arxiv.org/html/2608.17070#A5)\.

Table 1:Summary of results\. Each row is one model\. We denote anmm\-layer feed\-forward network withnnneurons per layer bym×\[n\]\.m\\times\[n\]\.Prove and verify times are reported as mean and standard deviation\. FairProof Adult is a two\-layer network with 8 and 2 neurons, denoted\[8,2\]\[8,2\]\.DatasetStructureAct\.Prove \(s\)Verify \(s\)ProofCROWNDrift\(MB\)\(s\)\(%\)MNIST2×\[20\]2\\times\[20\]ReLU22\.81±2022\.81\\pm 200\.97±10\.97\\pm 131\.3e\-40\.023×\[1024\]3\\times\[1024\]ReLU101\.58±375101\.58\\pm 3754\.60±134\.60\\pm 1390\.220\.034×\[1024\]4\\times\[1024\]ReLU226\.08±1467226\.08\\pm 14679\.56±489\.56\\pm 48170\.44\-0\.014×\[1024\]4\\times\[1024\]Sigmoid327\.47±1136327\.47\\pm 113614\.13±4614\.13\\pm 46310\.472\.484×\[1024\]4\\times\[1024\]Tanh333\.94±581333\.94\\pm 58114\.31±2814\.31\\pm 28320\.466\.33OtherSafeNLP med2×\[128\]2\\times\[128\]ReLU23\.04±1923\.04\\pm 190\.81±10\.81\\pm 131\.3e\-4\-0\.05SafeNLP robot2×\[128\]2\\times\[128\]ReLU20\.33±1920\.33\\pm 190\.78±10\.78\\pm 131\.4e\-4\-0\.29LunarLander3×\[64\]3\\times\[64\]ReLU36\.61±2936\.61\\pm 291\.46±21\.46\\pm 258\.1e\-5\-0\.09FairProof Adult\[8,2\]\[8,2\]ReLU34\.8934\.891\.211\.2141\.4e\-5\-12\.60Q1: Scalability\. PANDA produces proofs of local robustness in under six minutes for the largest4×\[1024\]4\\times\[1024\]MNIST networks, which have 2\.9 million parameters\.

Q2: Support of activation functions\. Relative to ReLU networks, sigmoid/tanh increases proving time by1\.51\.5–2\.6×2\.6\\times, with verification time and proof size growing by a similar factor\.

Q3: Fidelity\. The use of quantization in PANDA induces errors relative to exact arithmetic in CROWN, as rounding operations are lossy and lookup tables discretize the real interval\. We assess the effect of quantization error empirically, by measuring the drift incurred between PANDA and CROWN, and recording any differences in the respective certification results\. Our results show that PANDA can verify all claims that CROWN verifies, and that the quantization drift is limited to small relative differences which can be effectively managed by tuning the quantization precision\.

Q4: Comparison with CROWN\. The cost of privacy is a prover overhead of roughly100100–1,000×1\{,\}000\\timesand a verifier overhead of2020–50×50\\timesover CROWN on the 1024\-neuron models \(rising to106×10^\{6\}\\timesonly on toy networks where CROWN runs in microseconds and ZKP fixed costs dominate\)\.

Q5: Comparison with previous work\. FairProof is the only suitable direct comparison; it is the only ZKP system that can certify local robustness, to the best of our knowledge\. We evaluate FairProof head\-to\-head with PANDA on small benchmarks\. We observe that FairProof cannot run on even the smallest network in the MNIST benchmark\. Where FairProof runs \(on FairProof Adult\), PANDA wins on prover time, requiring about half as much as FairProof’s prover time, with a feasible verifier cost \(1\.211\.21s\) and proof size \(44MB\)\. FairProof has smaller proof size and verifier time, whereas PANDA’s advantage is prover feasibility and scale\. See Appendix[C](https://arxiv.org/html/2608.17070#A3)for a detailed discussion\.

## 7Known Limitations

PANDA can only prove robustness for quantized models, not for general floating\-point models\. This limitation is consistent with previous works in zkML\[[22](https://arxiv.org/html/2608.17070#bib.bib16),[6](https://arxiv.org/html/2608.17070#bib.bib29)\]\. The precision level specified in the quantization affects the accuracy of values retrieved from the lookup tables used in our non\-linear activation functions and the lossiness of rounding operations\. Additionally, PANDA discloses the model architecture, layer dimensions, and activation function in the public statement, hiding only the model weights and biases\. However, DNNs can be padded with dummy layers and weights to hide exact dimensions\.

From the formal verification side, complete verification of local robustness of DNNs is NP\-hard\[[12](https://arxiv.org/html/2608.17070#bib.bib11)\]\. Algorithms such as CROWN areincomplete verifiers: they over\-approximate robustness bounds in polynomial time\. They can verify many but not all robustness claims, and crucially they cannot falsify a claim\. PANDA inherits this property of being an incomplete verifier\.

## 8Related Work

Proof of fairness\. Fairness is a notion related to local robustness which states that sensitive characteristics such as race and gender should not affect model outputs\. FairProof\[[31](https://arxiv.org/html/2608.17070#bib.bib17)\]proposes a framework for verifying local fairness as well as robustness properties using ZKPs\. Their approach supports only ReLU activations and enumerates all possible neuron activations in a preprocessing phase\. The prover time grows exponentially with the number of neurons in the network, which does not scale well to large models\. FairZK by\[[33](https://arxiv.org/html/2608.17070#bib.bib18)\]and OATH by\[[5](https://arxiv.org/html/2608.17070#bib.bib26)\]prove a notion ofglobal fairnessusing aggregated statistics; this direction is disjoint from our work and produces weaker bounds\. Confidential\-PROFITT by\[[24](https://arxiv.org/html/2608.17070#bib.bib19)\]enables privacy\-preserving proofs of training for tree\-split constraints in decision trees, which are simpler than those required for deep neural networks\. A separate line of work, including\[[23](https://arxiv.org/html/2608.17070#bib.bib21),[27](https://arxiv.org/html/2608.17070#bib.bib20)\], focuses on verifying global fairness in a third\-party auditor setting\.

Non\-cryptographic certification approaches\. Prior work has developed powerful formal verification techniques for certifying local robustness of DNNs\[[12](https://arxiv.org/html/2608.17070#bib.bib11),[32](https://arxiv.org/html/2608.17070#bib.bib3),[30](https://arxiv.org/html/2608.17070#bib.bib5)\]\. However, these approaches operate in a non\-cryptographic setting, where the verifier requires access to model parameters\. In contrast, PANDA certifies such properties in zero knowledge, without revealing model parameters\.

Concurrent work\. In a concurrent paper,[25](https://arxiv.org/html/2608.17070#bib.bib30)introduce an algorithm called SecureCROWN, which augments the CROWN algorithm to add privacy and verifiability to local robustness claims\. They use secure two\-party computation \(2PC\) to jointly compute the CROWN algorithm\. As a result, a data owner can hide their query point𝒙0\\boldsymbol\{x\}\_\{0\}and perturbation radiusε\\varepsilonwhile the model owner hides the model\. However, their computation trace is not publicly verifiable, and their construction is in the honest\-but\-curious setting which assumes the server does not deviate from the protocol\. The use of 2PC results in high communication overhead between the two parties, and their protocol supports only ReLU activations and not sigmoid or tanh\.

## 9Conclusion

In this paper, we introduced the PANDA protocol for confidentially proving and verifying linear properties of model outputs, such as fairness and robustness\. We evaluated PANDA on leading benchmarks and demonstrated our performance improvements in terms of prover time and scalability\. PANDA promotes transparency in ML infrastructure by enabling model owners to publicly share verifiable proofs of robustness without revealing model data\. We hope this work will encourage greater interest and further research in this direction\.

## Acknowledgments and Disclosure of Funding

This material is based upon work supported in part by the Defense Advanced Research Projects Agency \(DARPA\) under Agreement No\. HR00112590130 and by the NSF awards CCF\-2219995, CNS\-2245344, and CCF\-2318974\. Ben Merbaum gratefully acknowledges financial support for this project by the Fulbright Canada Student Program, which is sponsored by the U\.S\. Department of State and Fulbright Canada\. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the funding agencies\. We thank Tianyu Zhang for insightful discussions on implementing customized ZKP systems\. We acknowledge the resources provided by the Yale Center for Research Computing\.

## References

- \[1\]arkworks authors\(2022\)Arkworks zkSNARK ecosystem\.External Links:[Link](https://arkworks.rs/)Cited by:[§6](https://arxiv.org/html/2608.17070#S6.p1.1)\.
- \[2\]M\. Casadio, T\. Dinkar, E\. Komendantskaya, L\. Arnaboldi, M\. L\. Daggitt, O\. Isac, G\. Katz, V\. Rieser, and O\. Lemon\(2026\)NLP verification: towards a general methodology for certifying robustness\.European Journal of Applied Mathematics37\(1\),pp\. 180–237\.External Links:[Document](https://dx.doi.org/10.1017/S0956792525000099)Cited by:[§6](https://arxiv.org/html/2608.17070#S6.p9.1)\.
- \[3\]H\. Duong, T\. Nguyen, and M\. Dwyer\(2024\)A DPLL\(T\) framework for verifying deep neural networks\.External Links:2307\.10266,[Link](https://arxiv.org/abs/2307.10266)Cited by:[§1](https://arxiv.org/html/2608.17070#S1.p7.1)\.
- \[4\]H\. Duong, T\. Nguyen, and M\. Dwyer\(2025\)Generating and checking DNN verification proofs\.InAdvances in Neural Information Processing Systems,D\. Belgrave, C\. Zhang, H\. Lin, R\. Pascanu, P\. Koniusz, M\. Ghassemi, and N\. Chen \(Eds\.\),Vol\.38,pp\. 65887–65909\.External Links:[Link](https://proceedings.neurips.cc/paper_files/paper/2025/file/5f326d2e040a20d52438873f5d727e58-Paper-Conference.pdf)Cited by:[§1](https://arxiv.org/html/2608.17070#S1.p5.1)\.
- \[5\]O\. Franzese, A\. S\. Shamsabadi, C\. Luck, and H\. Haddadi\(2025\)Secure and confidential certificates of online fairness\.InThe Thirty\-ninth Annual Conference on Neural Information Processing Systems,External Links:[Link](https://openreview.net/forum?id=9jaQTx1O8T)Cited by:[§8](https://arxiv.org/html/2608.17070#S8.p1.1)\.
- \[6\]N\. Gailly, I\. Hishon\-Rezaizadeh, T\. Liu, N\. Mainardi, D\. Papadopoulos, C\. Papamanthou, C\. Pappas, S\. Srinivasan, Z\. Youell, and Y\. Zhang\(2026\)DeepProve: verifiable end\-to\-end large language model inference\.Note:Cryptology ePrint Archive, Paper 2026/1112External Links:[Link](https://eprint.iacr.org/2026/1112)Cited by:[§1](https://arxiv.org/html/2608.17070#S1.p4.1),[§2](https://arxiv.org/html/2608.17070#S2.p6.1),[§7](https://arxiv.org/html/2608.17070#S7.p1.1)\.
- \[7\]R\. J\. George, J\. Cruden, X\. Zhong, H\. Zhang, and A\. Anandkumar\(2026\)TorchLean: formalizing neural networks in lean\.External Links:2602\.22631,[Link](https://arxiv.org/abs/2602.22631)Cited by:[§1](https://arxiv.org/html/2608.17070#S1.p5.1)\.
- \[8\]S\. Goldwasser, S\. Micali, and C\. Rackoff\(1985\)The knowledge complexity of interactive proof\-systems\.InProceedings of the Seventeenth Annual ACM Symposium on Theory of Computing,STOC ’85,New York, NY, USA,pp\. 291–304\.External Links:ISBN 0897911512,[Link](https://doi.org/10.1145/22145.22178),[Document](https://dx.doi.org/10.1145/22145.22178)Cited by:[§1](https://arxiv.org/html/2608.17070#S1.p4.1)\.
- \[9\]A\. Hannun, C\. Guo, and L\. van der Maaten\(2021\)Measuring data leakage in machine\-learning models with Fisher information\.InProceedings of the Thirty\-Seventh Conference on Uncertainty in Artificial Intelligence,C\. de Campos and M\. H\. Maathuis \(Eds\.\),Proceedings of Machine Learning Research, Vol\.161,pp\. 760–770\.External Links:[Link](https://proceedings.mlr.press/v161/hannun21a.html)Cited by:[§1](https://arxiv.org/html/2608.17070#S1.p3.1)\.
- \[10\]M\. Hines\(2019\)I Smell a Bot: California’s S\.B\. 1001, Free Speech, and the Future of Bot Regulation\.Houston Law Review57\(2\) \(en\)\.External Links:[Link](https://houstonlawreview.org/article/11569-i-smell-a-bot-california-s-s-b-1001-free-speech-and-the-future-of-bot-regulation)Cited by:[§1](https://arxiv.org/html/2608.17070#S1.p1.1)\.
- \[11\]B\. Jacob, S\. Kligys, B\. Chen, M\. Zhu, M\. Tang, A\. Howard, H\. Adam, and D\. Kalenichenko\(2018\)Quantization and training of neural networks for efficient integer\-arithmetic\-only inference\.In2018 IEEE/CVF Conference on Computer Vision and Pattern Recognition,Vol\.,pp\. 2704–2713\.External Links:[Document](https://dx.doi.org/10.1109/CVPR.2018.00286)Cited by:[§2](https://arxiv.org/html/2608.17070#S2.p6.1)\.
- \[12\]G\. Katz, C\. Barrett, D\. L\. Dill, K\. Julian, and M\. J\. Kochenderfer\(2017\)Reluplex: an efficient SMT solver for verifying deep neural networks\.InComputer Aided Verification,R\. Majumdar and V\. Kunčak \(Eds\.\),Cham,pp\. 97–117\.External Links:ISBN 978\-3\-319\-63387\-9Cited by:[§7](https://arxiv.org/html/2608.17070#S7.p2.1),[§8](https://arxiv.org/html/2608.17070#S8.p2.1)\.
- \[13\]K\. Kaulen, T\. Ladner, S\. Bak, C\. Brix, H\. Duong, T\. Flinkow, T\. T\. Johnson, L\. Koller, E\. Manino, T\. H\. Nguyen, and H\. Wu\(2025\)The 6th international verification of neural networks competition \(VNN\-COMP 2025\): summary and results\.External Links:2512\.19007,[Link](https://arxiv.org/abs/2512.19007)Cited by:[§6](https://arxiv.org/html/2608.17070#S6.p9.1)\.
- \[14\]D\. Kaviani and S\. Setty\(2025\)Vega: low\-latency zero\-knowledge proofs over existing credentials\.Note:Cryptology ePrint Archive, Paper 2025/2094External Links:[Link](https://eprint.iacr.org/2025/2094)Cited by:[§6](https://arxiv.org/html/2608.17070#S6.p1.1)\.
- \[15\]M\. Kop\(2021\)EU Artificial Intelligence Act: The European Approach to AI\.SSRN Scholarly Paper,Social Science Research Network,Rochester, NY\(en\)\.External Links:[Link](https://papers.ssrn.com/abstract=3930959)Cited by:[§1](https://arxiv.org/html/2608.17070#S1.p1.1)\.
- \[16\]A\. Kothapalli and S\. Setty\(2024\)HyperNova: recursive arguments for customizable constraint systems\.InAdvances in Cryptology – CRYPTO 2024,L\. Reyzin and D\. Stebila \(Eds\.\),Cham,pp\. 345–379\.External Links:ISBN 978\-3\-031\-68403\-6Cited by:[§6](https://arxiv.org/html/2608.17070#S6.p1.1)\.
- \[17\]V\. Krish\(2022\)min\-err\-trajs\-vnncomp\-benchmarks\.Note:\[Online; accessed 6\. May 2026\]External Links:[Link](https://github.com/Ethos-lab/min-err-trajs-vnncomp-benchmarks)Cited by:[§6](https://arxiv.org/html/2608.17070#S6.p9.1)\.
- \[18\]Y\. LeCun, L\. Bottou, Y\. Bengio, and P\. Haffner\(1998\)Gradient\-based learning applied to document recognition\.Proceedings of the IEEE86\(11\),pp\. 2278–2324\.External Links:[Link](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.7665)Cited by:[§6](https://arxiv.org/html/2608.17070#S6.p9.1)\.
- \[19\]M\. N\. Müller, C\. Brix, S\. Bak, C\. Liu, and T\. T\. Johnson\(2023\)The third international verification of neural networks competition \(VNN\-COMP 2022\): summary and results\.External Links:2212\.10376,[Link](https://arxiv.org/abs/2212.10376)Cited by:[§6](https://arxiv.org/html/2608.17070#S6.p9.1)\.
- \[20\]M\. Nasr, R\. Shokri, and A\. Houmansadr\(2019\)Comprehensive privacy analysis of deep learning: passive and active white\-box inference attacks against centralized and federated learning\.In2019 IEEE Symposium on Security and Privacy \(SP\),Vol\.,pp\. 739–753\.External Links:[Document](https://dx.doi.org/10.1109/SP.2019.00065)Cited by:[§1](https://arxiv.org/html/2608.17070#S1.p3.1)\.
- \[21\]S\. Papini and U\. Haböck\(2023\)Improving logarithmic derivative lookups using GKR\.Note:Cryptology ePrint Archive, Paper 2023/1284External Links:[Link](https://eprint.iacr.org/2023/1284)Cited by:[Table 4](https://arxiv.org/html/2608.17070#A4.T4),[§6](https://arxiv.org/html/2608.17070#S6.p1.1)\.
- \[22\]W\. Qu, Y\. Sun, X\. Liu, T\. Lu, Y\. Guo, K\. Chen, and J\. Zhang\(2025\)zkGPT: an efficient non\-interactive zero\-knowledge proof framework for LLM inference\.InProceedings of the 34th USENIX Conference on Security Symposium,SEC ’25,USA\.External Links:ISBN 978\-1\-939133\-52\-6Cited by:[§1](https://arxiv.org/html/2608.17070#S1.p4.1),[§2](https://arxiv.org/html/2608.17070#S2.p6.1),[§7](https://arxiv.org/html/2608.17070#S7.p1.1)\.
- \[23\]S\. Segal, Y\. Adi, B\. Pinkas, C\. Baum, C\. Ganesh, and J\. Keshet\(2021\)Fairness in the eyes of the data: certifying machine\-learning models\.InProceedings of the 2021 AAAI/ACM Conference on AI, Ethics, and Society,AIES ’21,New York, NY, USA,pp\. 926–935\.External Links:ISBN 9781450384735,[Link](https://doi.org/10.1145/3461702.3462554),[Document](https://dx.doi.org/10.1145/3461702.3462554)Cited by:[§8](https://arxiv.org/html/2608.17070#S8.p1.1)\.
- \[24\]A\. S\. Shamsabadi, S\. C\. Wyllie, N\. Franzese, N\. Dullerud, S\. Gambs, N\. Papernot, X\. Wang, and A\. Weller\(2023\)Confidential\-PROFITT: confidential PRO of FaIr Training of Trees\.InThe Eleventh International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=iIfDQVyuFD)Cited by:[§8](https://arxiv.org/html/2608.17070#S8.p1.1)\.
- \[25\]N\. Song, X\. Luan, Y\. Guo, R\. Bie, M\. Sun, and X\. Zhang\(2026\)Privacy\-preserving robustness verification for neural networks\.InThe 42nd Conference on Uncertainty in Artificial Intelligence \(UAI\),Cited by:[§8](https://arxiv.org/html/2608.17070#S8.p3.1)\.
- \[26\]J\. Thaler\(2013\)Time\-optimal interactive proofs for circuit evaluation\.InAdvances in Cryptology – CRYPTO 2013,R\. Canetti and J\. A\. Garay \(Eds\.\),Berlin, Heidelberg,pp\. 71–89\.External Links:ISBN 978\-3\-642\-40084\-1Cited by:[Table 4](https://arxiv.org/html/2608.17070#A4.T4),[§6](https://arxiv.org/html/2608.17070#S6.p1.1)\.
- \[27\]E\. Toreini, M\. Mehrnezhad, and A\. van Moorsel\(2023\)Verifiable fairness: privacy\-preserving computation of fairness for machine learning systems\.InComputer Security\. ESORICS 2023 International Workshops: CPS4CIP, ADIoT, SecAssure, WASP, TAURIN, PriST\-AI, and SECAI, The Hague, The Netherlands, September 25–29, 2023, Revised Selected Papers, Part II,Berlin, Heidelberg,pp\. 569–584\.External Links:ISBN 978\-3\-031\-54128\-5,[Link](https://doi.org/10.1007/978-3-031-54129-2_34),[Document](https://dx.doi.org/10.1007/978-3-031-54129-2%5F34)Cited by:[§8](https://arxiv.org/html/2608.17070#S8.p1.1)\.
- \[28\]R\. S\. Wahby, I\. Tzialla, A\. Shelat, J\. Thaler, and M\. Walfish\(2018\)Doubly\-efficient zkSNARKs without trusted setup\.In2018 IEEE Symposium on Security and Privacy \(SP\),Vol\.,pp\. 926–943\.External Links:[Document](https://dx.doi.org/10.1109/SP.2018.00060)Cited by:[Table 4](https://arxiv.org/html/2608.17070#A4.T4),[§6](https://arxiv.org/html/2608.17070#S6.p1.1)\.
- \[29\]S\. Wang, H\. Zhang, K\. Xu, X\. Lin, S\. Jana, C\. Hsieh, and J\. Z\. Kolter\(2021\)Beta\-CROWN: efficient bound propagation with per\-neuron split constraints for neural network robustness verification\.InAdvances in Neural Information Processing Systems,M\. Ranzato, A\. Beygelzimer, Y\. Dauphin, P\.S\. Liang, and J\. W\. Vaughan \(Eds\.\),Vol\.34,pp\. 29909–29921\.External Links:[Link](https://proceedings.neurips.cc/paper_files/paper/2021/file/fac7fead96dafceaf80c1daffeae82a4-Paper.pdf)Cited by:[§1](https://arxiv.org/html/2608.17070#S1.p7.1)\.
- \[30\]K\. Xu, H\. Zhang, S\. Wang, Y\. Wang, S\. Jana, X\. Lin, and C\. Hsieh\(2021\)Fast and Complete: enabling complete neural network verification with rapid and massively parallel incomplete verifiers\.InInternational Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=nVZtXBI6LNn)Cited by:[§1](https://arxiv.org/html/2608.17070#S1.p7.1),[§5\.2](https://arxiv.org/html/2608.17070#S5.SS2.p1.3),[§8](https://arxiv.org/html/2608.17070#S8.p2.1)\.
- \[31\]C\. Yadav, A\. Roy Chowdhury, D\. Boneh, and K\. Chaudhuri\(2024\)FairProof: confidential and certifiable fairness for neural networks\.InProceedings of the 41st International Conference on Machine Learning,R\. Salakhutdinov, Z\. Kolter, K\. Heller, A\. Weller, N\. Oliver, J\. Scarlett, and F\. Berkenkamp \(Eds\.\),Proceedings of Machine Learning Research, Vol\.235,pp\. 55682–55705\.External Links:[Link](https://proceedings.mlr.press/v235/yadav24a.html)Cited by:[Appendix C](https://arxiv.org/html/2608.17070#A3.p1.1),[§1](https://arxiv.org/html/2608.17070#S1.p4.1),[§6](https://arxiv.org/html/2608.17070#S6.p9.1),[§8](https://arxiv.org/html/2608.17070#S8.p1.1)\.
- \[32\]H\. Zhang, T\. Weng, P\. Chen, C\. Hsieh, and L\. Daniel\(2018\)Efficient neural network robustness certification with general activation functions\.InProceedings of the 32nd International Conference on Neural Information Processing Systems,NIPS’18,Red Hook, NY, USA,pp\. 4944–4953\.Cited by:[§1](https://arxiv.org/html/2608.17070#S1.p10.1),[§1](https://arxiv.org/html/2608.17070#S1.p7.1),[§3](https://arxiv.org/html/2608.17070#S3.p1.1),[2nd item](https://arxiv.org/html/2608.17070#S5.I3.i2.p1.1),[§8](https://arxiv.org/html/2608.17070#S8.p2.1)\.
- \[33\]T\. Zhang, S\. Dong, O\. D\. Kose, Y\. Shen, and Y\. Zhang\(2025\)FairZK: a scalable system to prove machine learning fairness in zero\-knowledge\.In2025 IEEE Symposium on Security and Privacy \(SP\),Vol\.,pp\. 3460–3478\.External Links:[Document](https://dx.doi.org/10.1109/SP61157.2025.00205)Cited by:[§8](https://arxiv.org/html/2608.17070#S8.p1.1)\.

## Appendix ADetails of CROWN

In this section, we provide the full descriptions of the CROWN algorithm and the PANDA framework, with pseudocode algorithms\.

### A\.1The CROWN Algorithm

Algorithm[1](https://arxiv.org/html/2608.17070#alg1)gives the full CROWN procedure\. This consists of an outer forward pass over layerskk, and an inner backward pass from layerkkdown to the input layer 0\. The backward pass repeatedly callsStep1, the activation\-relaxation update \([11](https://arxiv.org/html/2608.17070#S3.E11)\), andStep2, the linear\-map substitution \([12](https://arxiv.org/html/2608.17070#S3.E12)\)\. Concretization \([13](https://arxiv.org/html/2608.17070#S3.E13)\) is applied following each backward pass\. For simplicity of notation, we assume relaxation scalars\(𝒂¯\(ℓ\),𝒃¯\(ℓ\),𝒂¯\(ℓ\),𝒃¯\(ℓ\)\)\(\\boldsymbol\{\\overline\{a\}\}^\{\(\\ell\)\},\\boldsymbol\{\\overline\{b\}\}^\{\(\\ell\)\},\\boldsymbol\{\\underline\{a\}\}^\{\(\\ell\)\},\\boldsymbol\{\\underline\{b\}\}^\{\(\\ell\)\}\)for each layerℓ\\ellare implicitly passed as input to all procedures below upon generation\.

Algorithm 1The CROWN algorithm\.Relaxproduces linear relaxations ofσ\\sigma\(see Section[5](https://arxiv.org/html/2608.17070#S5), and the selection algorithm in Appendix[A\.2](https://arxiv.org/html/2608.17070#A1.SS2)\)\.1:Network

\{𝐖\(k\),𝒃\(k\)\}k=1m\\\{\\mathbf\{W\}^\{\(k\)\},\\boldsymbol\{b\}^\{\(k\)\}\\\}\_\{k=1\}^\{m\}, input

𝒙0\\boldsymbol\{x\}\_\{0\}, perturbation budget

ε\\varepsilon, robustness claim

\(𝐂,𝒖\)\(\\mathbf\{C\},\\boldsymbol\{u\}\)
2:for

k=1,…,mk=1,\\dots,mdo⊳\\trianglerightouter forward pass

3:

\(𝐀¯\(k\),𝒅¯\(k\),𝐀¯\(k\),𝒅¯\(k\)\)←BackwardPass​\(k\)\(\\underline\{\\mathbf\{A\}\}^\{\(k\)\},\\boldsymbol\{\\underline\{d\}\}^\{\(k\)\},\\overline\{\\mathbf\{A\}\}^\{\(k\)\},\\boldsymbol\{\\overline\{d\}\}^\{\(k\)\}\)\\leftarrow\\textsc\{BackwardPass\}\(k\)
4:

\(𝑳\(k\),𝑼\(k\)\)←Concretize​\(𝐀¯\(k\),𝒅¯\(k\),𝐀¯\(k\),𝒅¯\(k\),𝒙0,ε\)\(\\boldsymbol\{L\}^\{\(k\)\},\\boldsymbol\{U\}^\{\(k\)\}\)\\leftarrow\\textsc\{Concretize\}\(\\underline\{\\mathbf\{A\}\}^\{\(k\)\},\\boldsymbol\{\\underline\{d\}\}^\{\(k\)\},\\overline\{\\mathbf\{A\}\}^\{\(k\)\},\\boldsymbol\{\\overline\{d\}\}^\{\(k\)\},\\boldsymbol\{x\}\_\{0\},\\varepsilon\)
5:foreach neuron

iiin layer

k<mk<mdo

6:

\(a¯i\(k\),b¯i\(k\),a¯i\(k\),b¯i\(k\)\)←Relax​\(σ,Li\(k\),Ui\(k\)\)\(\\overline\{a\}^\{\(k\)\}\_\{i\},\\overline\{b\}^\{\(k\)\}\_\{i\},\\underline\{a\}^\{\(k\)\}\_\{i\},\\underline\{b\}^\{\(k\)\}\_\{i\}\)\\leftarrow\\textsc\{Relax\}\(\\sigma,L^\{\(k\)\}\_\{i\},U^\{\(k\)\}\_\{i\}\)
7:endfor

8:endfor

9:returnTrue if

𝑼\(m\)≤𝒖\\boldsymbol\{U\}^\{\(m\)\}\\leq\\boldsymbol\{u\}entry\-wise, else False otherwise

10:Upper\-bound pass \(the lower\-bound pass is analogous\):

11:procedureBackwardPass\(

kk\)

12:if

k<mk<mthen

13:

𝐀←𝐖\(k\),𝒅←𝒃\(k\)\\mathbf\{A\}\\leftarrow\\mathbf\{W\}^\{\(k\)\},\\quad\\boldsymbol\{d\}\\leftarrow\\boldsymbol\{b\}^\{\(k\)\}⊳\\trianglerightinitializesℐh\(k−1\)\\mathcal\{I\}\_\{h\}^\{\(k\-1\)\}

14:elseif

k=mk=mthen

15:

𝐀←𝐂𝐖\(k\),𝒅←𝐂​𝒃\(k\)\\mathbf\{A\}\\leftarrow\\mathbf\{C\}\\mathbf\{W\}^\{\(k\)\},\\quad\\boldsymbol\{d\}\\leftarrow\\mathbf\{C\}\\boldsymbol\{b\}^\{\(k\)\}⊳\\trianglerightfinal\-layer initialization

16:endif

17:for

ℓ=k−1,…,1\\ell=k\-1,\\dots,1do

18:

\(𝐀,𝒅\)←Step1​\(𝐀,𝒅,ℓ\)\(\\mathbf\{A\},\\boldsymbol\{d\}\)\\leftarrow\\textsc\{Step1\}\(\\mathbf\{A\},\\boldsymbol\{d\},\\ell\)⊳\\trianglerightℐh\(ℓ\)⇒ℐz\(ℓ\)\\mathcal\{I\}\_\{h\}^\{\(\\ell\)\}\\Rightarrow\\mathcal\{I\}\_\{z\}^\{\(\\ell\)\}

19:

\(𝐀,𝒅\)←Step2​\(𝐀,𝒅,ℓ\)\(\\mathbf\{A\},\\boldsymbol\{d\}\)\\leftarrow\\textsc\{Step2\}\(\\mathbf\{A\},\\boldsymbol\{d\},\\ell\)⊳\\trianglerightℐz\(ℓ\)⇒ℐh\(ℓ−1\)\\mathcal\{I\}\_\{z\}^\{\(\\ell\)\}\\Rightarrow\\mathcal\{I\}\_\{h\}^\{\(\\ell\-1\)\}

20:endfor

21:return

\(𝐀,𝒅\)\(\\mathbf\{A\},\\boldsymbol\{d\}\)⊳\\trianglerighttermination atℐh\(0\)\\mathcal\{I\}\_\{h\}^\{\(0\)\}

22:endprocedure

23:

24:procedureStep1\(

𝐀,𝒅,ℓ\\mathbf\{A\},\\boldsymbol\{d\},\\ell\)⊳\\trianglerightactivation\-relaxation update \([11](https://arxiv.org/html/2608.17070#S3.E11)\)

25:

𝐀\+←max⁡\(𝐀,0\)\\mathbf\{A\}\_\{\+\}\\leftarrow\\max\(\\mathbf\{A\},0\),

𝐀−←min⁡\(𝐀,0\)\\mathbf\{A\}\_\{\-\}\\leftarrow\\min\(\\mathbf\{A\},0\)
26:

𝒅←𝒅\+𝐀\+​𝒃¯\(ℓ\)\+𝐀−​𝒃¯\(ℓ\)\\boldsymbol\{d\}\\leftarrow\\boldsymbol\{d\}\+\\mathbf\{A\}\_\{\+\}\\,\\boldsymbol\{\\overline\{b\}\}^\{\(\\ell\)\}\+\\mathbf\{A\}\_\{\-\}\\,\\boldsymbol\{\\underline\{b\}\}^\{\(\\ell\)\}
27:

𝐀←𝐀\+​diag​\(𝒂¯\(ℓ\)\)\+𝐀−​diag​\(𝒂¯\(ℓ\)\)\\mathbf\{A\}\\leftarrow\\mathbf\{A\}\_\{\+\}\\,\\mathrm\{diag\}\(\\boldsymbol\{\\overline\{a\}\}^\{\(\\ell\)\}\)\+\\mathbf\{A\}\_\{\-\}\\,\\mathrm\{diag\}\(\\boldsymbol\{\\underline\{a\}\}^\{\(\\ell\)\}\)
28:return

\(𝐀,𝒅\)\(\\mathbf\{A\},\\boldsymbol\{d\}\)
29:endprocedure

30:

31:procedureStep2\(

𝐀,𝒅,ℓ\\mathbf\{A\},\\boldsymbol\{d\},\\ell\)⊳\\trianglerightlinear\-map substitution \([12](https://arxiv.org/html/2608.17070#S3.E12)\)

32:

𝒅←𝒅\+𝐀​𝒃\(ℓ\)\\boldsymbol\{d\}\\leftarrow\\boldsymbol\{d\}\+\\mathbf\{A\}\\,\\boldsymbol\{b\}^\{\(\\ell\)\}
33:

𝐀←𝐀​𝐖\(ℓ\)\\mathbf\{A\}\\leftarrow\\mathbf\{A\}\\,\\mathbf\{W\}^\{\(\\ell\)\}
34:return

\(𝐀,𝒅\)\(\\mathbf\{A\},\\boldsymbol\{d\}\)
35:endprocedure

36:

37:procedureConcretize\(

𝐀¯,𝒅¯,𝐀¯,𝒅¯,𝒙0,ε\\underline\{\\mathbf\{A\}\},\\boldsymbol\{\\underline\{d\}\},\\overline\{\\mathbf\{A\}\},\\boldsymbol\{\\overline\{d\}\},\\boldsymbol\{x\}\_\{0\},\\varepsilon\)

38:

𝐀¯\+←max⁡\(𝐀¯,0\)\\overline\{\\mathbf\{A\}\}\_\{\+\}\\leftarrow\\max\(\\overline\{\\mathbf\{A\}\},0\),

𝐀¯−←min⁡\(𝐀¯,0\)\\overline\{\\mathbf\{A\}\}\_\{\-\}\\leftarrow\\min\(\\overline\{\\mathbf\{A\}\},0\)
39:

𝐀¯\+←max⁡\(𝐀¯,0\)\\underline\{\\mathbf\{A\}\}\_\{\+\}\\leftarrow\\max\(\\underline\{\\mathbf\{A\}\},0\),

𝐀¯−←min⁡\(𝐀¯,0\)\\underline\{\\mathbf\{A\}\}\_\{\-\}\\leftarrow\\min\(\\underline\{\\mathbf\{A\}\},0\)
40:

𝑼←𝐀¯\+​\(𝒙0\+ε​𝟏\)\+𝐀¯−​\(𝒙0−ε​𝟏\)\+𝒅¯\\boldsymbol\{U\}\\leftarrow\\overline\{\\mathbf\{A\}\}\_\{\+\}\(\\boldsymbol\{x\}\_\{0\}\+\\varepsilon\\mathbf\{1\}\)\+\\overline\{\\mathbf\{A\}\}\_\{\-\}\(\\boldsymbol\{x\}\_\{0\}\-\\varepsilon\\mathbf\{1\}\)\+\\boldsymbol\{\\overline\{d\}\}
41:

𝑳←𝐀¯\+​\(𝒙0−ε​𝟏\)\+𝐀¯−​\(𝒙0\+ε​𝟏\)\+𝒅¯\\boldsymbol\{L\}\\leftarrow\\underline\{\\mathbf\{A\}\}\_\{\+\}\(\\boldsymbol\{x\}\_\{0\}\-\\varepsilon\\mathbf\{1\}\)\+\\underline\{\\mathbf\{A\}\}\_\{\-\}\(\\boldsymbol\{x\}\_\{0\}\+\\varepsilon\\mathbf\{1\}\)\+\\boldsymbol\{\\underline\{d\}\}
42:return

\(𝑳,𝑼\)\(\\boldsymbol\{L\},\\boldsymbol\{U\}\)
43:endprocedure

Time complexity\. For a neural network withmmlayers,nnneurons per layer, andnnoutput neurons, CROWN runs in timeO⁡\(m2​n3\)\.O\(m^\{2\}n^\{3\}\)\.The algorithm performs two nested for\-loops, consisting of the outer forward pass and the inner backward pass, each overmmlayers\. At each layer, CROWN performs multiplications ofn×nn\\times nmatrices, each requiring timeO⁡\(n3\)O\(n^\{3\}\)\.

### A\.2The Relaxation Algorithm

TheRelaxalgorithm takes as input a concretized interval\(l,u\)\(l,u\)and an activation functionσ\\sigma, and outputs scalars\(a¯,b¯,a¯,b¯\)\(\\overline\{a\},\\overline\{b\},\\underline\{a\},\\underline\{b\}\)satisfying

a¯​z\+b¯≤σ⁡\(z\)≤a¯​z\+b¯,∀z∈\[l,u\]\.\\underline\{a\}z\+\\underline\{b\}\\;\\leq\\;\\sigma\(z\)\\;\\leq\\;\\overline\{a\}z\+\\overline\{b\},\\qquad\\forall z\\in\[l,u\]\.\(18\)This algorithm is called extensively by CROWN to produce per\-neuron linear relaxations which can then be verified by PANDA via the Four\-Point Relaxation Gadget in Section[5](https://arxiv.org/html/2608.17070#S5)\.

Below, we describe theRelaxprocedure for S\-shaped activationsσ\\sigma\. The procedure for ReLU activations is provided in Section[5\.2](https://arxiv.org/html/2608.17070#S5.SS2)\. We also focus on the selection of the upper boundhU​\(z\)=a¯​z\+b¯h\_\{U\}\(z\)=\\overline\{a\}z\+\\overline\{b\}, as the lower bound is similar but with the roles ofllanduureversed\.

Procedure\. CROWN selects an optimal pair\(a¯,b¯\)\(\\overline\{a\},\\overline\{b\}\)via the following steps:

1. 1\.Solve the equation σ′​\(τ\)=σ⁡\(τ\)−σ⁡\(l\)τ−l\\sigma^\{\\prime\}\(\\tau\)=\\frac\{\\sigma\(\\tau\)\-\\sigma\(l\)\}\{\\tau\-l\}\(19\)forτ\\tau\. This can be solved directly given a closed form forσ\\sigmaandσ′\\sigma^\{\\prime\}, or iteratively solved via Newton’s method\. Intuitively, this equation asks for a valueτ\\tausuch that the tangent line ofσ⁡\(z\)\\sigma\(z\)atz=τz=\\tauis exactly equal to the secant line through\(l,σ⁡\(l\)\)\(l,\\sigma\(l\)\)and\(τ,σ⁡\(τ\)\)\.\(\\tau,\\sigma\(\\tau\)\)\.This equation has two solutions for S\-shaped activations, includingτ=l\\tau=las a trivial root\. By abuse of notation, we letτ\\taudenote the non\-trivial root\.
2. 2\.Choose an upper boundhU​\(z\)=a¯​z\+b¯h\_\{U\}\(z\)=\\overline\{a\}z\+\\overline\{b\}based on whereτ\\taufalls relative to the interval\[l,u\]\[l,u\]: - •Case 1:τ∈\(l,u\)\\tau\\in\(l,u\)\.Output the tangent line forσ\\sigmaatz=τz=\\tau: hU​\(z\)=σ⁡\(τ\)−σ⁡\(l\)τ−l​\(z−l\)\+σ⁡\(l\)\.h\_\{U\}\(z\)=\\frac\{\\sigma\(\\tau\)\-\\sigma\(l\)\}\{\\tau\-l\}\(z\-l\)\+\\sigma\(l\)\. - •Case 2:τ≤l\\tau\\leq l\.Thenσ\\sigmais concave on\[l,u\]\[l,u\], so any tangent line is an upper bound forσ\\sigmaover the interval\. Output the tangent at the midpointμ:=l\+u2\\mu:=\\frac\{l\+u\}\{2\}: hU​\(z\)=σ′​\(μ\)​\(z−μ\)\+σ⁡\(μ\)\.h\_\{U\}\(z\)=\\sigma^\{\\prime\}\(\\mu\)\(z\-\\mu\)\+\\sigma\(\\mu\)\. - •Case 3:τ≥u\\tau\\geq u\.Output the secant line through the two interval endpoints: hU​\(z\)=σ⁡\(u\)−σ⁡\(l\)u−l​\(z−l\)\+σ⁡\(l\)\.h\_\{U\}\(z\)=\\frac\{\\sigma\(u\)\-\\sigma\(l\)\}\{u\-l\}\(z\-l\)\+\\sigma\(l\)\.
3. 3\.Output\(a¯,b¯\)\(\\overline\{a\},\\overline\{b\}\)from the slope and intercept ofhUh\_\{U\}\.

The proof of soundness for this selection \(that it produces a valid upper bound\) is given in Appendix[H](https://arxiv.org/html/2608.17070#A8)\.

## Appendix BDetails of PANDA

In this appendix, we present the PANDA system in full detail\. Algorithm[2](https://arxiv.org/html/2608.17070#alg2)presents the prover for theFour\-Point Relaxation Gadget, accompanying Section[5\.1](https://arxiv.org/html/2608.17070#S5.SS1)\. Appendix[F](https://arxiv.org/html/2608.17070#A6)further shows how to eliminate theTσ′T\_\{\\sigma^\{\\prime\}\}table in Algorithm[2](https://arxiv.org/html/2608.17070#alg2)through an optimization\. Algorithms[3](https://arxiv.org/html/2608.17070#alg3)and[4](https://arxiv.org/html/2608.17070#alg4)present the full PANDA prover and verifier procedures, respectively\.

In our algorithms,Πlookup\\Pi\_\{\\textsc\{lookup\}\}uses three precomputed public lookup tables over the quantization domain𝒟\\mathcal\{D\}:

TReLU:=\{\(x,ReLU⁡\(x\)\):x∈𝒟\},Tσ:=\{\(x,σ⁡\(x\)\):x∈𝒟\},Tσ′:=\{\(x,σ′​\(x\)\):x∈𝒟\}\.T\_\{\\mathrm\{ReLU\}\}:=\\\{\(x,\\mathrm\{ReLU\}\(x\)\):x\\in\\mathcal\{D\}\\\},\\quad T\_\{\\sigma\}:=\\\{\(x,\\sigma\(x\)\):x\\in\\mathcal\{D\}\\\},\\quad T\_\{\\sigma^\{\\prime\}\}:=\\\{\(x,\\sigma^\{\\prime\}\(x\)\):x\\in\\mathcal\{D\}\\\}\.Πlookup\\Pi\_\{\\textsc\{lookup\}\}is also used to perform range proofs, as discussed in Section[2](https://arxiv.org/html/2608.17070#S2)\.

Algorithm 2Four\-Point Relaxation Gadget prover \(upper bound\)\.1:Witness

\(l,u,a¯,b¯,z1,z2\)\(l,u,\\overline\{a\},\\overline\{b\},z\_\{1\},z\_\{2\}\)and lookup tables

TσT\_\{\\sigma\},

Tσ′T\_\{\\sigma^\{\\prime\}\}
2:Compute

sl←σ⁡\(l\),su←σ⁡\(u\),s1←σ⁡\(z1\),s2←σ⁡\(z2\),s1′←σ′​\(z1\),s2′←σ′​\(z2\)s\_\{l\}\\leftarrow\\sigma\(l\),\\ s\_\{u\}\\leftarrow\\sigma\(u\),\\ s\_\{1\}\\leftarrow\\sigma\(z\_\{1\}\),\\ s\_\{2\}\\leftarrow\\sigma\(z\_\{2\}\),\\ s^\{\\prime\}\_\{1\}\\leftarrow\\sigma^\{\\prime\}\(z\_\{1\}\),\\ s^\{\\prime\}\_\{2\}\\leftarrow\\sigma^\{\\prime\}\(z\_\{2\}\)\.

3:

Πlookup\.Prove​\(\(l,sl\),\(u,su\),\(z1,s1\),\(z2,s2\)∈Tσ\)\.\\Pi\_\{\\textsc\{lookup\}\}\.\\textsc\{Prove\}\\left\(\(l,s\_\{l\}\),\(u,s\_\{u\}\),\(z\_\{1\},s\_\{1\}\),\(z\_\{2\},s\_\{2\}\)\\in T\_\{\\sigma\}\\right\)\.
4:

Πlookup\.Prove​\(\(z1,s1′\),\(z2,s2′\)∈Tσ′\)\\Pi\_\{\\textsc\{lookup\}\}\.\\textsc\{Prove\}\\left\(\(z\_\{1\},s\_\{1\}^\{\\prime\}\),\(z\_\{2\},s\_\{2\}^\{\\prime\}\)\\in T\_\{\\sigma^\{\\prime\}\}\\right\)\.

5:

Πlookup\.Prove​\(a¯​l\+b¯−sl≥0\)\.\\Pi\_\{\\textsc\{lookup\}\}\.\\textsc\{Prove\}\(\\overline\{a\}l\+\\overline\{b\}\-s\_\{l\}\\geq 0\)\.⊳\\trianglerightLeft endpoint

6:

Πlookup\.Prove​\(a¯​u\+b¯−su≥0\)\\Pi\_\{\\textsc\{lookup\}\}\.\\textsc\{Prove\}\(\\overline\{a\}u\+\\overline\{b\}\-s\_\{u\}\\geq 0\)\.⊳\\trianglerightRight endpoint

7:

Πlookup\.Prove​\(z1≤0\)\\Pi\_\{\\textsc\{lookup\}\}\.\\textsc\{Prove\}\(z\_\{1\}\\leq 0\)and

Πlookup\.Prove​\(z2≥0\)\\Pi\_\{\\textsc\{lookup\}\}\.\\textsc\{Prove\}\(z\_\{2\}\\geq 0\)\.⊳\\trianglerightTangency point ordering

8:

Πarith\.Prove​\(si′=a¯\)\\Pi\_\{\\textsc\{arith\}\}\.\\textsc\{Prove\}\(s\_\{i\}^\{\\prime\}=\\overline\{a\}\)for

i∈\{1,2\}i\\in\\\{1,2\\\}\.⊳\\trianglerightTangency point correctness

9:

Πlookup\.Prove​\(a¯​z1\+b¯−s1≥0\)\\Pi\_\{\\textsc\{lookup\}\}\.\\textsc\{Prove\}\(\\overline\{a\}z\_\{1\}\+\\overline\{b\}\-s\_\{1\}\\geq 0\)\.⊳\\trianglerightLeft tangency condition

10:

Πlookup\.Prove​\(\(u−z2\)​\(a¯​z2\+b¯−s2\)≥0\)\\Pi\_\{\\textsc\{lookup\}\}\.\\textsc\{Prove\}\\left\(\(u\-z\_\{2\}\)\(\\overline\{a\}z\_\{2\}\+\\overline\{b\}\-s\_\{2\}\)\\geq 0\\right\)\.⊳\\trianglerightRight tangency condition

11:returnall proofs generated\.

Algorithm 3The PANDA prover\.1:Public statement\.Input point

𝒙0∈ℝn0\\boldsymbol\{x\}\_\{0\}\\in\\mathbb\{R\}^\{n\_\{0\}\}, perturbation budget

ε\>0\\varepsilon\>0, model architecture, robustness claim

\(𝐂,𝒖\)\(\\mathbf\{C\},\\boldsymbol\{u\}\), and commitments to witnesses\.

2:Private witnesses\.Model parameters

\{𝐖\(k\),𝒃\(k\)\}k=1m\\\{\\mathbf\{W\}^\{\(k\)\},\\boldsymbol\{b\}^\{\(k\)\}\\\}\_\{k=1\}^\{m\}and all values in the quantized CROWN transcript \(Section[4](https://arxiv.org/html/2608.17070#S4)\) generated by running Algorithm[1](https://arxiv.org/html/2608.17070#alg1)\.

𝒫\\mathcal\{P\}commits to the witnesses via

Πcom\\Pi\_\{\\textsc\{com\}\}\.

3:Prover claim\.

∀𝒙∈𝔹⁡\(𝒙0,ε\),𝐂​f​\(𝒙\)≤𝒖\\forall\\boldsymbol\{x\}\\in\\mathbb\{B\}\(\\boldsymbol\{x\}\_\{0\},\\varepsilon\),\\;\\mathbf\{C\}f\(\\boldsymbol\{x\}\)\\leq\\boldsymbol\{u\}\.

4:Proof\.

𝒫\\mathcal\{P\}runs Algorithm[1](https://arxiv.org/html/2608.17070#alg1), accumulating the following proofs along the way in a list

Π\\Pi:

5:\(1\) Signed components\.For each call

𝐀\+←max⁡\(𝐀,0\),𝐀−←min⁡\(𝐀,0\)\\mathbf\{A\}\_\{\+\}\\leftarrow\\max\(\\mathbf\{A\},0\),\\;\\mathbf\{A\}\_\{\-\}\\leftarrow\\min\(\\mathbf\{A\},0\):

6:

π\+←Πlookup\.Prove​\(\(𝐀,𝐀\+\)⊂TReLU\)\\pi\_\{\+\}\\leftarrow\\Pi\_\{\\textsc\{lookup\}\}\.\\textsc\{Prove\}\\bigl\(\(\\mathbf\{A\},\\mathbf\{A\}\_\{\+\}\)\\subset T\_\{\\mathrm\{ReLU\}\}\\bigr\)
7:

π−←Πlookup\.Prove​\(\(−𝐀,−𝐀−\)⊂TReLU\)\\pi\_\{\-\}\\leftarrow\\Pi\_\{\\textsc\{lookup\}\}\.\\textsc\{Prove\}\\bigl\(\(\-\\mathbf\{A\},\-\\mathbf\{A\}\_\{\-\}\)\\subset T\_\{\\mathrm\{ReLU\}\}\\bigr\)
8:

Π←Π∪\{π\+,π−\}\\Pi\\leftarrow\\Pi\\cup\\\{\\pi\_\{\+\},\\pi\_\{\-\}\\\}
9:\(2\) Activation\-relaxation update\.For each call

\(𝐀′,𝒅′\)←Step1​\(𝐀,𝒅,ℓ\)\(\\mathbf\{A\}^\{\\prime\},\\boldsymbol\{d\}^\{\\prime\}\)\\leftarrow\\textsc\{Step1\}\(\\mathbf\{A\},\\boldsymbol\{d\},\\ell\):

10:

π1←Πarith\.Prove​\(𝐀′=𝐀\+​diag​\(𝒂¯\(ℓ\)\)\+𝐀−​diag​\(𝒂¯\(ℓ\)\)\)\\pi\_\{1\}\\leftarrow\\Pi\_\{\\textsc\{arith\}\}\.\\textsc\{Prove\}\\bigl\(\\mathbf\{A\}^\{\\prime\}=\\mathbf\{A\}\_\{\+\}\\,\\mathrm\{diag\}\(\\boldsymbol\{\\overline\{a\}\}^\{\(\\ell\)\}\)\+\\mathbf\{A\}\_\{\-\}\\,\\mathrm\{diag\}\(\\boldsymbol\{\\underline\{a\}\}^\{\(\\ell\)\}\)\\bigr\)
11:

π2←Πarith\.Prove​\(𝒅′=𝒅\+𝐀\+​𝒃¯\(ℓ\)\+𝐀−​𝒃¯\(ℓ\)\)\\pi\_\{2\}\\leftarrow\\Pi\_\{\\textsc\{arith\}\}\.\\textsc\{Prove\}\\bigl\(\\boldsymbol\{d\}^\{\\prime\}=\\boldsymbol\{d\}\+\\mathbf\{A\}\_\{\+\}\\,\\boldsymbol\{\\overline\{b\}\}^\{\(\\ell\)\}\+\\mathbf\{A\}\_\{\-\}\\,\\boldsymbol\{\\underline\{b\}\}^\{\(\\ell\)\}\\bigr\)
12:

Π←Π∪\{π1,π2\}\\Pi\\leftarrow\\Pi\\cup\\\{\\pi\_\{1\},\\pi\_\{2\}\\\}
13:\(3\) Linear\-map substitution\.For each call

\(𝐀′,𝒅′\)←Step2​\(𝐀,𝒅,ℓ\)\(\\mathbf\{A\}^\{\\prime\},\\boldsymbol\{d\}^\{\\prime\}\)\\leftarrow\\textsc\{Step2\}\(\\mathbf\{A\},\\boldsymbol\{d\},\\ell\):

14:

π3←Πarith\.Prove​\(𝐀′=𝐀​𝐖\(ℓ\)\)\\pi\_\{3\}\\leftarrow\\Pi\_\{\\textsc\{arith\}\}\.\\textsc\{Prove\}\\bigl\(\\mathbf\{A\}^\{\\prime\}=\\mathbf\{A\}\\,\\mathbf\{W\}^\{\(\\ell\)\}\\bigr\)
15:

π4←Πarith\.Prove​\(𝒅′=𝒅\+𝐀​𝒃\(ℓ\)\)\\pi\_\{4\}\\leftarrow\\Pi\_\{\\textsc\{arith\}\}\.\\textsc\{Prove\}\\bigl\(\\boldsymbol\{d\}^\{\\prime\}=\\boldsymbol\{d\}\+\\mathbf\{A\}\\,\\boldsymbol\{b\}^\{\(\\ell\)\}\\bigr\)
16:

Π←Π∪\{π3,π4\}\\Pi\\leftarrow\\Pi\\cup\\\{\\pi\_\{3\},\\pi\_\{4\}\\\}
17:\(4\) Concretization\.For each call

\(𝑳,𝑼\)←Concretize​\(𝐀¯,𝒅¯,𝐀¯,𝒅¯,𝒙0,ε\)\(\\boldsymbol\{L\},\\boldsymbol\{U\}\)\\leftarrow\\textsc\{Concretize\}\(\\underline\{\\mathbf\{A\}\},\\boldsymbol\{\\underline\{d\}\},\\overline\{\\mathbf\{A\}\},\\boldsymbol\{\\overline\{d\}\},\\boldsymbol\{x\}\_\{0\},\\varepsilon\):

18:call\(1\) Signed componentsfor

𝐀¯,𝐀¯\\overline\{\\mathbf\{A\}\},\\underline\{\\mathbf\{A\}\}
19:

π5←Πarith\.Prove​\(𝑼=𝐀¯\+​\(𝒙0\+ε​𝟏\)\+𝐀¯−​\(𝒙0−ε​𝟏\)\+𝒅¯\)\\pi\_\{5\}\\leftarrow\\Pi\_\{\\textsc\{arith\}\}\.\\textsc\{Prove\}\\bigl\(\\boldsymbol\{U\}=\\overline\{\\mathbf\{A\}\}\_\{\+\}\(\\boldsymbol\{x\}\_\{0\}\+\\varepsilon\\mathbf\{1\}\)\+\\overline\{\\mathbf\{A\}\}\_\{\-\}\(\\boldsymbol\{x\}\_\{0\}\-\\varepsilon\\mathbf\{1\}\)\+\\boldsymbol\{\\overline\{d\}\}\\bigr\)
20:

π6←Πarith\.Prove​\(𝑳=𝐀¯\+​\(𝒙0−ε​𝟏\)\+𝐀¯−​\(𝒙0\+ε​𝟏\)\+𝒅¯\)\\pi\_\{6\}\\leftarrow\\Pi\_\{\\textsc\{arith\}\}\.\\textsc\{Prove\}\\bigl\(\\boldsymbol\{L\}=\\underline\{\\mathbf\{A\}\}\_\{\+\}\(\\boldsymbol\{x\}\_\{0\}\-\\varepsilon\\mathbf\{1\}\)\+\\underline\{\\mathbf\{A\}\}\_\{\-\}\(\\boldsymbol\{x\}\_\{0\}\+\\varepsilon\\mathbf\{1\}\)\+\\boldsymbol\{\\underline\{d\}\}\\bigr\)
21:

Π←Π∪\{π5,π6\}\\Pi\\leftarrow\\Pi\\cup\\\{\\pi\_\{5\},\\pi\_\{6\}\\\}
22:\(5\) Activation relaxation\.For each call

\(a¯,b¯,a¯,b¯\)←Relax​\(σ,𝑳,𝑼\)\(\\overline\{a\},\\overline\{b\},\\underline\{a\},\\underline\{b\}\)\\leftarrow\\textsc\{Relax\}\(\\sigma,\\boldsymbol\{L\},\\boldsymbol\{U\}\):

23:

πu←Relaxation\-Gadget​\(σ,𝑳,𝑼,a¯,b¯\)\\pi\_\{u\}\\leftarrow\\textsc\{Relaxation\-Gadget\}\(\\sigma,\\boldsymbol\{L\},\\boldsymbol\{U\},\\overline\{a\},\\overline\{b\}\)⊳\\trianglerightcalls upper bound Alg\.[2](https://arxiv.org/html/2608.17070#alg2)

24:

πl←Relaxation\-Gadget​\(σ,𝑳,𝑼,a¯,b¯\)\\pi\_\{l\}\\leftarrow\\textsc\{Relaxation\-Gadget\}\(\\sigma,\\boldsymbol\{L\},\\boldsymbol\{U\},\\underline\{a\},\\underline\{b\}\)⊳\\trianglerightlower bound is analogous

25:

Π←Π∪\{πu,πl\}\\Pi\\leftarrow\\Pi\\cup\\\{\\pi\_\{u\},\\pi\_\{l\}\\\}
26:\(6\) Final robustness claim\.After Algorithm[1](https://arxiv.org/html/2608.17070#alg1)terminates at layer

mm,

𝒫\\mathcal\{P\}proves that the final concretized upper bound

𝑼\(m\)\\boldsymbol\{U\}^\{\(m\)\}is at most

𝒖\\boldsymbol\{u\}entry\-wise via a range proof\.

27:

πfinal←Πlookup\.Prove​\(𝒖−𝑼\(m\)≥0\)\\pi\_\{\\mathrm\{final\}\}\\leftarrow\\Pi\_\{\\textsc\{lookup\}\}\.\\textsc\{Prove\}\(\\boldsymbol\{u\}\-\\boldsymbol\{U\}^\{\(m\)\}\\geq 0\)
28:

Π←Π∪\{πfinal\}\\Pi\\leftarrow\\Pi\\cup\\\{\\pi\_\{\\mathrm\{final\}\}\\\}
29:\(7\) Quantization rescaling\.For each rescaling

qz=⌊Sz​qx/Sx⌋q\_\{z\}=\\left\\lfloor S\_\{z\}q\_\{x\}/S\_\{x\}\\right\\rfloorwith committed remainder

rr:

30:

πrem←Πlookup\.Prove​\(0≤r<Sx\)\\pi\_\{\\mathrm\{rem\}\}\\leftarrow\\Pi\_\{\\textsc\{lookup\}\}\.\\textsc\{Prove\}\(0\\leq r<S\_\{x\}\)⊳\\trianglerightThis is rewritten asr≥0∧Sx−r\>0r\\geq 0\\wedge S\_\{x\}\-r\>0\.

31:

πdiv←Πarith\.Prove​\(Sz​qx=Sx​qz\+r\)\\pi\_\{\\mathrm\{div\}\}\\leftarrow\\Pi\_\{\\textsc\{arith\}\}\.\\textsc\{Prove\}\(S\_\{z\}q\_\{x\}=S\_\{x\}q\_\{z\}\+r\)
32:

Π←Π∪\{πrem,πdiv\}\\Pi\\leftarrow\\Pi\\cup\\\{\\pi\_\{\\mathrm\{rem\}\},\\pi\_\{\\mathrm\{div\}\}\\\}
33:return

Π\\Pi

Algorithm 4The PANDA verifier\.1:Public statement

xxand proof

Π\\Pifrom Algorithm[3](https://arxiv.org/html/2608.17070#alg3)\.

2:foreach proof

π←Πarith\.Prove\\pi\\leftarrow\\Pi\_\{\\textsc\{arith\}\}\.\\textsc\{Prove\}in

Π\\Pido

3:run

Πarith\.Verify​\(x,π\)\\Pi\_\{\\textsc\{arith\}\}\.\\textsc\{Verify\}\(x,\\pi\)
4:endfor

5:foreach proof

π←Πlookup\.Prove\\pi\\leftarrow\\Pi\_\{\\textsc\{lookup\}\}\.\\textsc\{Prove\}in

Π\\Pido

6:run

Πlookup\.Verify​\(x,π\)\\Pi\_\{\\textsc\{lookup\}\}\.\\textsc\{Verify\}\(x,\\pi\)
7:endfor

8:foreach relaxation\-gadget proof

π∈Π\\pi\\in\\Pido

9:run

Verify\-Relaxation\-Gadget​\(x,π\)\\textsc\{Verify\-Relaxation\-Gadget\}\(x,\\pi\)
10:endfor

11:acceptiff every check above passes

## Appendix CComparison with FairProof

FairProof\[[31](https://arxiv.org/html/2608.17070#bib.bib17)\]is the only suitable direct comparison, since it is the only ZKP system that certifies local robustness, to the best of our knowledge\. We evaluate FairProof’s own system head\-to\-head with PANDA on shared benchmarks: the FairProof Adult model and our smallest MNIST models on the first 5 properties PANDA proves\. FairProof’s offline phase was never released, so we reimplemented it and validated it against their released example, using a single core and the same CPUs as in PANDA’s evaluation\. We present the results in Table[2](https://arxiv.org/html/2608.17070#A3.T2)\.

Where FairProof runs \(only on FairProof Adult\), PANDA requires about half \(34\.89s\) of FairProof’s prover time \(66\.0s in total\)\. FairProof’s verifier time is smaller, but PANDA’s is still on the order of seconds\. However, FairProof cannot scale to any of the larger MNIST models\.

Table 2:FairProof’s performance on small benchmarks\.ModelOffline prove \(s\)Online prove \(s\)Verify \(s\)Proof \(KB\)FairProof Adult9\.29\.256\.856\.80\.020\.0219\.119\.1MNIST2×\[20\]2\\times\[20\]ReLU1908\.0†1908\.0^\{\\dagger\}4/5 timeout \(\>\>1h\),1/5 OOM \(\>\>512GiB\)——MNIST3×\[20\]3\\times\[20\]ReLUtimeout \(\>\>12h\)———MNIST2×\[1024\]2\\times\[1024\]ReLUtimeout \(\>\>12h\)———
- †\\daggerThe offline phase completed, but the online phase was killed\.

## Appendix DComplete Evaluation

Table 3:Evaluation\. Each row is one model\. \(adv\.\) denotes adversarially trained models\. 100 tests are run for each model, except for FairProof \(only one test is run\) and MNIST \(only images correctly classified by the model are tested\)\. Prove/verify times showμ±σ\\mu\\pm\\sigma\(mean and standard deviation\) over the verified subset only\. N is the number of benchmarks evaluated for each model, which is also the number of properties that CROWN certifies for that model\.DatasetStructureAct\.Prove \(s\)Verify \(s\)ProofCROWNDriftN\(MB\)\(s\)\(%\)MNIST2×\[20\]2\\times\[20\]ReLU22\.81±2022\.81\\pm 200\.97±10\.97\\pm 130\.000130\.02972×\[20\]2\\times\[20\]Sigmoid58\.35±8158\.35\\pm 812\.33±32\.33\\pm 380\.000140\.19942×\[20\]2\\times\[20\]Tanh58\.77±3958\.77\\pm 392\.34±32\.34\\pm 380\.000140\.16973×\[20\]3\\times\[20\]ReLU42\.64±5142\.64\\pm 511\.90±31\.90\\pm 360\.000180\.04953×\[20\]3\\times\[20\]Sigmoid99\.62±12099\.62\\pm 1204\.21±54\.21\\pm 5140\.000220\.55933×\[20\]3\\times\[20\]Tanh105\.56±233105\.56\\pm 2334\.46±104\.46\\pm 10150\.000190\.40932×\[1024\]2\\times\[1024\]ReLU41\.70±7241\.70\\pm 721\.69±21\.69\\pm 240\.060\.02982×\[1024\]2\\times\[1024\]Sigmoid74\.60±14974\.60\\pm 1493\.26±63\.26\\pm 690\.060\.62992×\[1024\]2\\times\[1024\]Tanh83\.17±33883\.17\\pm 3383\.63±153\.63\\pm 1590\.070\.39983×\[1024\]3\\times\[1024\]\(adv\.\)ReLU90\.79±4490\.79\\pm 444\.68±34\.68\\pm 390\.22\-0\.18973×\[1024\]3\\times\[1024\]ReLU101\.58±375101\.58\\pm 3754\.60±134\.60\\pm 1390\.220\.03983×\[1024\]3\\times\[1024\]Sigmoid172\.29±304172\.29\\pm 3047\.76±147\.76\\pm 14190\.211\.66983×\[1024\]3\\times\[1024\]Tanh179\.27±326179\.27\\pm 3267\.83±157\.83\\pm 15200\.211\.83984×\[1024\]4\\times\[1024\]\(adv\.\)ReLU172\.16±389172\.16\\pm 3898\.96±158\.96\\pm 15160\.450\.01984×\[1024\]4\\times\[1024\]ReLU226\.08±1467226\.08\\pm 14679\.56±489\.56\\pm 48170\.44\-0\.011004×\[1024\]4\\times\[1024\]Sigmoid327\.47±1136327\.47\\pm 113614\.13±4614\.13\\pm 46310\.472\.48974×\[1024\]4\\times\[1024\]Tanh333\.94±581333\.94\\pm 58114\.31±2814\.31\\pm 28320\.466\.3399OtherSafeNLP med2×\[128\]2\\times\[128\]ReLU23\.04±1923\.04\\pm 190\.81±10\.81\\pm 130\.00013\-0\.0554SafeNLP robot2×\[128\]2\\times\[128\]ReLU20\.33±1920\.33\\pm 190\.78±10\.78\\pm 130\.00014\-0\.293LunarLander3×\[64\]3\\times\[64\]ReLU36\.61±2936\.61\\pm 291\.46±21\.46\\pm 258\.1e\-5\-0\.0918FairProof Adult\[8,2\]\[8,2\]ReLU34\.8934\.891\.211\.2141\.4e\-5\-12\.601Table 4:Component\-wise breakdown of the prover time\.commit= polynomial commitments to every witness \(Hyrax\[[28](https://arxiv.org/html/2608.17070#bib.bib14)\]\);matmul= the matrix\-multiplication verification \(\[[26](https://arxiv.org/html/2608.17070#bib.bib15)\]\);lookup= all lookup arguments \(LogUp\-GKR\[[21](https://arxiv.org/html/2608.17070#bib.bib13)\]\);other= other cryptographic computation; total in Cryptographic = the sum of the four preceding columns; total in Non\-crypto = total non\-cryptographic computation time of the prover \(including the plaintext quantized\-CROWN that generates witnesses\);tangent= time for computing the tangent points used in linear relaxations of S\-shaped activation functions, which is a part of total in \. Upper panel: absolute times; lower panel: shares ofprove\. Note the unit change ontangent\.CryptographicNon\-cryptoStructureAct\.provecommitmatmullookupothertotaltangenttotal*Absolute time \(s\);tangentin ms*3×\[20\]3\\times\[20\]ReLU45\.080\.930\.3543\.590\.2145\.070\.0000\.013×\[20\]3\\times\[20\]Sigmoid92\.340\.860\.3390\.250\.8992\.330\.0090\.013×\[20\]3\\times\[20\]Tanh116\.450\.940\.36113\.271\.87116\.440\.0130\.013×\[1024\]3\\times\[1024\]ReLU106\.9515\.708\.5466\.080\.5190\.820\.00016\.123×\[1024\]3\\times\[1024\]Sigmoid170\.1316\.178\.50127\.502\.70154\.860\.02215\.263×\[1024\]3\\times\[1024\]Tanh196\.8020\.6210\.49144\.393\.42178\.910\.64617\.84*As % ofprove\(provein s\)*3×\[20\]3\\times\[20\]ReLU45\.082\.10\.896\.70\.5100\.0<<0\.010\.03×\[20\]3\\times\[20\]Sigmoid92\.340\.90\.497\.71\.0100\.0<<0\.010\.03×\[20\]3\\times\[20\]Tanh116\.450\.80\.397\.31\.6100\.0<<0\.010\.03×\[1024\]3\\times\[1024\]ReLU106\.9514\.78\.061\.80\.584\.9<<0\.0115\.13×\[1024\]3\\times\[1024\]Sigmoid170\.139\.55\.074\.91\.691\.0<<0\.019\.03×\[1024\]3\\times\[1024\]Tanh196\.8010\.55\.373\.41\.790\.9<<0\.019\.1
## Appendix EProver Breakdown

We provide the component\-wise breakdown of the prover time for three MNIST3×\[20\]3\\times\[20\]models and three MNIST3×\[1024\]3\\times\[1024\]models in Table[4](https://arxiv.org/html/2608.17070#A4.T4)\. Every row shows the mean over the first55properties PANDA proves\.

We identify the largest component as the lookup arguments, but we still observe that all components scale polynomially in the size of the network, which aligns with the theoretical guarantees of these cryptographic protocols\.

## Appendix FOptimization: Finite Differences

The Four\-Point Relaxation Gadget presented in Algorithm[2](https://arxiv.org/html/2608.17070#alg2)requires lookup proofs against both the tableTσ=\{\(z,σ⁡\(z\)\)\}T\_\{\\sigma\}=\\\{\\left\(z,\\sigma\(z\)\\right\)\\\}and the tableTσ′=\{\(z,σ′​\(z\)\)\}T\_\{\\sigma^\{\\prime\}\}=\\\{\\left\(z,\\sigma^\{\\prime\}\(z\)\\right\)\\\}for its derivative\. TheTσ′T\_\{\\sigma^\{\\prime\}\}checks are equalities, which are more brittle in the quantized setting than inequalities, and precomputing both tables is a memory bottleneck\. We therefore eliminate theTσ′T\_\{\\sigma^\{\\prime\}\}table using the technique of finite differences\. We use an additional condition thatσ\\sigmais strictly increasing\.

To prove thatσ′​\(z\)=α\\sigma^\{\\prime\}\(z\)=\\alphafor fixedz∈ℝ,α∈\(0,B\]z\\in\\mathbb\{R\},\\alpha\\in\(0,B\]up to some quantization error, it suffices to find a nearbyz0∈\(z−δ,z\+δ\)z\_\{0\}\\in\(z\-\\delta,z\+\\delta\)satisfying

σ⁡\(z0\)−σ⁡\(z0−δ\)δ≤α≤σ⁡\(z0\+δ\)−σ⁡\(z0\)δ\\frac\{\\sigma\(z\_\{0\}\)\-\\sigma\(z\_\{0\}\-\\delta\)\}\{\\delta\}\\leq\\alpha\\leq\\frac\{\\sigma\(z\_\{0\}\+\\delta\)\-\\sigma\(z\_\{0\}\)\}\{\\delta\}\(20\)whereδ\\deltais an error threshold determined by the quantization; whenσ\\sigmais concave nearzz, the inequalities in \([20](https://arxiv.org/html/2608.17070#A6.E20)\) are reversed\. Equation \([20](https://arxiv.org/html/2608.17070#A6.E20)\) can be encoded in Algorithm[2](https://arxiv.org/html/2608.17070#alg2)using only the lookup tables forσ\\sigma\. The following theorem demonstrates the sufficiency of \([20](https://arxiv.org/html/2608.17070#A6.E20)\)\.

###### Theorem F\.1\(Finite differences\)\.

Letσ\\sigmasatisfy Assumption[5\.1](https://arxiv.org/html/2608.17070#S5.Thmassumption1)and also be strictly increasing and letδ\>0\.\\delta\>0\.Let𝒟\\mathcal\{D\}be the set of values exactly represented in our quantization, and suppose that the points of𝒟\\mathcal\{D\}are uniformly spaced with spacing at mostδ\\delta\.

- •Ifσ′​\(z\)=α\\sigma^\{\\prime\}\(z\)=\\alphaandσ\\sigmais convex over\(z−δ,z\+δ\)\(z\-\\delta,z\+\\delta\), then there exists somez0∈𝒟∩\(z−δ,z\+δ\)z\_\{0\}\\in\\mathcal\{D\}\\cap\(z\-\\delta,z\+\\delta\)such thatσ⁡\(z0\)−σ⁡\(z0−δ\)≤δ​α\\sigma\(z\_\{0\}\)\-\\sigma\(z\_\{0\}\-\\delta\)\\leq\\delta\\alphaandσ⁡\(z0\+δ\)−σ⁡\(z0\)≥δ​α\\sigma\(z\_\{0\}\+\\delta\)\-\\sigma\(z\_\{0\}\)\\geq\\delta\\alpha\.
- •Ifσ′​\(z\)=α\\sigma^\{\\prime\}\(z\)=\\alphaandσ\\sigmais concave over\(z−δ,z\+δ\)\(z\-\\delta,z\+\\delta\), then there exists somez0∈𝒟∩\(z−δ,z\+δ\)z\_\{0\}\\in\\mathcal\{D\}\\cap\(z\-\\delta,z\+\\delta\)such thatσ⁡\(z0\)−σ⁡\(z0−δ\)≥δ​α\\sigma\(z\_\{0\}\)\-\\sigma\(z\_\{0\}\-\\delta\)\\geq\\delta\\alphaandσ⁡\(z0\+δ\)−σ⁡\(z0\)≤δ​α\\sigma\(z\_\{0\}\+\\delta\)\-\\sigma\(z\_\{0\}\)\\leq\\delta\\alpha\.

Conversely, ifsign⁡\(σ⁡\(z0\)−σ⁡\(z0−δ\)−δ​α\)≠sign⁡\(σ⁡\(z0\+δ\)−σ⁡\(z0\)−δ​α\)\\operatorname\{sign\}\(\\sigma\(z\_\{0\}\)\-\\sigma\(z\_\{0\}\-\\delta\)\-\\delta\\alpha\)\\neq\\operatorname\{sign\}\(\\sigma\(z\_\{0\}\+\\delta\)\-\\sigma\(z\_\{0\}\)\-\\delta\\alpha\)then there exists somez∈\(z0−δ,z0\+δ\)z\\in\(z\_\{0\}\-\\delta,z\_\{0\}\+\\delta\)such thatσ′​\(z\)=α\.\\sigma^\{\\prime\}\(z\)=\\alpha\.

###### Proof\.

Consider the first statement\. Define the finite difference functionsf⁡\(x\)=σ⁡\(x\)−σ⁡\(x−δ\)f\(x\)=\\sigma\(x\)\-\\sigma\(x\-\\delta\)andg⁡\(x\)=σ⁡\(x\+δ\)−σ⁡\(x\)g\(x\)=\\sigma\(x\+\\delta\)\-\\sigma\(x\)\. Sinceσ\\sigmais convex over\(z−δ,z\+δ\)\(z\-\\delta,z\+\\delta\), and its derivativeσ′\\sigma^\{\\prime\}is strictly increasing over this region, which implies thatf⁡\(x\)f\(x\)andg⁡\(x\)g\(x\)are also strictly increasing\.

By the Mean Value Theorem, there exists somec1∈\(z−δ,z\)c\_\{1\}\\in\(z\-\\delta,z\)such thatf⁡\(z\)=δ​σ′​\(c1\)f\(z\)=\\delta\\sigma^\{\\prime\}\(c\_\{1\}\)\. Sincec1<zc\_\{1\}<zandσ′\\sigma^\{\\prime\}is increasing,σ′​\(c1\)≤σ′​\(z\)=α\\sigma^\{\\prime\}\(c\_\{1\}\)\\leq\\sigma^\{\\prime\}\(z\)=\\alpha, givingf⁡\(z\)≤δ​αf\(z\)\\leq\\delta\\alpha\. Similarly, there existsc2∈\(z,z\+δ\)c\_\{2\}\\in\(z,z\+\\delta\)such thatg⁡\(z\)=δ​σ′​\(c2\)g\(z\)=\\delta\\sigma^\{\\prime\}\(c\_\{2\}\)\. Sincec2\>zc\_\{2\}\>z,σ′​\(c2\)≥σ′​\(z\)=α\\sigma^\{\\prime\}\(c\_\{2\}\)\\geq\\sigma^\{\\prime\}\(z\)=\\alpha, yieldingg⁡\(z\)≥δ​αg\(z\)\\geq\\delta\\alpha\.

DefineA=f−1\(\(−∞,δα\]\)A=f^\{\-1\}\(\(\-\\infty,\\delta\\alpha\]\)andB=g−1​\(\[δ​α,∞\)\)B=g^\{\-1\}\(\[\\delta\\alpha,\\infty\)\)\. Sinceffandggare increasing and continuous,A=\(−∞,z\+\]A=\(\-\\infty,z\_\{\+\}\]andB=\[z−,∞\)B=\[z\_\{\-\},\\infty\)for somez−,z\+z\_\{\-\},z\_\{\+\}which satisfyf⁡\(z\+\)=δ​α=g⁡\(z−\)f\(z\_\{\+\}\)=\\delta\\alpha=g\(z\_\{\-\}\)\. Also,z∈A∩Bz\\in A\\cap B, soz−≤z\+z\_\{\-\}\\leq z\_\{\+\}andA∩B=\[z−,z\+\]A\\cap B=\[z\_\{\-\},z\_\{\+\}\]\. Now observe thatg⁡\(x\)=f⁡\(x\+δ\)g\(x\)=f\(x\+\\delta\)is simply a translation, which implies thatg⁡\(z\+−δ\)=f⁡\(z\+\)=δ​αg\(z\_\{\+\}\-\\delta\)=f\(z\_\{\+\}\)=\\delta\\alpha\. Sinceggis strictly increasing,z−z\_\{\-\}is the unique point withg⁡\(z−\)=δ​αg\(z\_\{\-\}\)=\\delta\\alpha, soz−=z\+−δz\_\{\-\}=z\_\{\+\}\-\\deltaandA∩B=\[z−,z\+\]A\\cap B=\[z\_\{\-\},z\_\{\+\}\]is of lengthδ\\delta\. Since the points of𝒟\\mathcal\{D\}are spaced at mostδ\\deltaapart, there exists some pointz0∈𝒟z\_\{0\}\\in\\mathcal\{D\}withinA∩BA\\cap B, and thisz0z\_\{0\}therefore satisfiesf⁡\(z0\)=σ⁡\(z0\)−σ⁡\(z0−δ\)≤δ​αf\(z\_\{0\}\)=\\sigma\(z\_\{0\}\)\-\\sigma\(z\_\{0\}\-\\delta\)\\leq\\delta\\alphaandg⁡\(z0\)=σ⁡\(z0\+δ\)−σ⁡\(z0\)≥δ​α\.g\(z\_\{0\}\)=\\sigma\(z\_\{0\}\+\\delta\)\-\\sigma\(z\_\{0\}\)\\geq\\delta\\alpha\.

The second statement follows analogously, whereσ′,f,\\sigma^\{\\prime\},f,andggare all instead decreasing\.

Now consider the converse statement\. Without loss of generality, suppose that

σ⁡\(z0\)−σ⁡\(z0−δ\)−α​δ≤0andσ⁡\(z0\+δ\)−σ⁡\(z0\)−α​δ≥0\.\\sigma\(z\_\{0\}\)\-\\sigma\(z\_\{0\}\-\\delta\)\-\\alpha\\delta\\leq 0\\quad\\text\{and\}\\quad\\sigma\(z\_\{0\}\+\\delta\)\-\\sigma\(z\_\{0\}\)\-\\alpha\\delta\\geq 0\.By rearranging, we obtain

σ⁡\(z0\)−σ⁡\(z0−δ\)z0−\(z0−δ\)≤αandσ⁡\(z0\+δ\)−σ⁡\(z0\)\(z0\+δ\)−z0≥α\.\\frac\{\\sigma\(z\_\{0\}\)\-\\sigma\(z\_\{0\}\-\\delta\)\}\{z\_\{0\}\-\(z\_\{0\}\-\\delta\)\}\\leq\\alpha\\quad\\text\{and\}\\quad\\frac\{\\sigma\(z\_\{0\}\+\\delta\)\-\\sigma\(z\_\{0\}\)\}\{\(z\_\{0\}\+\\delta\)\-z\_\{0\}\}\\geq\\alpha\.Then by the Mean Value Theorem, there exist somez0−∈\(z0−δ,z0\)z\_\{0\}^\{\-\}\\in\(z\_\{0\}\-\\delta,z\_\{0\}\)andz0\+∈\(z0,z0\+δ\)z\_\{0\}^\{\+\}\\in\(z\_\{0\},z\_\{0\}\+\\delta\)such thatσ′​\(z0−\)≤α\\sigma^\{\\prime\}\(z\_\{0\}^\{\-\}\)\\leq\\alphaandσ′​\(z0\+\)≥α\.\\sigma^\{\\prime\}\(z\_\{0\}^\{\+\}\)\\geq\\alpha\.By the Intermediate Value Theorem applied toσ′\\sigma^\{\\prime\}, there must be somez∈\(z0−,z0\+\)⊂\(z0−δ,z0\+δ\)z\\in\(z\_\{0\}^\{\-\},z\_\{0\}^\{\+\}\)\\subset\(z\_\{0\}\-\\delta,z\_\{0\}\+\\delta\)such thatσ′​\(z\)=α\.\\sigma^\{\\prime\}\(z\)=\\alpha\.The case where the signs are flipped follows similarly\. ∎

Instantiation in Algorithm[2](https://arxiv.org/html/2608.17070#alg2)\. This theorem shows that one can select a witness valuez0z\_\{0\}in our quantization which satisfies the above conditions, andz0z\_\{0\}will be aδ\\delta\-approximation of the solutionzzsatisfyingσ′​\(z\)=α\.\\sigma^\{\\prime\}\(z\)=\\alpha\.For cases whereσ\\sigmais neither concave nor convex over\(z−δ,z\+δ\)\(z\-\\delta,z\+\\delta\), it suffices to pickz0=0z\_\{0\}=0as aδ\\delta\-approximation\. Notably, these conditions only depend onσ\\sigmaand notσ′\.\\sigma^\{\\prime\}\.This optimization can be encoded in Algorithm[2](https://arxiv.org/html/2608.17070#alg2)\.

## Appendix GProof of Lemma[5\.1](https://arxiv.org/html/2608.17070#S5.Thmlemma1)

###### Proof\.

By assumption,σ\\sigmais convex on\(−∞,0\)\(\-\\infty,0\)and concave on\(0,\+∞\)\.\(0,\+\\infty\)\.Thus,σ′\\sigma^\{\\prime\}is continuous, bounded below by 0, strictly increasing on\(−∞,0\)\(\-\\infty,0\)and strictly decreasing on\(0,\+∞\)\.\(0,\+\\infty\)\.σ′\\sigma^\{\\prime\}attains its maximum atx=0x=0, whereσ′​\(0\)=B\\sigma^\{\\prime\}\(0\)=B\. Additionally, sinceσ\\sigmais bounded, it follows thatlimx→±∞σ′​\(x\)=0\\lim\_\{x\\rightarrow\\pm\\infty\}\\sigma^\{\\prime\}\(x\)=0\. Therefore, by the Intermediate Value Theorem applied toσ′\\sigma^\{\\prime\}, every pointα∈\(0,B\)\\alpha\\in\(0,B\)has oneσ′\\sigma^\{\\prime\}\-preimage in\(−∞,0\)\(\-\\infty,0\)and oneσ′\\sigma^\{\\prime\}\-preimage in\(0,\+∞\)\.\(0,\+\\infty\)\.Forα=B\\alpha=B, the unique preimage isz1=z2=0z\_\{1\}=z\_\{2\}=0, sinceσ′\\sigma^\{\\prime\}attains its maximumBBonly atx=0x=0\. ∎

## Appendix HProof of Theorem[5\.1](https://arxiv.org/html/2608.17070#S5.Thmtheorem1)

Theorem[5\.1](https://arxiv.org/html/2608.17070#S5.Thmtheorem1), part \(a\) \(Case\-free four\-point soundness\)\.Letσ\\sigmasatisfy Assumption[5\.1](https://arxiv.org/html/2608.17070#S5.Thmassumption1), and fix an interval\[l,u\]⊆ℝ\[l,u\]\\subseteq\\mathbb\{R\}\. Consider a candidate linearupper boundhU​\(z\)=a¯​z\+b¯h\_\{U\}\(z\)=\\overline\{a\}z\+\\overline\{b\}witha¯∈\(0,B\]\\overline\{a\}\\in\(0,B\]and two \(possibly coinciding\) points of tangencyz1≤0≤z2z\_\{1\}\\leq 0\\leq z\_\{2\}satisfyingσ′​\(z1\)=σ′​\(z2\)=a¯\\sigma^\{\\prime\}\(z\_\{1\}\)=\\sigma^\{\\prime\}\(z\_\{2\}\)=\\overline\{a\}\. If the following conditions are satisfied, thenhUh\_\{U\}is a valid upper bound on\[l,u\]\[l,u\]\.

- \(i\)Endpoints:σ⁡\(l\)≤hU​\(l\)\\sigma\(l\)\\leq h\_\{U\}\(l\)andσ⁡\(u\)≤hU​\(u\)\\sigma\(u\)\\leq h\_\{U\}\(u\)\.
- \(ii\)Left point of tangency:σ⁡\(z1\)≤hU​\(z1\)\\sigma\(z\_\{1\}\)\\leq h\_\{U\}\(z\_\{1\}\)\.
- \(iii\)Right point of tangency:0≤\(u−z2\)​\(hU​\(z2\)−σ⁡\(z2\)\)0\\leq\(u\-z\_\{2\}\)\\bigl\(h\_\{U\}\(z\_\{2\}\)\-\\sigma\(z\_\{2\}\)\\bigr\)\.

Consider a candidate linearlower boundhL​\(z\)=a¯​z\+b¯h\_\{L\}\(z\)=\\underline\{a\}z\+\\underline\{b\}witha¯∈\(0,B\]\\underline\{a\}\\in\(0,B\]and two \(possibly coinciding\) points of tangencyz1≤0≤z2z\_\{1\}\\leq 0\\leq z\_\{2\}satisfyingσ′​\(z1\)=σ′​\(z2\)=a¯\\sigma^\{\\prime\}\(z\_\{1\}\)=\\sigma^\{\\prime\}\(z\_\{2\}\)=\\underline\{a\}\. If the following conditions are satisfied, thenhLh\_\{L\}is a valid lower bound on\[l,u\]\[l,u\]\.

- \(i\)Endpoints:σ⁡\(l\)≥hL​\(l\)\\sigma\(l\)\\geq h\_\{L\}\(l\)andσ⁡\(u\)≥hL​\(u\)\\sigma\(u\)\\geq h\_\{L\}\(u\)\.
- \(ii\)Right point of tangency:σ⁡\(z2\)≥hL​\(z2\)\\sigma\(z\_\{2\}\)\\geq h\_\{L\}\(z\_\{2\}\)\.
- \(iii\)Left point of tangency:0≤\(z1−l\)​\(σ⁡\(z1\)−hL​\(z1\)\)0\\leq\(z\_\{1\}\-l\)\\bigl\(\\sigma\(z\_\{1\}\)\-h\_\{L\}\(z\_\{1\}\)\\bigr\)\.

###### Proof\.

We prove soundness for the upper bound, and the lower bound is analogous\. Define

f⁡\(z\):=hU​\(z\)−σ⁡\(z\)\.f\(z\):=h\_\{U\}\(z\)\-\\sigma\(z\)\.It suffices to showf≥0f\\geq 0on\[l,u\]\[l,u\]\. SinceffisC1C^\{1\}by Assumption[5\.1](https://arxiv.org/html/2608.17070#S5.Thmassumption1), the critical points offfare the roots off′f^\{\\prime\}given by solving

f′​\(z\)=a¯−σ′​\(z\)=0\.f^\{\\prime\}\(z\)=\\overline\{a\}\-\\sigma^\{\\prime\}\(z\)=0\.By Lemma[5\.1](https://arxiv.org/html/2608.17070#S5.Thmlemma1), there are two such solutionszzwhich we labelz1,z2z\_\{1\},z\_\{2\}\. By the Interior Extremum Theorem, the minimum offfon\[l,u\]\[l,u\]is attained either at an endpoint or at a critical point in\(l,u\)\(l,u\)\. It therefore suffices to showf≥0f\\geq 0atll,uu, and at each critical point that falls inside\[l,u\]\[l,u\]\.

- •Endpoints:f⁡\(l\),f⁡\(u\)≥0f\(l\),f\(u\)\\geq 0by condition \(i\)\.
- •Left critical point:f⁡\(z1\)≥0f\(z\_\{1\}\)\\geq 0by condition \(ii\)\.
- •Right critical point: ifz2∈\[l,u\]z\_\{2\}\\in\[l,u\]: - –ifz2=uz\_\{2\}=u,f⁡\(z2\)=f⁡\(u\)≥0f\(z\_\{2\}\)=f\(u\)\\geq 0by condition \(i\)\. - –ifz2<uz\_\{2\}<u, condition \(iii\) impliesf⁡\(z2\)≥0\.f\(z\_\{2\}\)\\geq 0\.

In all casesf≥0f\\geq 0on\[l,u\]\[l,u\], sohU≥σh\_\{U\}\\geq\\sigmaon\[l,u\]\[l,u\]\. ∎

Theorem[5\.1](https://arxiv.org/html/2608.17070#S5.Thmtheorem1), part \(b\) \(Case\-free four\-point completeness\)\.The CROWN algorithm selects linear relaxationshLh\_\{L\}andhUh\_\{U\}that satisfy the criteria of part \(a\)\.

###### Proof\.

We prove the upper\-bound case, and the lower bound is analogous\. The selection procedure forhU​\(z\)=a¯​z\+b¯h\_\{U\}\(z\)=\\overline\{a\}z\+\\overline\{b\}is described in Appendix[A\.2](https://arxiv.org/html/2608.17070#A1.SS2)\. We verify that each of its three cases produces an upper boundhUh\_\{U\}satisfying conditions \(i\), \(ii\), and \(iii\) of Theorem[5\.1](https://arxiv.org/html/2608.17070#S5.Thmtheorem1)part \(a\)\. Throughout, letz1≤0≤z2z\_\{1\}\\leq 0\\leq z\_\{2\}denote the tangency points satisfyingσ′​\(z1\)=σ′​\(z2\)=a¯\\sigma^\{\\prime\}\(z\_\{1\}\)=\\sigma^\{\\prime\}\(z\_\{2\}\)=\\overline\{a\}\. Letτ\\taudenote the non\-trivial root of

σ′​\(τ\)=σ⁡\(τ\)−σ⁡\(l\)τ−l,\\sigma^\{\\prime\}\(\\tau\)=\\frac\{\\sigma\(\\tau\)\-\\sigma\(l\)\}\{\\tau\-l\},computed in step 1 of the selection procedure\.τ\\tauis the unique value other thanllitself at which the tangent line ofσ⁡\(z\)\\sigma\(z\)atz=τz=\\taucoincides with the secant line through\(l,σ⁡\(l\)\)\(l,\\sigma\(l\)\)and\(τ,σ⁡\(τ\)\)\(\\tau,\\sigma\(\\tau\)\)\.

We will use throughout this proof thatτ\\tauandllmust lie on opposite sides of the inflection point00, and therefore have opposite signs\. This is because any tangent line toσ\\sigmawill also intersectσ\\sigmaon the opposite side of the inflection point00and nowhere else, sinceσ′′\\sigma^\{\\prime\\prime\}changes signs only atz=0\.z=0\.

- •Case 1:τ∈\(l,u\)\\tau\\in\(l,u\)\.The procedure outputs the line hU​\(z\)=σ′​\(τ\)​\(z−τ\)\+σ⁡\(τ\),h\_\{U\}\(z\)=\\sigma^\{\\prime\}\(\\tau\)\(z\-\\tau\)\+\\sigma\(\\tau\),which is simultaneously tangent toσ\\sigmaatz=τz=\\tauand is the secant connecting\(l,σ⁡\(l\)\)\(l,\\sigma\(l\)\)to\(τ,σ⁡\(τ\)\)\(\\tau,\\sigma\(\\tau\)\)\. It follows thata¯=σ′​\(τ\)\\overline\{a\}=\\sigma^\{\\prime\}\(\\tau\)andz2=τz\_\{2\}=\\tau, where we use thatτ\>0\\tau\>0since the tangent\-secant point lies in the concave region\. *Condition \(i\):*The left endpoint satisfieshU​\(l\)=σ​\(l\)h\_\{U\}\(l\)=\\sigma\(l\)\. For the right endpoint,σ⁡\(u\)≤hU​\(u\)\\sigma\(u\)\\leq h\_\{U\}\(u\)sinceσ​\(τ\)=hU​\(τ\)\\sigma\(\\tau\)=h\_\{U\}\(\\tau\)forτ∈\(l,u\)\\tau\\in\(l,u\)andσ\\sigmais concave on\[τ,u\]⊂\[0,∞\)\[\\tau,u\]\\subset\[0,\\infty\)\. *Condition \(ii\):*Note thatσ′​\(z\)≥a¯\\sigma^\{\\prime\}\(z\)\\geq\\overline\{a\}for allz∈\[z1,z2\]z\\in\[z\_\{1\},z\_\{2\}\]\. It follows that σ⁡\(z1\)=σ⁡\(z2\)−∫z1z2σ′​\(z\)​𝑑z≤σ⁡\(z2\)−∫z1z2a¯​𝑑z=σ⁡\(z2\)−a¯​\(z2−z1\)\.\\sigma\(z\_\{1\}\)=\\sigma\(z\_\{2\}\)\-\\int\_\{z\_\{1\}\}^\{z\_\{2\}\}\\sigma^\{\\prime\}\(z\)dz\\leq\\sigma\(z\_\{2\}\)\-\\int\_\{z\_\{1\}\}^\{z\_\{2\}\}\\overline\{a\}dz=\\sigma\(z\_\{2\}\)\-\\overline\{a\}\(z\_\{2\}\-z\_\{1\}\)\.SincehUh\_\{U\}has slopea¯\\overline\{a\}andhU​\(z2\)=σ⁡\(z2\)h\_\{U\}\(z\_\{2\}\)=\\sigma\(z\_\{2\}\), the right\-hand side is equal to hU​\(z2\)−a¯​\(z2−z1\)=hU​\(z1\)\.h\_\{U\}\(z\_\{2\}\)\-\\overline\{a\}\(z\_\{2\}\-z\_\{1\}\)=h\_\{U\}\(z\_\{1\}\)\.Thus,hU​\(z1\)≥σ⁡\(z1\)h\_\{U\}\(z\_\{1\}\)\\geq\\sigma\(z\_\{1\}\)\. *Condition \(iii\):*This follows sincehU​\(z2\)−σ⁡\(z2\)=0h\_\{U\}\(z\_\{2\}\)\-\\sigma\(z\_\{2\}\)=0\.
- •Case 2:τ≤l\\tau\\leq l\.This implies thatl≥0l\\geq 0, since ifl<0l<0thenτ\>0\\tau\>0, which contradicts Case 2\. The procedure outputs the tangent line at the midpointμ:=\(l\+u\)/2\\mu:=\(l\+u\)/2: hU​\(z\)=σ′​\(μ\)​\(z−μ\)\+σ⁡\(μ\)\.h\_\{U\}\(z\)=\\sigma^\{\\prime\}\(\\mu\)\(z\-\\mu\)\+\\sigma\(\\mu\)\.Since\[l,u\]⊂\[0,∞\)\[l,u\]\\subset\[0,\\infty\),σ\\sigmais concave on\[l,u\]\[l,u\], so the tangent at any point within this interval dominatesσ\\sigmaon the entire interval\. It follows thata¯=σ′​\(μ\)\\overline\{a\}=\\sigma^\{\\prime\}\(\\mu\)andz2=μz\_\{2\}=\\mu\. *Condition \(i\):*Sinceσ\\sigmais concave on\[l,u\]\[l,u\], the tangent linehUh\_\{U\}atμ∈\[l,u\]\\mu\\in\[l,u\]satisfieshU​\(l\)≥σ⁡\(l\)h\_\{U\}\(l\)\\geq\\sigma\(l\)andhU​\(u\)≥σ⁡\(u\)h\_\{U\}\(u\)\\geq\\sigma\(u\)\. *Condition \(ii\):*As in Case 1,hUh\_\{U\}is tangent toσ\\sigmaatz2z\_\{2\}sohU​\(z2\)=σ⁡\(z2\)h\_\{U\}\(z\_\{2\}\)=\\sigma\(z\_\{2\}\)\. The identical integral argument over\[z1,z2\]\[z\_\{1\},z\_\{2\}\]yieldshU​\(z1\)≥σ⁡\(z1\)h\_\{U\}\(z\_\{1\}\)\\geq\\sigma\(z\_\{1\}\)\. *Condition \(iii\):*This follows sincehU​\(z2\)−σ⁡\(z2\)=0\.h\_\{U\}\(z\_\{2\}\)\-\\sigma\(z\_\{2\}\)=0\.
- •Case 3:τ≥u\\tau\\geq u\.This implies thatl≤0l\\leq 0and thereforeτ\>0\\tau\>0, since ifl\>0l\>0thenτ<0\\tau<0, which contradicts Case 3\. The procedure outputs the secant line through\(l,σ⁡\(l\)\)\(l,\\sigma\(l\)\)and\(u,σ⁡\(u\)\)\(u,\\sigma\(u\)\): hU​\(z\)=σ⁡\(u\)−σ⁡\(l\)u−l​\(z−l\)\+σ⁡\(l\)\.h\_\{U\}\(z\)=\\frac\{\\sigma\(u\)\-\\sigma\(l\)\}\{u\-l\}\(z\-l\)\+\\sigma\(l\)\.We first observe thatz2≥uz\_\{2\}\\geq u\. Becauseτ\\taumaximizes the secant slope fromll, we have σ′​\(τ\)=σ⁡\(τ\)−σ⁡\(l\)τ−l≥σ⁡\(u\)−σ⁡\(l\)u−l=a¯=σ′​\(z2\)\.\\sigma^\{\\prime\}\(\\tau\)=\\frac\{\\sigma\(\\tau\)\-\\sigma\(l\)\}\{\\tau\-l\}\\geq\\frac\{\\sigma\(u\)\-\\sigma\(l\)\}\{u\-l\}=\\overline\{a\}=\\sigma^\{\\prime\}\(z\_\{2\}\)\.Sinceτ,z2∈\[0,∞\)\\tau,z\_\{2\}\\in\[0,\\infty\)andσ′\\sigma^\{\\prime\}is decreasing over this interval,σ′​\(τ\)≥σ′​\(z2\)\\sigma^\{\\prime\}\(\\tau\)\\geq\\sigma^\{\\prime\}\(z\_\{2\}\)impliesz2≥τ≥uz\_\{2\}\\geq\\tau\\geq u\. *Condition \(i\):*hU​\(l\)=σ​\(l\)h\_\{U\}\(l\)=\\sigma\(l\)andhU​\(u\)=σ​\(u\)h\_\{U\}\(u\)=\\sigma\(u\)by construction\. *Condition \(ii\):*Note thatz1,l≤0z\_\{1\},l\\leq 0, soσ′\\sigma^\{\\prime\}is increasing betweenllandz1z\_\{1\}\. Thus, ifz1≤lz\_\{1\}\\leq lthenσ′​\(z\)≥a¯\\sigma^\{\\prime\}\(z\)\\geq\\overline\{a\}forz∈\[z1,l\]z\\in\[z\_\{1\},l\], and ifz1\>lz\_\{1\}\>lthenσ′​\(z\)≤a¯\\sigma^\{\\prime\}\(z\)\\leq\\overline\{a\}forz∈\[l,z1\]\.z\\in\[l,z\_\{1\}\]\.Either way, σ⁡\(z1\)=σ⁡\(l\)−∫z1lσ′​\(z\)​𝑑z≤σ⁡\(l\)−∫z1la¯​𝑑z=σ⁡\(l\)−a¯​\(l−z1\)=hU​\(z1\)\.\\sigma\(z\_\{1\}\)=\\sigma\(l\)\-\\int\_\{z\_\{1\}\}^\{l\}\\sigma^\{\\prime\}\(z\)dz\\leq\\sigma\(l\)\-\\int\_\{z\_\{1\}\}^\{l\}\\overline\{a\}dz=\\sigma\(l\)\-\\overline\{a\}\(l\-z\_\{1\}\)=h\_\{U\}\(z\_\{1\}\)\.*Condition \(iii\):*Sincez2≥uz\_\{2\}\\geq u, the first factor satisfiesu−z2≤0u\-z\_\{2\}\\leq 0\. We show that the second factor satisfieshU​\(z2\)−σ⁡\(z2\)≤0h\_\{U\}\(z\_\{2\}\)\-\\sigma\(z\_\{2\}\)\\leq 0\. To see this, note thatσ′​\(z\)≥a¯\\sigma^\{\\prime\}\(z\)\\geq\\overline\{a\}for allz∈\[z1,z2\]z\\in\[z\_\{1\},z\_\{2\}\], and thatz1∈\[l,u\]z\_\{1\}\\in\[l,u\]by the Mean Value Theorem, implying thatσ′​\(z\)≥a¯\\sigma^\{\\prime\}\(z\)\\geq\\overline\{a\}for allz∈\[u,z2\]\.z\\in\[u,z\_\{2\}\]\.Integrating yields σ⁡\(z2\)=σ⁡\(u\)\+∫uz2σ′​\(z\)​𝑑z≥σ⁡\(u\)\+∫uz2a¯​𝑑z=σ⁡\(u\)\+a¯​\(z2−u\)\.\\sigma\(z\_\{2\}\)=\\sigma\(u\)\+\\int\_\{u\}^\{z\_\{2\}\}\\sigma^\{\\prime\}\(z\)dz\\geq\\sigma\(u\)\+\\int\_\{u\}^\{z\_\{2\}\}\\overline\{a\}dz=\\sigma\(u\)\+\\overline\{a\}\(z\_\{2\}\-u\)\.SincehUh\_\{U\}has slopea¯\\overline\{a\}andhU​\(u\)=σ​\(u\)h\_\{U\}\(u\)=\\sigma\(u\), the right\-hand side is equal to hU​\(u\)\+a¯​\(z2−u\)=hU​\(z2\)\.h\_\{U\}\(u\)\+\\overline\{a\}\(z\_\{2\}\-u\)=h\_\{U\}\(z\_\{2\}\)\.Thus,σ⁡\(z2\)≥hU​\(z2\)\.\\sigma\(z\_\{2\}\)\\geq h\_\{U\}\(z\_\{2\}\)\.∎