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

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

arXiv:2608.17070v1 [cs.LG] 17 Aug 2026

Youwei Zhong Yale University youwei.zhong@yale.edu

Ben Merbaum Yale University ben.merbaum@yale.edu

Ning Luo University of Illinois Urbana-Champaign nl27@illinois.edu

Timos Antonopoulos Yale University timos.antonopoulos@yale.edu

Charalampos Papamanthou Yale University charalampos.papamanthou@yale.edu

Katerina Sotiraki Yale University katerina.sotiraki@yale.edu

Ruzica Piskac Yale University ruzica.piskac@yale.edu

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.

1

Introduction

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, 10]. 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 x, which may encode an image, and outputs a predicted label. A standard notion of local robustness requires that, for a given input Preprint.

x0 , all sufficiently close (with respect to a parameter ε) inputs receive the same prediction. This property can be formalized as: ∀x. ∥x − x0 ∥ < ε ⇒ Classification(x) = Classification(x0 ).

(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] and leak information about the training data [9]. 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 using zero-knowledge proofs (ZKPs) [8], 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, 6]. 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] can only support models with ≈ 100 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, 7]. 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] 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, 29, 3]. 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 a certification algorithm which 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]. 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 the Four-Point Relaxation Gadget (Section 5). 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. 2

Instead of using a general-purpose ZKP backend, we design a customized backend that 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.

2

Preliminaries

A zero-knowledge proof (ZKP) allows a prover P to convince a verifier V that a public statement x is true, without revealing any further information about why it is true. Private information explaining the “why” is called the witness w. For instance, a public statement x may be that an ML model is locally robust at a given point, whereas the private witness w contains the private model weights and auxiliary values produced in computation. P uses x and w to outputs a proof π, which V checks alongside x and either accepts or rejects. A commit-and-prove ZKP system enables P to first produce a commitment cw to the witness w which is hiding (cw reveals nothing about w) and binding (P cannot find a different witness w′ ̸= w corresponding to cw ). The commitment cw is part of the public statement x, and P’s claim is that P knows a witness w whose commitment is cw and that w is a valid witness for x. PANDA is a commit-and-prove ZKP system which uses three underlying cryptographic primitives: 1. A polynomial commitment scheme, ΠCOM , which consists of three algorithms: • C OMMIT (run by P) takes as input a polynomial f and outputs a commitment cf to f which is hiding and binding. • E VAL (run by P) takes as input f , a point x, and a value y, and outputs a proof π, also called an opening, claiming that y = f (x). • V ERIFY (run by V) takes as input cf , x, y, π, and either accepts or rejects. ΠCOM is complete if V ERIFY accepts whenever cf ← C OMMIT(f ), y = f (x), and π ← E VAL(f, x, y). We say ΠCOM is evaluation-binding if a malicious P cannot produce an accepting proof π for x, y if y ̸= f (x). We say ΠCOM is zero-knowledge if π reveals no information about f. 2. A ZKP for matrix arithmetic, ΠARITH . We can encode matrices or vectors as polynomials using interpolation and then use ΠCOM for commitments to matrices or vectors. • The private witness w is a list of matrices (e.g., A, B, C, D). • The public statement x is a list of commitments to these matrices (e.g. cA , cB , cC , cD ) and a claimed arithmetic relation between them (e.g. A = BC + D). • P proves to V that P knows matrices in w whose commitments match those in x and satisfy this matrix arithmetic equality. 3. A ZKP for table lookups, ΠLOOKUP (also known as a lookup argument). • The private witness w is a lookup vector a.1 • The public statement x is a commitment ca to a as well as a table vector t. • P proves to V that P knows a vector a whose commitment is ca and such that each entry of a is in the table t. ΠARITH and ΠLOOKUP each contain two algorithms: • P ROVE (run by P) takes as input w and x and outputs a proof π. As a subroutine, P produces openings of masked versions of the witnesses via ΠCOM .E VAL. • V ERIFY (run by V) takes as input x and π and accepts or rejects. As a subroutine, V calls ΠCOM .V ERIFY to check the opening proofs (which are contained in π). We say that a ZKP is complete if, whenever w is a valid witness for x, V ERIFY accepts the proof π generated by P ROVE. A ZKP is sound if whenever x is an invalid statement, no computationally 1We present a simplified abstract interface. The concrete lookup arguments we use embed auxiliary information pertaining

to a and t in the witness w which is committed and appended to the public statement x.

3

bounded prover can forge a proof π that causes V ERIFY to accept. A ZKP is zero-knowledge if π reveals no information about w beyond the fact that w exists. ΠLOOKUP can be used for range proof ZKPs, which prove that each element of a vector a lies within an interval [l, r]. This is done simply by setting the table vector t = (l, l + 1, . . . , r). We often write one-sided range proofs as a ≥ 0, where l = 0 and r is chosen implicitly as the maximum attainable value of elements in a, dependent on the quantization. ΠLOOKUP can also prove non-linear function evaluations; that is, for a set of points {(xi , yi )}i∈[n] and a non-linear function f , ΠLOOKUP proves that f (xi ) = yi for each i ∈ [n]. This is achieved by setting a = ((xi , yi ))i∈[n] and t = ((z, f (z)))z , where z ranges over possible values in the domain. Quantization. Most existing ZKPs are incompatible with floating-point computation. Following precedent in prior zkML papers [22, 6], we perform quantization to translate all computations to finite field arithmetic. We follow the quantization approach introduced in [11], where we represent each real number x with a Q-bit integer qx ∈ [0, 2Q ) satisfying x · Sx ≈ qx for an optimally chosen scaling factor Sx ≫ 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 values x and y, we first rescale them to share the same scaling factor, then sum the quantized integers qx and qy . To multiply two values x and y, we multiply the quantized integers qx and qy , and set the scaling factor of the product to Sx Sy . To rescale qx ≈ x · Sx to some new scaling factor Sz , we compute qz = ⌊Sz qx /Sx ⌋ .

3

CROWN Algorithm

In this section, we review the CROWN algorithm [32], 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. 3.1

Setting and Goal

We consider an m-layer feed-forward network f : Rn0 → Rnm defined by the recursion   z (k) = W(k) h(k−1) + b(k) ∈ Rnk , h(k) = σ z (k) ∈ Rnk

(2)

for k = 1, . . . , m, with weight matrices W(k) ∈ Rnk ×nk−1 , biases b(k) ∈ Rnk , and a coordinatewise activation function σ : Rnk → Rnk for all k. The input is h(0) = x ∈ Rn0 and the output is f (x) = z (m) ∈ Rnm . The ℓth layer has nℓ neurons, and the output neurons on input x0 are denoted fc (x0 ) for c ∈ {1, . . . , nm }. For a classification model, the choice of c which maximizes fc (x0 ) is the predicted class of x0 . Given an input x0 , an ℓ∞ -perturbation radius ε, and a predicted class c of x0 , the network is locally robust at x0 with respect to a targeted attack class t ̸= c if ft (x) ≤ fc (x),

∀x ∈ B(x0 , ε),

(3)

where B(x0 , ε) := {x : ∥x − x0 ∥∞ ≤ ε}. Such a claim is a special case of the general statement C · f (x) ≤ u,

∀x ∈ B(x0 , ε),

(4)

⊤ where C ∈ RN ×nm , u ∈ RN , obtained by setting N = 1, u = 0, and C = e⊤ t − ec , where ei is th the i basis vector.

Goal of the algorithm. CROWN certifies statements of the form (4) by running an algorithm which computes a vector u′ such that C · f (x) ≤ u′ , and then ultimately checking that u′ ≤ u entry-wise. Crucially, this algorithm computes linear bounds on the pre-activation vector z (k) for each layer k as a function of the input x: A(k) x + d(k) ≤ z (k) ≤ A (k)

(k)

where A(k) , A ∈ Rnk ×n0 and d(k) , d bounds on C · z (m) rather than on z (m) .

(k)

(k)

x+d

,

∀x ∈ B(x0 , ε),

(5)

∈ Rnk . In the final layer m, CROWN constructs linear

4

Outer forward pass, inner backward pass. CROWN builds (5) layer by layer, passing forward from k = 1 to k = m. Computing the bounds at layer k, however, requires a backward pass from layer k down to the input, using the previously computed bounds for layers ℓ < k. Once this is completed, a concretization step transforms (5) into scalar bounds used to derive u′ . 3.2

Backward Pass

The backward pass for layer k begins with a set of concretized bounds {L(ℓ) , U (ℓ) }ℓ<k for layers ℓ < k, where each pre-activation vector z (ℓ) satisfies the entry-wise inequality L(ℓ) ≤ z (ℓ) ≤ U (ℓ) ,

∀x ∈ B(x0 , ε).

(6)

These are obtained by recursively calling CROWN for layers ℓ = 1, . . . , k −1. The goal is to compute the linear bounds of (5) for layer k. We describe the upper bound case; the lower bound is symmetric. Activation relaxation. A prerequisite is a pair of linear relaxations of the activation σ. For every (ℓ) layer ℓ < k, CROWN supplies four vectors a(ℓ) , b , a(ℓ) , b(ℓ) such that (ℓ)

a(ℓ) z + b(ℓ) ≤ σ(z (ℓ) ) ≤ a(ℓ) z + b

∀z ∈ [L(ℓ) , U (ℓ) ].

,

(7)

The linear relaxations are selected through an intricate procedure detailed in Appendix A.2. Invariants. The backward pass maintains and updates an affine bound (A, d) with A ∈ Rnk ×nℓ and d ∈ Rnk . At each depth ℓ from k down to 0, the bound satisfies one of two invariants: (ℓ)

Invariant Ih Invariant

z (k) ≤ A h(ℓ) + d,

:

Iz(ℓ)

:

z

(k)

≤ Az

(ℓ)

(8)

+ d,

(9)

where the inequality is entry-wise and the bound holds for all x ∈ B(x0 , ε). The recursion starts at (k−1) (0) Ih , ends with (5) at Ih , and alternates between the two invariants as follows: (ℓ)

(ℓ)

(ℓ)

(ℓ−1)

• Step 1 at depth ℓ transforms Ih ⇒ Iz by linear relaxation through the activation. • Step 2 at depth ℓ transforms Iz ⇒ Ih

by substitution through the linear map. (k−1)

Initialization. z (k) = W(k) h(k−1) + b(k) establishes Ih (ℓ)

by setting A ← W(k) and d ← b(k) .

(ℓ)

Step 1: Ih ⇒ Iz . We substitute h(ℓ) = σ(z (ℓ) ) into (8) and apply the linear relaxation (7). Each (ℓ)

(ℓ)

(ℓ)

(ℓ)

entry of A uses the upper relaxation (ai , bi ) when positive and the lower relaxation (ai , bi ) when negative, since multiplying by a negative number flips the inequality. Splitting A into A+ = max(A, 0),

A− = min(A, 0)

(10)

yields the following update: d ← d + A+ b

(ℓ)

+ A− b(ℓ) ,

A ← A+ diag(a(ℓ) ) + A− diag(a(ℓ) )

(11)

where diag(v) denotes the diagonal matrix with entries of the vector v on its diagonal. After the (ℓ) update, (A, d) satisfies Iz . (ℓ)

(ℓ−1)

Step 2: Iz ⇒ Ih

. We substitute z (ℓ) = W(ℓ) h(ℓ−1) + b(ℓ) , so d ← d + Ab(ℓ) ,

A ← AW(ℓ) . (ℓ−1)

The affine bound (A, d) has advanced one level and now satisfies Ih

(12) .

(0)

Termination. Iterating down to ℓ = 1 produces Ih , which is exactly equation (5) since h(0) = x. We finally retrieve A

(k)

(k)

← A and d

← d.

Final layer. In the final layer k = m, the backward pass must be modified in order to support the (ℓ) (ℓ) claim Cf (x) ≤ u. Notably, invariants Ih and Iz replace the left-hand side z (m) with Cz (m) . The initialization step is given by A ← C · W(m) and d ← C · b(m) . Steps 1 and 2 in the backward pass remain the same, and the final concretization yields the desired claim. 5

3.3

Concretization

Once the backward pass is complete for layer k, concretization yields the vectors L(k) , U (k) ∈ Rnk by maximizing and minimizing the affine bounds of (5) over x ∈ B(x0 , ε). The upper bound U (k) (and symmetrically the lower bound L(k) ) is derived as  (k)  (k) (k) (k) (k) U (k) = max A x+d = A+ (x0 + ε1) + A− (x0 − ε1) + d , (13) x∈B(x0 ,ε)

n0

where 1 ∈ R

is the all-ones vector and (k)

A+ = max(A

4

(k)

(k)

, 0),

A− = min(A

(k)

, 0).

(14)

PANDA Framework

This section presents PANDA, our commit-and-prove ZKP for certifying local robustness of neural networks. We describe the steps used by P to convince V of a local robustness claim in zero knowledge. The PANDA algorithm is provided in full detail with pseudocode in Appendix B. Setup. P and V agree on the input point x0 ∈ Rn0 , the perturbation bound ε, the model architecture, and a public matrix C and vector u which define the local robustness claim of (4), ∀x ∈ B(x0 , ε),

Cf (x) ≤ u.

Initial pass. P runs quantized CROWN on input (x0 , ε), producing a transcript for each layer k: (k)

(a) linear bounds A(k) , A

, d(k) , d

(k)

of (5),

(b) all intermediate states (A, d) derived in the backward pass of (8) and (9), (c) signed component matrices from equations (11) and (13), (d) concretized scalar bounds L(k) and U (k) of (13), (e) per-neuron linear relaxation coefficients a(k) , b

(k)

, a(k) , b(k) of (7), and

(f) quantization scaling factors Sx for each value x in the transcript. Commit. P calls ΠCOM .C OMMIT to commit to the model parameters and all quantities in the CROWN transcript. Prove. The ZKP private witness w contains the model parameters {W(k) , b(k) }m k=1 and the CROWN transcript. The public statement x contains all commitments to the witness values together with the robustness claim (x0 , ε, C, u) and the model architecture. For each operation performed in the initial pass of quantized CROWN, P produces a proof π using one of two underlying ZKPs: ΠARITH for matrix arithmetic and ΠLOOKUP for table lookups. • ΠARITH is used for P to prove correctness of equations (8),(9),(11),(12), and (13), • ΠLOOKUP is used for P to prove correctness of equations (10) and (14). Proof of activation relaxations. Existing primitives ΠARITH and ΠLOOKUP are insufficient to prove equation (7). In particular, P must prove at each neuron that its committed scalars a, b, a, b satisfy az + b ≤ σ(z) ≤ az + b over a real-valued interval [l, u]. While pointwise checks are feasible using ΠLOOKUP , such checks do not provide soundness guarantees between points. We therefore create a novel component to prove such equations, the Four-Point Relaxation Gadget, which is the subject of Section 5. Proof of rescaling. All quantization operations must also be associated with proofs so that V can check P does not deviate from the protocol. As discussed in Section 2, a value x is represented as qx ≈ x · Sx where qx is the quantized integer and Sx is a scaling factor, also an integer. Rescaling to a new scaling factor Sz requires computing qz = ⌊Sz qx /Sx ⌋. P retains the remainder r ∈ [0, Sx ) of 6

Figure 1: Linear relaxations of the ReLU (left) and tanh (right) activation functions over the interval [l, u] (shaded). Each activation σ(z) (black) is bounded by affine functions hU (z) (dashed green) and hL (z) (dashed red) over the interval [l, u]. the rounding operation as an auxiliary witness, and proves that 0 ≤ r < Sx using ΠLOOKUP . Finally, P proves the identity Sz · qx = Sx · qz + r (15) using ΠARITH , which asserts the correctness of the rounding operation. Full protocol. The pseudocode of the PANDA algorithm is provided in Appendix B. The completeness, soundness, and zero-knowledge properties of PANDA follow directly from the respective properties of the underlying primitives ΠCOM , ΠARITH , and ΠLOOKUP . Asymptotic runtime. The runtime of CROWN and PANDA are both polynomial in the number of neurons in the network. For an m-layer neural network with n neurons per layer, CROWN runs in time O(m2 n3 ) (see Appendix A). 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.

5

The Four-Point Relaxation Gadget

A core challenge in converting CROWN to a ZKP system is verifying that per-neuron linear relaxations in (7) are valid over a real interval. Our construction is designed such that V can check pointwise inequalities at only four points in order to determine the validity of a linear relaxation. Throughout this section, we focus on a single neuron with pre-activation bounds l ≤ u and fix an activation function σ. Definition 5.1 (Linear relaxation of an activation function). A linear relaxation for σ over an interval [l, u] is a pair of affine functions hL (z) = az + b,

hU (z) = az + b,

(16)

satisfying hL (z) ≤ σ(z) ≤ hU (z),

∀z ∈ [l, u].

(17)

Figure 1 depicts examples of linear relaxations of the ReLU and tanh functions. We design a system such that V can verify whether (17) holds by checking only a constant number of pointwise inequalities. Observe that verifying (17) over all possible z ∈ [l, u] is impossible (there are infinitely many such z), whereas checking (17) at finitely many sample points does not guarantee that the equation holds between these sample points.   x In Section 5.1, we focus on S-shaped activation functions such as sigmoid σ(x) = exe+1 , tanh  
x −x σ(x) = eex −e , and arctan σ(x) = tan−1 (x) , which arise naturally in ML applications. In −x +e Section 5.2, we focus on ReLU activations (σ(x) = max(0, x)). 7

5.1

S-shaped Activations

We first focus on S-shaped activations and we show that linear relaxation validity reduces to checks at only four points per neuron, independent of interval width. Assumption 5.1 (S-shaped activation). σ : R → R is C 1 , monotone increasing, bounded, and has a single inflection point at z = 0. Sigmoid, tanh, and arctan satisfy Assumption 5.1. The assumption implies that σ is convex on (−∞, 0] and concave on [0, ∞), and that the derivative σ ′ has a finite maximum B ∈ R, attained at z = 0. It suffices to consider linear relaxation slopes a, a ∈ (0, B]. Lemma 5.1. Let σ satisfy Assumption 5.1. For any α ∈ (0, B], there exist two tangency points z1 ≤ 0 ≤ z2 such that σ ′ (z1 ) = σ ′ (z2 ) = α. Moreover, these points are distinct if α < B, and they coincide at z1 = z2 = 0 if α = B. See proof in Appendix G. 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 to hU (z) − σ(z). Lemma 5.2 (Four-point soundness). Let σ satisfy Assumption 5.1, and fix an interval [l, u] ⊆ R. The upper bound hU (z) = az + b with a > 0 satisfies σ(z) ≤ hU (z) for all z ∈ [l, u] if and only if (i) Endpoints: σ(l) ≤ hU (l) and σ(u) ≤ hU (u); (ii) Tangency points: for every z ∈ [l, u] with σ ′ (z) = a, σ(z) ≤ hU (z). The dual statement holds for the lower bound with the inequality directions reversed. By Lemma 5.1, σ ′ has at most two preimages of a, so it suffices to verify the values of σ and hU at no more than four points: the two endpoints l, u and the two tangency points z1 , z2 . The case-work obstacle. Encoding Lemma 5.2 directly into a ZKP requires case-work at each tangency point zi for i ∈ {1, 2}: there must be a range proof asserting that either (a) zi ≤ l, (b) zi ≥ u, or (c) σ(zi ) ≤ hU (zi ). Declaring which case holds for each zi , however, leaks information about l and u, which are themselves derived from the private model parameters. We therefore replace Lemma 5.2 with a case-free, sufficient (but not necessary) set of criteria for determining whether hU and hL are a valid linear relaxation over the interval [l, u]. Theorem 5.1 (Case-free four-point soundness). Let σ satisfy Assumption 5.1 and fix an interval [l, u] ⊆ R. Let z1 ≤ 0 ≤ z2 be the (possibly coinciding) tangency points satisfying σ ′ (z1 ) = σ ′ (z2 ) = a. The upper bound hU is valid on [l, u] if each of the following criteria is satisfied. (i) Endpoints: σ(l) ≤ hU (l) and σ(u) ≤ hU (u); (ii) Left tangency: σ(z1 ) ≤ hU (z1 );
(iii) Right tangency: 0 ≤ (u − z2 ) hU (z2 ) − σ(z2 ) ; A symmetric statement holds for the lower bound hL and is given in Appendix H. Moreover, the linear relaxations selected by CROWN (given in Appendix A.2) satisfy these criteria. See proof in Appendix H. Figure 2 provides an example of upper bounds hU for both cases z2 ≤ u and z2 > u. ZKP Algorithm. We present the Four-Point Relaxation Gadget (formal algorithm in Appendix B) as a simple set of criteria which P proves and V verifies. We encode Theorem 5.1 as a set of ZKP constraints, which invoke ΠARITH and ΠLOOKUP ZKP systems as subroutines. For each neuron, and for the upper bound case, P takes as private witness the interval endpoints (l, u), the upper bound (a, b), and the tangency points (z1 , z2 ). P evaluates σ at the witness points and proves the correctness of these evaluations using lookup tables Tσ and Tσ′ . P then proves the conditions of Theorem 5.1 are met. Algorithm 2 of Appendix B formally presents the prover for the upper-bound case, and the lower-bound case is analogous. V checks the correctness of all proofs. 8

Figure 2: Case-free four-point soundness (Theorem 5.1) for the activation function σ(z) = tanh(z). The left image depicts [l, u] = [−1.5, 1.5], z2 ≤ u, and σ(z2 ) ≤ hU (z2 ). The right image depicts [l, u] = [−1.5, 0.2], z2 > u, and σ(z2 ) > hU (z2 ). Both cases therefore satisfy the criteria given by Theorem 5.1 without requiring case-specific analysis. 5.2

ReLU Activations

For ReLU, σ(z) = max(0, z) is piecewise linear and convex. CROWN selects lower and upper bounds (hL , hU ) for an interval [l, u] as follows: • Upper bound hU : select the secant line connecting (l, σ(l)) and (u, σ(u)), given by hU (z) =

σ(u) − σ(l) (z − l) + σ(l). u−l

• Lower bound hL : select hL (z) = az for any a ∈ {0, 1}. Either choice of a guarantees a valid linear relaxation. Zhang et al. [32] recommends selecting a = 1 [|u| ≥ |l|] . We design a simple algorithm for proving the validity of such a linear relaxation (hL , hU ). • Upper bound hU : prove σ(l) = hU (l) and σ(u) = hU (u). • Lower bound hL : prove a(a − 1) = 0 (i.e. a ∈ {0, 1}) and intercept b = 0. Each of these conditions is proven with ΠARITH . For further generality, a can be selected within the closed interval [0, 1] and ΠLOOKUP can be used for the proof, thus supporting α-CROWN [30].

6

Implementation and Evaluations

We implement PANDA in Rust, using the arkworks ecosystem [1] for ZKP programming. We use Hyrax [28] over the elliptic curve BN254 for ΠCOM , the protocol of Thaler [26] for ΠARITH , and LogUp-GKR [21] for Π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, 14]). 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. Our implementation is available at https://github.com/youweizhong/PANDA. 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? 9

Table 1: Summary of results. Each row is one model. We denote an m-layer feed-forward network with n neurons per layer by m × [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]. Dataset

Structure

Act.

Prove (s)

Verify (s)

Proof CROWN (MB) (s)

Drift (%)

2 × [20] 3 × [1024] 4 × [1024] 4 × [1024] 4 × [1024]

ReLU ReLU ReLU Sigmoid Tanh

22.81 ± 0.20 0.97 ± 0.01 101.58 ± 3.75 4.60 ± 0.13 226.08 ± 14.67 9.56 ± 0.48 327.47 ± 11.36 14.13 ± 0.46 333.94 ± 5.81 14.31 ± 0.28

3 9 17 31 32

1.3e-4 0.22 0.44 0.47 0.46

2 × [128] 2 × [128] 3 × [64] [8, 2]

ReLU ReLU ReLU ReLU

23.04 ± 0.19 20.33 ± 0.19 36.61 ± 0.29 34.89

3 3 5 4

1.3e-4 -0.05 1.4e-4 -0.29 8.1e-5 -0.09 1.4e-5 -12.60

MNIST

Other SafeNLP med SafeNLP robot LunarLander FairProof Adult

0.81 ± 0.01 0.78 ± 0.01 1.46 ± 0.02 1.21

0.02 0.03 -0.01 2.48 6.33

Benchmark suites. We evaluate PANDA on the MNIST image classification models [18] from the CROWN evaluation. In addition, we evaluate PANDA on two application-focused benchmarks: SafeNLP [2] from VNN-COMP 2025 [13] 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] from VNN-COMP 2022 [19] classifies safe actions to be taken by lunar robots. Finally, we evaluate on the only publicly available benchmark from FairProof’s suite [31]. 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, with full benchmarks in Table 3 and a component-wise breakdown of prover time in Appendix E. Q1: Scalability. PANDA produces proofs of local robustness in under six minutes for the largest 4 × [1024] MNIST networks, which have 2.9 million parameters. Q2: Support of activation functions. Relative to ReLU networks, sigmoid/tanh increases proving time by 1.5–2.6×, 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 roughly 100–1,000× and a verifier overhead of 20–50× over CROWN on the 1024-neuron models (rising to 106 × only 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.21s) and proof size (4MB). FairProof has smaller proof size and verifier time, whereas PANDA’s advantage is prover feasibility and scale. See Appendix C for a detailed discussion.

7

Known 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, 6]. The precision level specified in the quantization affects the accuracy of values retrieved from the lookup tables used in our non-linear 10

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]. Algorithms such as CROWN are incomplete 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.

8

Related 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] 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] and OATH by [5] prove a notion of global fairness using aggregated statistics; this direction is disjoint from our work and produces weaker bounds. Confidential-PROFITT by [24] 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, 27], 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, 32, 30]. 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, Song et al. [25] 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 x0 and perturbation radius ε while 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.

9

Conclusion

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. 11

References [1] arkworks authors. arkworks zkSNARK ecosystem, 2022. URL https://arkworks.rs. [2] M. Casadio, T. Dinkar, E. Komendantskaya, L. Arnaboldi, M. L. Daggitt, O. Isac, G. Katz, V. Rieser, and O. Lemon. NLP verification: towards a general methodology for certifying robustness. European Journal of Applied Mathematics, 37(1):180–237, 2026. doi: 10.1017/ S0956792525000099. [3] H. Duong, T. Nguyen, and M. Dwyer. A DPLL(T) framework for verifying deep neural networks, 2024. URL https://arxiv.org/abs/2307.10266. [4] H. Duong, T. Nguyen, and M. Dwyer. Generating and checking DNN verification proofs. In D. Belgrave, C. Zhang, H. Lin, R. Pascanu, P. Koniusz, M. Ghassemi, and N. Chen, editors, Advances in Neural Information Processing Systems, volume 38, pages 65887–65909. Curran Associates, Inc., 2025. URL https://proceedings.neurips.cc/paper_files/paper/ 2025/file/5f326d2e040a20d52438873f5d727e58-Paper-Conference.pdf. [5] O. Franzese, A. S. Shamsabadi, C. Luck, and H. Haddadi. Secure and confidential certificates of online fairness. In The Thirty-ninth Annual Conference on Neural Information Processing Systems, 2025. URL https://openreview.net/forum?id=9jaQTx1O8T. [6] N. Gailly, I. Hishon-Rezaizadeh, T. Liu, N. Mainardi, D. Papadopoulos, C. Papamanthou, C. Pappas, S. Srinivasan, Z. Youell, and Y. Zhang. DeepProve: Verifiable end-to-end large language model inference. Cryptology ePrint Archive, Paper 2026/1112, 2026. URL https: //eprint.iacr.org/2026/1112. [7] R. J. George, J. Cruden, X. Zhong, H. Zhang, and A. Anandkumar. TorchLean: Formalizing neural networks in lean, 2026. URL https://arxiv.org/abs/2602.22631. [8] S. Goldwasser, S. Micali, and C. Rackoff. The knowledge complexity of interactive proofsystems. In Proceedings of the Seventeenth Annual ACM Symposium on Theory of Computing, STOC ’85, pages 291–304, New York, NY, USA, 1985. Association for Computing Machinery. ISBN 0897911512. doi: 10.1145/22145.22178. URL https://doi.org/10.1145/22145. 22178. [9] A. Hannun, C. Guo, and L. van der Maaten. Measuring data leakage in machine-learning models with Fisher information. In C. de Campos and M. H. Maathuis, editors, Proceedings of the Thirty-Seventh Conference on Uncertainty in Artificial Intelligence, volume 161 of Proceedings of Machine Learning Research, pages 760–770. PMLR, 27–30 Jul 2021. URL https://proceedings.mlr.press/v161/hannun21a.html. [10] M. Hines. I Smell a Bot: California’s S.B. 1001, Free Speech, and the Future of Bot Regulation. Houston Law Review, 57(2), Dec. 2019. URL https://houstonlawreview.org/article/ 11569-i-smell-a-bot-california-s-s-b-1001-free-speech-and-the-future-of-bot-regulation. [11] B. Jacob, S. Kligys, B. Chen, M. Zhu, M. Tang, A. Howard, H. Adam, and D. Kalenichenko. Quantization and training of neural networks for efficient integer-arithmetic-only inference. In 2018 IEEE/CVF Conference on Computer Vision and Pattern Recognition, pages 2704–2713, 2018. doi: 10.1109/CVPR.2018.00286. [12] G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In R. Majumdar and V. Kunčak, editors, Computer Aided Verification, pages 97–117, Cham, 2017. Springer International Publishing. ISBN 978-3-319-63387-9. [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. The 6th international verification of neural networks competition (VNN-COMP 2025): Summary and results, 2025. URL https://arxiv.org/abs/2512. 19007. [14] D. Kaviani and S. Setty. Vega: Low-latency zero-knowledge proofs over existing credentials. Cryptology ePrint Archive, Paper 2025/2094, 2025. URL https://eprint.iacr.org/2025/ 2094. 12

[15] M. Kop. EU Artificial Intelligence Act: The European Approach to AI, Sept. 2021. URL https://papers.ssrn.com/abstract=3930959. [16] A. Kothapalli and S. Setty. HyperNova: Recursive arguments for customizable constraint systems. In L. Reyzin and D. Stebila, editors, Advances in Cryptology – CRYPTO 2024, pages 345–379, Cham, 2024. Springer Nature Switzerland. ISBN 978-3-031-68403-6. [17] V. Krish. min-err-trajs-vnncomp-benchmarks, June 2022. URL https://github.com/ Ethos-lab/min-err-trajs-vnncomp-benchmarks. [Online; accessed 6. May 2026]. [18] Y. LeCun, L. Bottou, Y. Bengio, and P. Haffner. Gradient-based learning applied to document recognition. Proceedings of the IEEE, 86(11):2278–2324, 1998. URL http://citeseerx. ist.psu.edu/viewdoc/summary?doi=10.1.1.42.7665. [19] M. N. Müller, C. Brix, S. Bak, C. Liu, and T. T. Johnson. The third international verification of neural networks competition (VNN-COMP 2022): Summary and results, 2023. URL https://arxiv.org/abs/2212.10376. [20] M. Nasr, R. Shokri, and A. Houmansadr. Comprehensive privacy analysis of deep learning: Passive and active white-box inference attacks against centralized and federated learning. In 2019 IEEE Symposium on Security and Privacy (SP), pages 739–753, 2019. doi: 10.1109/SP. 2019.00065. [21] S. Papini and U. Haböck. Improving logarithmic derivative lookups using GKR. Cryptology ePrint Archive, Paper 2023/1284, 2023. URL https://eprint.iacr.org/2023/1284. [22] W. Qu, Y. Sun, X. Liu, T. Lu, Y. Guo, K. Chen, and J. Zhang. zkGPT: an efficient noninteractive zero-knowledge proof framework for LLM inference. In Proceedings of the 34th USENIX Conference on Security Symposium, SEC ’25, USA, 2025. USENIX Association. ISBN 978-1-939133-52-6. [23] S. Segal, Y. Adi, B. Pinkas, C. Baum, C. Ganesh, and J. Keshet. Fairness in the eyes of the data: Certifying machine-learning models. In Proceedings of the 2021 AAAI/ACM Conference on AI, Ethics, and Society, AIES ’21, pages 926–935, New York, NY, USA, 2021. Association for Computing Machinery. ISBN 9781450384735. doi: 10.1145/3461702.3462554. URL https://doi.org/10.1145/3461702.3462554. [24] A. S. Shamsabadi, S. C. Wyllie, N. Franzese, N. Dullerud, S. Gambs, N. Papernot, X. Wang, and A. Weller. Confidential-PROFITT: Confidential PRO of FaIr Training of Trees. In The Eleventh International Conference on Learning Representations, 2023. URL https: //openreview.net/forum?id=iIfDQVyuFD. [25] N. Song, X. Luan, Y. Guo, R. Bie, M. Sun, and X. Zhang. Privacy-preserving robustness verification for neural networks. In The 42nd Conference on Uncertainty in Artificial Intelligence (UAI), 2026. [26] J. Thaler. Time-optimal interactive proofs for circuit evaluation. In R. Canetti and J. A. Garay, editors, Advances in Cryptology – CRYPTO 2013, pages 71–89, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. ISBN 978-3-642-40084-1. [27] E. Toreini, M. Mehrnezhad, and A. van Moorsel. Verifiable fairness: Privacy-preserving computation of fairness for machine learning systems. In Computer 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, pages 569–584, Berlin, Heidelberg, 2023. Springer-Verlag. ISBN 978-3-031-54128-5. doi: 10.1007/ 978-3-031-54129-2_34. URL https://doi.org/10.1007/978-3-031-54129-2_34. [28] R. S. Wahby, I. Tzialla, A. Shelat, J. Thaler, and M. Walfish. Doubly-efficient zkSNARKs without trusted setup. In 2018 IEEE Symposium on Security and Privacy (SP), pages 926–943, 2018. doi: 10.1109/SP.2018.00060. 13

[29] S. Wang, H. Zhang, K. Xu, X. Lin, S. Jana, C.-J. Hsieh, and J. Z. Kolter. Beta-CROWN: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. In M. Ranzato, A. Beygelzimer, Y. Dauphin, P. Liang, and J. W. Vaughan, editors, Advances in Neural Information Processing Systems, volume 34, pages 29909–29921. Curran Associates, Inc., 2021. URL https://proceedings.neurips.cc/paper_files/paper/ 2021/file/fac7fead96dafceaf80c1daffeae82a4-Paper.pdf. [30] K. Xu, H. Zhang, S. Wang, Y. Wang, S. Jana, X. Lin, and C.-J. Hsieh. Fast and Complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In International Conference on Learning Representations, 2021. URL https: //openreview.net/forum?id=nVZtXBI6LNn. [31] C. Yadav, A. Roy Chowdhury, D. Boneh, and K. Chaudhuri. FairProof: Confidential and certifiable fairness for neural networks. In R. Salakhutdinov, Z. Kolter, K. Heller, A. Weller, N. Oliver, J. Scarlett, and F. Berkenkamp, editors, Proceedings of the 41st International Conference on Machine Learning, volume 235 of Proceedings of Machine Learning Research, pages 55682–55705. PMLR, 21–27 Jul 2024. URL https://proceedings.mlr.press/ v235/yadav24a.html. [32] H. Zhang, T.-W. Weng, P.-Y. Chen, C.-J. Hsieh, and L. Daniel. Efficient neural network robustness certification with general activation functions. In Proceedings of the 32nd International Conference on Neural Information Processing Systems, NIPS’18, pages 4944–4953, Red Hook, NY, USA, 2018. Curran Associates Inc. [33] T. Zhang, S. Dong, O. D. Kose, Y. Shen, and Y. Zhang. FairZK: A scalable system to prove machine learning fairness in zero-knowledge. In 2025 IEEE Symposium on Security and Privacy (SP), pages 3460–3478, 2025. doi: 10.1109/SP61157.2025.00205.

14

A

Details of CROWN

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

The CROWN Algorithm

Algorithm 1 gives the full CROWN procedure. This consists of an outer forward pass over layers k, and an inner backward pass from layer k down to the input layer 0. The backward pass repeatedly calls S TEP 1, the activation-relaxation update (11), and S TEP 2, the linear-map substitution (12). Concretization (13) is applied following each backward pass. For simplicity of notation, we assume (ℓ) relaxation scalars (a(ℓ) , b , a(ℓ) , b(ℓ) ) for each layer ℓ are implicitly passed as input to all procedures below upon generation. Time complexity. For a neural network with m layers, n neurons per layer, and n output neurons, CROWN runs in time O(m2 n3 ). The algorithm performs two nested for-loops, consisting of the outer forward pass and the inner backward pass, each over m layers. At each layer, CROWN performs multiplications of n × n matrices, each requiring time O(n3 ). A.2

The Relaxation Algorithm

The R ELAX algorithm takes as input a concretized interval (l, u) and an activation function σ, and outputs scalars (a, b, a, b) satisfying az + b ≤ σ(z) ≤ az + b,

∀z ∈ [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. Below, we describe the R ELAX procedure for S-shaped activations σ. The procedure for ReLU activations is provided in Section 5.2. We also focus on the selection of the upper bound hU (z) = az + b, as the lower bound is similar but with the roles of l and u reversed. Procedure. CROWN selects an optimal pair (a, b) via the following steps: 1. Solve the equation σ(τ ) − σ(l) (19) τ −l for τ . This can be solved directly given a closed form for σ and σ ′ , or iteratively solved via Newton’s method. Intuitively, this equation asks for a value τ such that the tangent line of σ(z) at z = τ is exactly equal to the secant line through (l, σ(l)) and (τ, σ(τ )). This equation has two solutions for S-shaped activations, including τ = l as a trivial root. By abuse of notation, we let τ denote the non-trivial root. 2. Choose an upper bound hU (z) = az + b based on where τ falls relative to the interval [l, u]: • Case 1: τ ∈ (l, u). Output the tangent line for σ at z = τ : σ ′ (τ ) =

hU (z) =

σ(τ ) − σ(l) (z − l) + σ(l). τ −l

• Case 2: τ ≤ l. Then σ is concave on [l, u], so any tangent line is an upper bound for σ over the interval. Output the tangent at the midpoint µ := l+u 2 : hU (z) = σ ′ (µ)(z − µ) + σ(µ). • Case 3: τ ≥ u. Output the secant line through the two interval endpoints: hU (z) =

σ(u) − σ(l) (z − l) + σ(l). u−l

3. Output (a, b) from the slope and intercept of hU . The proof of soundness for this selection (that it produces a valid upper bound) is given in Appendix H. 15

Algorithm 1 The CROWN algorithm. R ELAX produces linear relaxations of σ (see Section 5, and the selection algorithm in Appendix A.2). Require: Network {W(k) , b(k) }m k=1 , input x0 , perturbation budget ε, robustness claim (C, u) 1: for k = 1, . . . , m do ▷ outer forward pass (k) (k) (k) (k) 2: (A , d , A , d ) ← BACKWARD PASS(k) (k)

(k)

(L(k) , U (k) ) ← C ONCRETIZE(A(k) , d(k) , A , d , x0 , ε) for each neuron i in layer k < m do (k) (k) (k) (k) (k) (k) 5: (ai , bi , ai , bi ) ← R ELAX(σ, Li , Ui ) 6: end for 7: end for (m) 8: return True if U ≤ u entry-wise, else False otherwise Upper-bound pass (the lower-bound pass is analogous): 9: procedure BACKWARD PASS(k) 10: if k < m then 11: A ← W(k) , d ← b(k) 12: else if k = m then 13: A ← CW(k) , d ← Cb(k) 14: end if 15: for ℓ = k − 1, . . . , 1 do 16: (A, d) ← S TEP 1(A, d, ℓ) 17: (A, d) ← S TEP 2(A, d, ℓ) 18: end for 19: return (A, d) 20: end procedure 3: 4:

21: procedure S TEP 1(A, d, ℓ) 22: A+ ← max(A, 0), A− ← min(A, 0)

(k−1)

▷ initializes Ih

▷ final-layer initialization (ℓ)

(ℓ)

▷ Ih ⇒ Iz (ℓ−1) (ℓ) ▷ Iz ⇒ Ih (0)

▷ termination at Ih

▷ activation-relaxation update (11)

(ℓ)

d ← d + A+ b + A− b(ℓ) 24: A ← A+ diag(a(ℓ) ) + A− diag(a(ℓ) ) 25: return (A, d) 26: end procedure 23:

27: procedure S TEP 2(A, d, ℓ)

▷ linear-map substitution (12)

(ℓ)

28: d ← d + Ab 29: A ← A W(ℓ) 30: return (A, d) 31: end procedure

32: procedure C ONCRETIZE(A, d, A, d, x0 , ε) 33: A+ ← max(A, 0), A− ← min(A, 0) 34: A+ ← max(A, 0), A− ← min(A, 0) 35: U ← A+ (x0 + ε1) + A− (x0 − ε1) + d 36: L ← A+ (x0 − ε1) + A− (x0 + ε1) + d 37: return (L, U ) 38: end procedure

16

B

Details of PANDA

In this appendix, we present the PANDA system in full detail. Algorithm 2 presents the prover for the Four-Point Relaxation Gadget, accompanying Section 5.1. Appendix F further shows how to eliminate the Tσ′ table in Algorithm 2 through an optimization. Algorithms 3 and 4 present the full PANDA prover and verifier procedures, respectively. In our algorithms, ΠLOOKUP uses three precomputed public lookup tables over the quantization domain D: TReLU := {(x, ReLU(x)) : x ∈ D},

Tσ := {(x, σ(x)) : x ∈ D},

Tσ′ := {(x, σ ′ (x)) : x ∈ D}.

ΠLOOKUP is also used to perform range proofs, as discussed in Section 2.

Algorithm 2 Four-Point Relaxation Gadget prover (upper bound). Require: Witness (l, u, a, b, z1 , z2 ) and lookup tables Tσ , Tσ′ 1: Compute sl ← σ(l), su ← σ(u), s1 ← σ(z1 ), s2 ← σ(z2 ), s′1 ← σ ′ (z1 ), s′2 ← σ ′ (z2 ). 2: ΠLOOKUP .P ROVE ((l, sl ), (u, su ), (z1 , s1 ), (z2 , s2 ) ∈ Tσ ) . 3: ΠLOOKUP .P ROVE ((z1 , s′1 ), (z2 , s′2 ) ∈ Tσ ′ ). ▷ Left endpoint 4: ΠLOOKUP .P ROVE(al + b − sl ≥ 0). 5: ΠLOOKUP .P ROVE(au + b − su ≥ 0). ▷ Right endpoint 6: ΠLOOKUP .P ROVE(z1 ≤ 0) and ΠLOOKUP .P ROVE(z2 ≥ 0). ▷ Tangency point ordering ▷ Tangency point correctness 7: ΠARITH .P ROVE(s′i = a) for i ∈ {1, 2}. 8: ΠLOOKUP .P ROVE(az1 + b − s1 ≥ 0). ▷ Left tangency condition
9: ΠLOOKUP .P ROVE (u − z2 )(az2 + b − s2 ) ≥ 0 . ▷ Right tangency condition 10: return all proofs generated.

C

Comparison with FairProof

FairProof [31] 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. 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. Model FairProof Adult MNIST 2 × [20] ReLU MNIST 3 × [20] ReLU MNIST 2 × [1024] ReLU †

Offline prove (s)

Online prove (s)

Verify (s)

Proof (KB)

9.2

56.8 4/5 timeout (>1h), 1/5 OOM (>512GiB) — —

0.02

19.1

—

—

— —

— —

†

1908.0

timeout (>12h) timeout (>12h)

The offline phase completed, but the online phase was killed.

17

Algorithm 3 The PANDA prover. Public statement. Input point x0 ∈ Rn0 , perturbation budget ε > 0, model architecture, robustness claim (C, u), and commitments to witnesses. Private witnesses. Model parameters {W(k) , b(k) }m k=1 and all values in the quantized CROWN transcript (Section 4) generated by running Algorithm 1. P commits to the witnesses via ΠCOM . Prover claim. ∀x ∈ B(x0 , ε), Cf (x) ≤ u. Proof. P runs Algorithm 1, accumulating the following proofs along the way in a list Π: (1) Signed components. For each call A+ ←
max(A, 0), A− ← min(A, 0):

1: π+ ← ΠLOOKUP .P ROVE (A, A+ ) ⊂ TReLU

2: π− ← ΠLOOKUP .P ROVE (−A, −A− ) ⊂ TReLU 3: Π ← Π ∪ {π+ , π− }

(2) Activation-relaxation update. For each call (A′ , d′ ) ← S TEP
1(A, d, ℓ): 4: π1 ← ΠARITH .P ROVE A′ = A+ diag(a(ℓ) ) + A− diag(a(ℓ) )
(ℓ) ′ 5: π2 ← ΠARITH .P ROVE d = d + A+ b + A− b(ℓ) 6: Π ← Π ∪ {π1 , π2 } (3) Linear-map substitution. For each
call (A′ , d′ ) ← S TEP 2(A, d, ℓ): 7: π3 ← ΠARITH .P ROVE A′ = A W(ℓ)
′ (ℓ) 8: π4 ← ΠARITH .P ROVE d = d + A b 9: Π ← Π ∪ {π3 , π4 } (4) Concretization. For each call (L, U ) ← C ONCRETIZE(A, d, A, d, x0 , ε): 10: call (1) Signed components for A, A
11: π5 ← ΠARITH .P ROVE U = A+ (x0 + ε1) + A− (x0 − ε1) + d

12: π6 ← ΠARITH .P ROVE L = A+ (x0 − ε1) + A− (x0 + ε1) + d 13: Π ← Π ∪ {π5 , π6 }

(5) Activation relaxation. For each call (a, b, a, b) ← R ELAX(σ, L, U ): ▷ calls upper bound Alg. 2 ▷ lower bound is analogous

14: πu ← R ELAXATION -G ADGET(σ, L, U , a, b) 15: πl ← R ELAXATION -G ADGET(σ, L, U , a, b) 16: Π ← Π ∪ {πu , πl }

(6) Final robustness claim. After Algorithm 1 terminates at layer m, P proves that the final concretized upper bound U (m) is at most u entry-wise via a range proof. (m) 17: πfinal ← ΠLOOKUP .P ROVE(u − U ≥ 0) 18: Π ← Π ∪ {πfinal } (7) Quantization rescaling. For each rescaling qz = ⌊Sz qx /Sx ⌋ with committed remainder r: 19: πrem ← ΠLOOKUP .P ROVE(0 ≤ r < Sx ) ▷ This is rewritten as r ≥ 0 ∧ Sx − r > 0. 20: πdiv ← ΠARITH .P ROVE(Sz qx = Sx qz + r) 21: Π ← Π ∪ {πrem , πdiv } 22: return Π

Algorithm 4 The PANDA verifier. Require: Public statement x and proof Π from Algorithm 3. 1: for each proof π ← ΠARITH .P ROVE in Π do 2: run ΠARITH .V ERIFY(x, π) 3: end for 4: for each proof π ← ΠLOOKUP .P ROVE in Π do 5: run ΠLOOKUP .V ERIFY(x, π) 6: end for 7: for each relaxation-gadget proof π ∈ Π do 8: run V ERIFY-R ELAXATION -G ADGET(x, π) 9: end for 10: accept iff every check above passes

18

D

Complete 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 µ ± σ (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. Dataset

Structure

Act.

Prove (s)

Verify (s)

Proof CROWN (MB) (s)

Drift (%)

2 × [20] 2 × [20] 2 × [20] 3 × [20] 3 × [20] 3 × [20] 2 × [1024] 2 × [1024] 2 × [1024] 3 × [1024] (adv.) 3 × [1024] 3 × [1024] 3 × [1024] 4 × [1024] (adv.) 4 × [1024] 4 × [1024] 4 × [1024]

ReLU Sigmoid Tanh ReLU Sigmoid Tanh ReLU Sigmoid Tanh ReLU ReLU Sigmoid Tanh ReLU ReLU Sigmoid Tanh

22.81 ± 0.20 0.97 ± 0.01 58.35 ± 0.81 2.33 ± 0.03 58.77 ± 0.39 2.34 ± 0.03 42.64 ± 0.51 1.90 ± 0.03 99.62 ± 1.20 4.21 ± 0.05 105.56 ± 2.33 4.46 ± 0.10 41.70 ± 0.72 1.69 ± 0.02 74.60 ± 1.49 3.26 ± 0.06 83.17 ± 3.38 3.63 ± 0.15 90.79 ± 0.44 4.68 ± 0.03 101.58 ± 3.75 4.60 ± 0.13 172.29 ± 3.04 7.76 ± 0.14 179.27 ± 3.26 7.83 ± 0.15 172.16 ± 3.89 8.96 ± 0.15 226.08 ± 14.67 9.56 ± 0.48 327.47 ± 11.36 14.13 ± 0.46 333.94 ± 5.81 14.31 ± 0.28

3 8 8 6 14 15 4 9 9 9 9 19 20 16 17 31 32

0.00013 0.00014 0.00014 0.00018 0.00022 0.00019 0.06 0.06 0.07 0.22 0.22 0.21 0.21 0.45 0.44 0.47 0.46

2 × [128] 2 × [128] 3 × [64] [8, 2]

ReLU ReLU ReLU ReLU

23.04 ± 0.19 20.33 ± 0.19 36.61 ± 0.29 34.89

3 3 5 4

0.00013 -0.05 0.00014 -0.29 8.1e-5 -0.09 1.4e-5 -12.60

N

MNIST

Other SafeNLP med SafeNLP robot LunarLander FairProof Adult

E

0.81 ± 0.01 0.78 ± 0.01 1.46 ± 0.02 1.21

0.02 97 0.19 94 0.16 97 0.04 95 0.55 93 0.40 93 0.02 98 0.62 99 0.39 98 -0.18 97 0.03 98 1.66 98 1.83 98 0.01 98 -0.01 100 2.48 97 6.33 99 54 3 18 1

Prover Breakdown

We provide the component-wise breakdown of the prover time for three MNIST 3 × [20] models and three MNIST 3 × [1024] models in Table 4. Every row shows the mean over the first 5 properties 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.

F

Optimization: Finite Differences

The Four-Point Relaxation Gadget presented in Algorithm 2 requires lookup proofs against both the table Tσ = {(z, σ(z))} and the table Tσ′ = {(z, σ ′ (z))} for its derivative. The Tσ′ checks are equalities, which are more brittle in the quantized setting than inequalities, and precomputing both tables is a memory bottleneck. We therefore eliminate the Tσ′ table using the technique of finite differences. We use an additional condition that σ is strictly increasing. To prove that σ ′ (z) = α for fixed z ∈ R, α ∈ (0, B] up to some quantization error, it suffices to find a nearby z0 ∈ (z − δ, z + δ) satisfying σ(z0 + δ) − σ(z0 ) σ(z0 ) − σ(z0 − δ) ≤α≤ (20) δ δ where δ is an error threshold determined by the quantization; when σ is concave near z, the inequalities in (20) are reversed. Equation (20) can be encoded in Algorithm 2 using only the lookup tables for σ. The following theorem demonstrates the sufficiency of (20). 19

Table 4: Component-wise breakdown of the prover time. commit = polynomial commitments to every witness (Hyrax [28]); matmul = the matrix-multiplication verification ([26]); lookup = all lookup arguments (LogUp-GKR [21]); 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 of prove. Note the unit change on tangent. Cryptographic Structure

Act.

Non-crypto

prove

commit

matmul

lookup

other

total

tangent

total

Absolute time (s); tangent in ms 3 × [20] ReLU 45.08 3 × [20] Sigmoid 92.34 3 × [20] Tanh 116.45 3 × [1024] ReLU 106.95 3 × [1024] Sigmoid 170.13 3 × [1024] Tanh 196.80

0.93 0.86 0.94 15.70 16.17 20.62

0.35 0.33 0.36 8.54 8.50 10.49

43.59 90.25 113.27 66.08 127.50 144.39

0.21 0.89 1.87 0.51 2.70 3.42

45.07 92.33 116.44 90.82 154.86 178.91

0.000 0.009 0.013 0.000 0.022 0.646

0.01 0.01 0.01 16.12 15.26 17.84

As % of prove (prove in s) 3 × [20] ReLU 45.08 3 × [20] Sigmoid 92.34 3 × [20] Tanh 116.45 3 × [1024] ReLU 106.95 3 × [1024] Sigmoid 170.13 3 × [1024] Tanh 196.80

2.1 0.9 0.8 14.7 9.5 10.5

0.8 0.4 0.3 8.0 5.0 5.3

96.7 97.7 97.3 61.8 74.9 73.4

0.5 1.0 1.6 0.5 1.6 1.7

100.0 100.0 100.0 84.9 91.0 90.9

<0.01 <0.01 <0.01 <0.01 <0.01 <0.01

0.0 0.0 0.0 15.1 9.0 9.1

Theorem F.1 (Finite differences). Let σ satisfy Assumption 5.1 and also be strictly increasing and let δ > 0. Let D be the set of values exactly represented in our quantization, and suppose that the points of D are uniformly spaced with spacing at most δ. • If σ ′ (z) = α and σ is convex over (z −δ, z +δ), then there exists some z0 ∈ D ∩(z −δ, z +δ) such that σ(z0 ) − σ(z0 − δ) ≤ δα and σ(z0 + δ) − σ(z0 ) ≥ δα. • If σ ′ (z) = α and σ is concave over (z−δ, z+δ), then there exists some z0 ∈ D∩(z−δ, z+δ) such that σ(z0 ) − σ(z0 − δ) ≥ δα and σ(z0 + δ) − σ(z0 ) ≤ δα. Conversely, if sign(σ(z0 ) − σ(z0 − δ) − δα) ̸= sign(σ(z0 + δ) − σ(z0 ) − δα) then there exists some z ∈ (z0 − δ, z0 + δ) such that σ ′ (z) = α. Proof. Consider the first statement. Define the finite difference functions f (x) = σ(x) − σ(x − δ) and g(x) = σ(x + δ) − σ(x). Since σ is convex over (z − δ, z + δ), and its derivative σ ′ is strictly increasing over this region, which implies that f (x) and g(x) are also strictly increasing. By the Mean Value Theorem, there exists some c1 ∈ (z − δ, z) such that f (z) = δσ ′ (c1 ). Since c1 < z and σ ′ is increasing, σ ′ (c1 ) ≤ σ ′ (z) = α, giving f (z) ≤ δα. Similarly, there exists c2 ∈ (z, z + δ) such that g(z) = δσ ′ (c2 ). Since c2 > z, σ ′ (c2 ) ≥ σ ′ (z) = α, yielding g(z) ≥ δα. Define A = f −1 ((−∞, δα]) and B = g −1 ([δα, ∞)). Since f and g are increasing and continuous, A = (−∞, z+ ] and B = [z− , ∞) for some z− , z+ which satisfy f (z+ ) = δα = g(z− ). Also, z ∈ A ∩ B, so z− ≤ z+ and A ∩ B = [z− , z+ ]. Now observe that g(x) = f (x + δ) is simply a translation, which implies that g(z+ − δ) = f (z+ ) = δα. Since g is strictly increasing, z− is the unique point with g(z− ) = δα, so z− = z+ − δ and A ∩ B = [z− , z+ ] is of length δ. Since the points of D are spaced at most δ apart, there exists some point z0 ∈ D within A ∩ B, and this z0 therefore satisfies f (z0 ) = σ(z0 ) − σ(z0 − δ) ≤ δα and g(z0 ) = σ(z0 + δ) − σ(z0 ) ≥ δα. The second statement follows analogously, where σ ′ , f, and g are all instead decreasing. Now consider the converse statement. Without loss of generality, suppose that σ(z0 ) − σ(z0 − δ) − αδ ≤ 0

and 20

σ(z0 + δ) − σ(z0 ) − αδ ≥ 0.

By rearranging, we obtain σ(z0 ) − σ(z0 − δ) ≤α z0 − (z0 − δ)

and

σ(z0 + δ) − σ(z0 ) ≥ α. (z0 + δ) − z0

Then by the Mean Value Theorem, there exist some z0− ∈ (z0 − δ, z0 ) and z0+ ∈ (z0 , z0 + δ) such that σ ′ (z0− ) ≤ α and σ ′ (z0+ ) ≥ α. By the Intermediate Value Theorem applied to σ ′ , there must be some z ∈ (z0− , z0+ ) ⊂ (z0 − δ, z0 + δ) such that σ ′ (z) = α. The case where the signs are flipped follows similarly. Instantiation in Algorithm 2. This theorem shows that one can select a witness value z0 in our quantization which satisfies the above conditions, and z0 will be a δ-approximation of the solution z satisfying σ ′ (z) = α. For cases where σ is neither concave nor convex over (z − δ, z + δ), it suffices to pick z0 = 0 as a δ-approximation. Notably, these conditions only depend on σ and not σ ′ . This optimization can be encoded in Algorithm 2.

G

Proof of Lemma 5.1

Proof. By assumption, σ is convex on (−∞, 0) and concave on (0, +∞). Thus, σ ′ is continuous, bounded below by 0, strictly increasing on (−∞, 0) and strictly decreasing on (0, +∞). σ ′ attains its maximum at x = 0, where σ ′ (0) = B. Additionally, since σ is bounded, it follows that limx→±∞ σ ′ (x) = 0. Therefore, by the Intermediate Value Theorem applied to σ ′ , every point α ∈ (0, B) has one σ ′ -preimage in (−∞, 0) and one σ ′ -preimage in (0, +∞). For α = B, the unique preimage is z1 = z2 = 0, since σ ′ attains its maximum B only at x = 0.

H

Proof of Theorem 5.1

Theorem 5.1, part (a) (Case-free four-point soundness). Let σ satisfy Assumption 5.1, and fix an interval [l, u] ⊆ R. Consider a candidate linear upper bound hU (z) = az + b with a ∈ (0, B] and two (possibly coinciding) points of tangency z1 ≤ 0 ≤ z2 satisfying σ ′ (z1 ) = σ ′ (z2 ) = a. If the following conditions are satisfied, then hU is a valid upper bound on [l, u]. (i) Endpoints: σ(l) ≤ hU (l) and σ(u) ≤ hU (u). (ii) Left point of tangency: σ(z1 ) ≤ hU (z1 ).
(iii) Right point of tangency: 0 ≤ (u − z2 ) hU (z2 ) − σ(z2 ) . Consider a candidate linear lower bound hL (z) = az + b with a ∈ (0, B] and two (possibly coinciding) points of tangency z1 ≤ 0 ≤ z2 satisfying σ ′ (z1 ) = σ ′ (z2 ) = a. If the following conditions are satisfied, then hL is a valid lower bound on [l, u]. (i) Endpoints: σ(l) ≥ hL (l) and σ(u) ≥ hL (u). (ii) Right point of tangency: σ(z2 ) ≥ hL (z2 ).
(iii) Left point of tangency: 0 ≤ (z1 − l) σ(z1 ) − hL (z1 ) . Proof. We prove soundness for the upper bound, and the lower bound is analogous. Define f (z) := hU (z) − σ(z). It suffices to show f ≥ 0 on [l, u]. Since f is C 1 by Assumption 5.1, the critical points of f are the roots of f ′ given by solving f ′ (z) = a − σ ′ (z) = 0. By Lemma 5.1, there are two such solutions z which we label z1 , z2 . By the Interior Extremum Theorem, the minimum of f on [l, u] is attained either at an endpoint or at a critical point in (l, u). It therefore suffices to show f ≥ 0 at l, u, and at each critical point that falls inside [l, u]. • Endpoints: f (l), f (u) ≥ 0 by condition (i). 21

• Left critical point: f (z1 ) ≥ 0 by condition (ii). • Right critical point: if z2 ∈ [l, u]: – if z2 = u, f (z2 ) = f (u) ≥ 0 by condition (i). – if z2 < u, condition (iii) implies f (z2 ) ≥ 0. In all cases f ≥ 0 on [l, u], so hU ≥ σ on [l, u]. Remark. Many activations, such as sigmoid, tanh, and arctan, satisfy an additional property: their derivative σ ′ is an even function. For these functions z1 = −z2 , so it suffices to include only one of the two tangency points as a witness in Algorithm 2. Theorem 5.1, part (b) (Case-free four-point completeness). The CROWN algorithm selects linear relaxations hL and hU that satisfy the criteria of part (a). Proof. We prove the upper-bound case, and the lower bound is analogous. The selection procedure for hU (z) = az + b is described in Appendix A.2. We verify that each of its three cases produces an upper bound hU satisfying conditions (i), (ii), and (iii) of Theorem 5.1 part (a). Throughout, let z1 ≤ 0 ≤ z2 denote the tangency points satisfying σ ′ (z1 ) = σ ′ (z2 ) = a. Let τ denote the non-trivial root of σ(τ ) − σ(l) σ ′ (τ ) = , τ −l computed in step 1 of the selection procedure. τ is the unique value other than l itself at which the tangent line of σ(z) at z = τ coincides with the secant line through (l, σ(l)) and (τ, σ(τ )). We will use throughout this proof that τ and l must lie on opposite sides of the inflection point 0, and therefore have opposite signs. This is because any tangent line to σ will also intersect σ on the opposite side of the inflection point 0 and nowhere else, since σ ′′ changes signs only at z = 0. • Case 1: τ ∈ (l, u). The procedure outputs the line hU (z) = σ ′ (τ )(z − τ ) + σ(τ ), which is simultaneously tangent to σ at z = τ and is the secant connecting (l, σ(l)) to (τ, σ(τ )). It follows that a = σ ′ (τ ) and z2 = τ , where we use that τ > 0 since the tangent-secant point lies in the concave region. Condition (i): The left endpoint satisfies hU (l) = σ(l). For the right endpoint, σ(u) ≤ hU (u) since σ(τ ) = hU (τ ) for τ ∈ (l, u) and σ is concave on [τ, u] ⊂ [0, ∞). Condition (ii): Note that σ ′ (z) ≥ a for all z ∈ [z1 , z2 ]. It follows that Z z2 Z z2 adz = σ(z2 ) − a(z2 − z1 ). σ(z1 ) = σ(z2 ) − σ ′ (z)dz ≤ σ(z2 ) − z1

z1

Since hU has slope a and hU (z2 ) = σ(z2 ), the right-hand side is equal to hU (z2 ) − a(z2 − z1 ) = hU (z1 ). Thus, hU (z1 ) ≥ σ(z1 ). Condition (iii): This follows since hU (z2 ) − σ(z2 ) = 0. • Case 2: τ ≤ l. This implies that l ≥ 0, since if l < 0 then τ > 0, which contradicts Case 2. The procedure outputs the tangent line at the midpoint µ := (l + u)/2: hU (z) = σ ′ (µ)(z − µ) + σ(µ). Since [l, u] ⊂ [0, ∞), σ is concave on [l, u], so the tangent at any point within this interval dominates σ on the entire interval. It follows that a = σ ′ (µ) and z2 = µ. Condition (i): Since σ is concave on [l, u], the tangent line hU at µ ∈ [l, u] satisfies hU (l) ≥ σ(l) and hU (u) ≥ σ(u). Condition (ii): As in Case 1, hU is tangent to σ at z2 so hU (z2 ) = σ(z2 ). The identical integral argument over [z1 , z2 ] yields hU (z1 ) ≥ σ(z1 ). Condition (iii): This follows since hU (z2 ) − σ(z2 ) = 0. 22

• Case 3: τ ≥ u. This implies that l ≤ 0 and therefore τ > 0, since if l > 0 then τ < 0, which contradicts Case 3. The procedure outputs the secant line through (l, σ(l)) and (u, σ(u)): hU (z) =

σ(u) − σ(l) (z − l) + σ(l). u−l

We first observe that z2 ≥ u. Because τ maximizes the secant slope from l, we have σ ′ (τ ) =

σ(u) − σ(l) σ(τ ) − σ(l) ≥ = a = σ ′ (z2 ). τ −l u−l

Since τ, z2 ∈ [0, ∞) and σ ′ is decreasing over this interval, σ ′ (τ ) ≥ σ ′ (z2 ) implies z2 ≥ τ ≥ u. Condition (i): hU (l) = σ(l) and hU (u) = σ(u) by construction. Condition (ii): Note that z1 , l ≤ 0, so σ ′ is increasing between l and z1 . Thus, if z1 ≤ l then σ ′ (z) ≥ a for z ∈ [z1 , l], and if z1 > l then σ ′ (z) ≤ a for z ∈ [l, z1 ]. Either way, Z l Z l ′ σ(z1 ) = σ(l) − σ (z)dz ≤ σ(l) − adz = σ(l) − a(l − z1 ) = hU (z1 ). z1

z1

Condition (iii): Since z2 ≥ u, the first factor satisfies u − z2 ≤ 0. We show that the second factor satisfies hU (z2 ) − σ(z2 ) ≤ 0. To see this, note that σ ′ (z) ≥ a for all z ∈ [z1 , z2 ], and that z1 ∈ [l, u] by the Mean Value Theorem, implying that σ ′ (z) ≥ a for all z ∈ [u, z2 ]. Integrating yields Z z2 Z z2 σ ′ (z)dz ≥ σ(u) + adz = σ(u) + a(z2 − u). σ(z2 ) = σ(u) + u

u

Since hU has slope a and hU (u) = σ(u), the right-hand side is equal to hU (u) + a(z2 − u) = hU (z2 ). Thus, σ(z2 ) ≥ hU (z2 ).

23

Related documents

• Privacy-Preserving Robustness Verification for Neural Networks#343360
• Triggering Stealthy Feature Map Backdoors via Physical Fault Injection in Embedded Neural Networks#361405
• Universal Adversarial Perturbations#6677
• Efficient Privacy-Preserving Federated Learning with Sensitivity-Based Selective Homomorphic Encryption#431809
• Privacy-Preserving Machine Learning: Methods, Challenges and Directions#434595