arXiv subjects

Philipp Kern

Publications and source records attributed to Philipp Kern.

5 recordsLinked to original sources

arXiv2026

Shifting-based Optimizable Linear Relaxations for General Activation Functions

The use of neural networks (NNs) is rapidly increasing, including in safety- and security-critical domains. To provide formal guarantees about NN behavior, many verification methods rely on optimizable linear relaxations of activation functions. However, existing techniques depend on hand-crafted relaxations for each activation function. Extension to state-of-the-art activation functions therefore requires substantial manual effort. In contrast, our approach SLiR (Shifting-based Linear Relaxations) is broadly applicable, requiring only a Lipschitz constant or a set of critical points. SLiR parameterizes relaxations by their slope and computes the corresponding offset via a shifting procedure that ensures sound upper and lower bounds over the input domain, enabling efficient optimization while maintaining correctness. Our experiments show that SLiR produces tight relaxations across a wide range of practical activation functions and enables verification of up to 7.8x more properties compared to state-of-the-art methods.

cs.LG↗

arXiv2026

Encrypted Neural Networks without Overflows

The popular Cheon-Kim-Kim-Song (CKKS) scheme enables efficient private inference in neural networks by evaluating them on encrypted data. Since CKKS only supports addition, multiplication, and array rotation operations, turning neural networks into CKKS circuits requires approximating all activation functions (e.g. ReLU) with polynomials over fixed input ranges. Traditionally, these ranges are estimated via heuristic sampling techniques. In this paper, we empirically demonstrate that sampled ranges leave the CKKS network exposed to overflow events, i.e. legitimate inputs that exceed the ranges of the circuit and cause corrupted outputs, and propose an improved design technique that completely avoids them. First, we propose a practical algorithm to induce overflow events in a CKKS circuit, i.e. we automatically craft legitimate inputs that exceed the design ranges within the circuit and cause corrupted outputs. As an example, our algorithm can quickly corrupt around 47% of benign inputs in a CIFAR10 neural network. Second, we propose an end-to-end formal verification approach that constructs executable CKKS circuits. These circuits are guaranteed to be overflow-free and come with certified error bounds on the output difference w.r.t. the original neural network. Our experiments demonstrate that our approach supports a larger set of neural network architectures than prior certified techniques, while also delivering executable CKKS artifacts.

cs.CR↗

arXiv2024

Revisiting Differential Verification: Equivalence Verification with Confidence

When validated neural networks (NNs) are pruned (and retrained) before deployment, it is desirable to prove that the new NN behaves equivalently to the (original) reference NN. To this end, our paper revisits the idea of differential verification which performs reasoning on differences between NNs: On the one hand, our paper proposes a novel abstract domain for differential verification admitting more efficient reasoning about equivalence. On the other hand, we investigate empirically and theoretically which equivalence properties are (not) efficiently solved using differential reasoning. Based on the gained insights, and following a recent line of work on confidence-based verification, we propose a novel equivalence property that is amenable to Differential Verification while providing guarantees for large parts of the input space instead of small-scale guarantees constructed w.r.t. predetermined input points. We implement our approach in a new tool called VeryDiff and perform an extensive evaluation on numerous old and new benchmark families, including new pruned NNs for particle jet classification in the context of CERN's LHC where we observe median speedups >300x over the State-of-the-Art verifier alpha,beta-CROWN.

cs.LG↗

arXiv2022

Optimized Symbolic Interval Propagation for Neural Network Verification

Neural networks are increasingly applied in safety critical domains, their verification thus is gaining importance. A large class of recent algorithms for proving input-output relations of feed-forward neural networks are based on linear relaxations and symbolic interval propagation. However, due to variable dependencies, the approximations deteriorate with increasing depth of the network. In this paper we present DPNeurifyFV, a novel branch-and-bound solver for ReLU networks with low dimensional input-space that is based on symbolic interval propagation with fresh variables and input-splitting. A new heuristic for choosing the fresh variables allows to ameliorate the dependency problem, while our novel splitting heuristic, in combination with several other improvements, speeds up the branch-and-bound procedure. We evaluate our approach on the airborne collision avoidance networks ACAS Xu and demonstrate runtime improvements compared to state-of-the-art tools.

cs.LG↗

arXiv2021

Geometric Path Enumeration for Equivalence Verification of Neural Networks

As neural networks (NNs) are increasingly introduced into safety-critical domains, there is a growing need to formally verify NNs before deployment. In this work we focus on the formal verification problem of NN equivalence which aims to prove that two NNs (e.g. an original and a compressed version) show equivalent behavior. Two approaches have been proposed for this problem: Mixed integer linear programming and interval propagation. While the first approach lacks scalability, the latter is only suitable for structurally similar NNs with small weight changes. The contribution of our paper has four parts. First, we show a theoretical result by proving that the epsilon-equivalence problem is coNP-complete. Secondly, we extend Tran et al.'s single NN geometric path enumeration algorithm to a setting with multiple NNs. In a third step, we implement the extended algorithm for equivalence verification and evaluate optimizations necessary for its practical use. Finally, we perform a comparative evaluation showing use-cases where our approach outperforms the previous state of the art, both, for equivalence verification as well as for counter-example finding.

cs.LG↗