Training Mixed-Monotone Neural Networks for Verification Without Set Propagation

Jonas Fingerhut; Lukas Koller; Matthias Althoff

cs.LGOct 22, 2026

Training Mixed-Monotone Neural Networks for Verification Without Set Propagation

Authors: Jonas Fingerhut, Lukas Koller, Matthias Althoff

Organizations: Technical University of Munich

Abstract

Most formal verification approaches for neural networks conservatively enclose the output set of the neural network. However, computing a tight output enclosure is in general computationally hard. We sidestep this challenge with a novel neural network architecture that realizes mixed-monotone functions as the difference of monotone subnetworks. By utilizing the theory on mixed-monotone systems, this reduces the computation of a tight output enclosure from complicated set propagation to two simple forward passes of opposite corners of an input interval. Moreover, because the size of the resulting enclosure is a closed-form function of the weights of the neural network, we can directly minimize it during training. We prove a lower bound on the size of any such enclosure, given by the total variation of the represented function generalized to several inputs, which makes it possible to compare the tightness of the enclosure against the optimum. Our evaluation on regression and dynamical-system benchmarks demonstrates that our training reduces the enclosure size to within 0.5% of the lower bound without sacrificing prediction accuracy. Computing our enclosure is orders of magnitude faster than CROWN and $α$ -CROWN and on deep networks it is also tighter than zonotope propagation and CROWN, while its size exceeds that of $α$ -CROWN by only 5.1%.

Figures & tables

Panel of Figure 1 — Figure 1: Our neural network architecture is the difference of two monotone subnetworks $\Phi_{+}$ and $\Phi_{-}$ . Evaluating both subnetworks at the two opposite corners of the input interval yields an output enclosure without set propagation.

Panel of Figure 2 — Figure 2: The size of an enclosure depends on the decomposition: For the same function $f$ , two decompositions yield enclosures of different sizes.

Benchmark	#Layers $\kappa$	Accuracy $\uparrow$
Benchmark	#Layers $\kappa$	Baseline		Ours
Scalar analytic	2	$0.9837$ $\,\pm\,$	$0.0018$	$\mathbf{0.9858}$ $\,\pm\,$	$0.0009$
	4	$\mathbf{0.9998}$ $\,\pm\,$	$0.0001$	$0.9895$ $\,\pm\,$	$0.0051$
	8	$\mathbf{0.9997}$ $\,\pm\,$	$0.0003$	$0.9964$ $\,\pm\,$	$0.0035$
Pendulum	3	$\mathbf{0.9942}$ $\,\pm\,$	$0.0024$	$0.9878$ $\,\pm\,$	$0.0071$
Pendulum	8	$\mathbf{0.9931}$ $\,\pm\,$	$0.0049$	$0.9868$ $\,\pm\,$	$0.0098$

Table 1: Comparing prediction accuracy across different benchmarks shown as mean

\pm

standard deviation over ten seeds.

#Layers $\kappa$	Framework	Method	Tightness $\downarrow$		Runtime $\downarrow$
#Layers $\kappa$	Framework	Method	Tightness $\downarrow$		[ ms ]	[relative to ours]
4	auto_LiRPA	Ours (exported)	$1.1662$ $\,\pm\,$	$0.1167$	$\mathbf{0.12}$	$1\times$
		IBP	$1.1662$ $\,\pm\,$	$0.1167$	$1.21$	$9.9\times$
		CROWN	$1.1264$ $\,\pm\,$	$0.0371$	$13.7$	$112\times$
		$\alpha$ -CROWN	$\mathbf{1.0024}$ $\,\pm\,$	$0.0025$	$1\,070$	$8\,750\times$
	CORA	Ours	$1.1662$ $\,\pm\,$	$0.1167$	$\mathbf{0.01}$	$1\times$

Table 2: Comparing enclosure tightness and runtimes on the scalar analytic model shown as mean

\pm

standard deviation over five seeds. The runtime is the time to enclose the output set for one input interval, reported as the minimum over repeated measurements ( Sec. A.6 and A.6 ). We evaluate our approach within CORA as well as within auto_LiRPA .

Benchmark	$\beta$	Accuracy $\uparrow$		Tightness $\downarrow$
Scalar analytic	$0$	$0.9846$ $\,\pm\,$	$0.0007$	$1.821$ $\,\pm\,$	$0.136$
	$0.01$	$0.9857$ $\,\pm\,$	$0.0034$	$1.024$ $\,\pm\,$	$0.009$
	$0.05$	$\mathbf{0.9883}$ $\,\pm\,$	$0.0012$	$1.004$ $\,\pm\,$	$0.003$
	$0.2$	$0.9803$ $\,\pm\,$	$0.0012$	$\mathbf{1.000}$ $\,\pm\,$	$0.000$
	$1.0$	$0.9392$ $\,\pm\,$	$0.0121$	$\mathbf{1.000}$ $\,\pm\,$	$0.000$
Tanks	$0$	$\mathbf{0.9999}$ $\,\pm\,$	$0.0000$	$1.883$ $\,\pm\,$	$0.134$

Table 3: Comparing the accuracy and enclosure tightness for varying

\beta

in the loss function 5 shown as mean

\pm

standard deviation over three seeds.

#Input Dims	Tightness $\downarrow$
#Input Dims	Zonotope		Ours
2	$1.65$ $\,\pm\,$	$0.01$	$\mathbf{1.045}$ $\,\pm\,$	$0.008$
20	$1.77$ $\,\pm\,$	$0.09$	$\mathbf{1.073}$ $\,\pm\,$	$0.009$
100	$360$ $\,\pm\,$	$31$	$\mathbf{1.167}$ $\,\pm\,$	$0.039$

Table 4: Comparing the enclosure tightness for different numbers of input dimensions shown as mean

\pm

standard deviation over five seeds.

#Layers $\kappa$	Tightness $\downarrow$				Crossover Radius $\downarrow$ [median (range)]
#Layers $\kappa$	Zonotope		Ours		Crossover Radius $\downarrow$ [median (range)]
2	$\mathbf{1.08}$ $\,\pm\,$	$0.01$	$5.92$ $\,\pm\,$	$0.79$	–
3	$\mathbf{1.11}$ $\,\pm\,$	$0.02$	$2.47$ $\,\pm\,$	$0.72$	$1.00$ ( $0.1$ – $1.5$ )
4	$\mathbf{1.14}$ $\,\pm\,$	$0.03$	$1.56$ $\,\pm\,$	$0.37$	$0.20$ ( $0.03$ – $0.5$ )
6	$1.24$ $\,\pm\,$	$0.12$	$\mathbf{1.13}$ $\,\pm\,$	$0.12$	$0.025$ ( $0.01$ – $0.15$ )
8	$1.38$ $\,\pm\,$	$0.25$	$\mathbf{1.19}$ $\,\pm\,$	$0.18$	$0.04$ ( $0.01$ – $0.075$ )

Table 5: Comparing the enclosure tightness for different numbers of neural network layers shown as mean

\pm

standard deviation over ten seeds. The crossover radius is reported as median (range) over seeds; “–” indicates no crossover.

Panel of Figure 3 — Figure 3: Size of the enclosure of the reachable set over time for the Tanks system, when the neural network is applied iteratively.

Appendix figures & tables4 assets

Supplementary material from the paper’s appendix.

Appendix

Experiment	Benchmark	#Layers $\kappa$	$\beta$	#Seeds	#Epochs	#Input Sets
Tab. 1 and 7	Scalar analytic	2, 3, 4, 6, 8	0	10	120	–
Tab. 1	Pendulum, Tanks	3, 8	0	10	100	–
Tab. 2 and 8	Scalar analytic	2, 3, 4, 6, 8	0	5	120	100
Tab. 3	Scalar analytic, Tanks	3	0–1	3	80	150
Tab. 4 and 9	Multi-input analytic	4	0.05	5	120	100
Tab. 5	Scalar analytic	2, 3, 4, 6, 8	0	10	120	150

Appendix

Table 6: Settings of the experiments.

#Layers $\kappa$	Architecture
#Layers $\kappa$	Baseline (unconstr.)		Ours (sign-constr)		Lip.-res. (monotone) Kitouni et al. (2023)		Lip. (non-monotone)
2	$0.984$ $\,\pm\,$	$0.002$	$\mathbf{0.986}$ $\,\pm\,$	$0.001$	$0.973$ $\,\pm\,$	$0.002$	$0.972$ $\,\pm\,$	$0.002$
3	$\mathbf{0.999}$ $\,\pm\,$	$0.002$	$0.992$ $\,\pm\,$	$0.003$	$0.983$ $\,\pm\,$	$0.001$	$0.983$ $\,\pm\,$	$0.001$
4	$\mathbf{1.000}$ $\,\pm\,$	$0.000$	$0.990$ $\,\pm\,$	$0.005$	$0.982$ $\,\pm\,$	$0.001$	$0.981$ $\,\pm\,$	$0.001$
6	$\mathbf{1.000}$ $\,\pm\,$	$0.000$	$0.992$ $\,\pm\,$	$0.006$	$0.876$ $\,\pm\,$	$0.022$	$0.838$ $\,\pm\,$	$0.028$
8	$\mathbf{1.000}$ $\,\pm\,$	$0.000$	$0.996$ $\,\pm\,$	$0.004$	$0.752$ $\,\pm\,$	$0.048$	$0.635$ $\,\pm\,$	$0.074$

Appendix

Table 7: Comparing the prediction accuracy of different architectures on the scalar analytic model shown as mean

\pm

standard deviation over ten seeds; bold font marks the best architecture per number of layers.

#Layers $\kappa$	Tightness $\downarrow$								Runtime relative to ours $\downarrow$
#Layers $\kappa$	Ours / IBP		Zonotope		CROWN		$\alpha$ -CROWN		IBP	Zono.	CROWN	$\alpha$ -CR.
2	$3.58$ $\,\pm\,$	$0.55$	$1.08$ $\,\pm\,$	$0.01$	$1.07$ $\,\pm\,$	$0.01$	$\mathbf{1.001}$ $\,\pm\,$	$0.000$	$10.8$	$6.5$	$23.5$	$1\,490$
3	$2.00$ $\,\pm\,$	$0.43$	$1.14$ $\,\pm\,$	$0.03$	$1.12$ $\,\pm\,$	$0.03$	$\mathbf{1.004}$ $\,\pm\,$	$0.002$	$8.1$	$8.4$	$54.4$	$6\,130$
4	$1.17$ $\,\pm\,$	$0.12$	$1.16$ $\,\pm\,$	$0.05$	$1.13$ $\,\pm\,$	$0.04$	$\mathbf{1.002}$ $\,\pm\,$	$0.002$	$9.9$	$11.7$	$112$	$8\,750$
6	$1.07$ $\,\pm\,$	$0.08$	$1.25$ $\,\pm\,$	$0.10$	$1.18$ $\,\pm\,$	$0.04$	$\mathbf{1.002}$ $\,\pm\,$	$0.001$	$10.2$	$19.6$	$193$	$12\,900$
8	$1.05$ $\,\pm\,$	$0.08$	$1.44$ $\,\pm\,$	$0.07$	$1.26$ $\,\pm\,$	$0.06$	$\mathbf{1.002}$ $\,\pm\,$	$0.001$	$11.2$	$31.8$	$256$	$20\,600$

Appendix

Table 8: Comparing enclosure tightness and runtimes of all verification methods on the scalar analytic model at

\epsilon=0.05

for all tested numbers of layers. The tightness is shown as mean

\pm

standard deviation over five seeds, and the runtimes are relative to our enclosure within the same toolbox; bold font marks the best tightness per number of layers.

Perturbed	$n_{0}$	Input Set Size $\lVert\mathcal{X}\rVert_{\mathrm{I}}$	Ours		Lip.-res. Kitouni et al. (2023)		Zonotope
all	$2$	$1.92$	$1.045$ $\,\pm\,$	$0.008$	$19.4$ $\,\pm\,$	$0.4$	$1.65$ $\,\pm\,$	$0.01$
	$5$	$4.82$	$1.054$ $\,\pm\,$	$0.012$	$38.2$ $\,\pm\,$	$3.2$	$1.59$ $\,\pm\,$	$0.05$
	$10$	$9.56$	$1.050$ $\,\pm\,$	$0.009$	$86.5^{\dagger}$ $\,\pm\,$	$6.9$	$1.66$ $\,\pm\,$	$0.08$
	$20$	$19.18$	$1.073$ $\,\pm\,$	$0.009$	$181^{\dagger}$ $\,\pm\,$	$37$	$1.77$ $\,\pm\,$	$0.09$
	$50$	$47.90$	$1.105$ $\,\pm\,$	$0.013$	$378^{\dagger}$ $\,\pm\,$	$38$	$152^{\dagger}$ $\,\pm\,$	$12$
	$100$	$95.91$	$1.167$ $\,\pm\,$	$0.039$	$862^{\dagger}$ $\,\pm\,$	$95$	$360^{\dagger}$ $\,\pm\,$	$31$

Appendix

Table 9: Comparing the enclosure tightness for different input dimensions

n_{0}

\epsilon=0.5

, when all inputs or only the first two inputs are perturbed, shown as mean

\pm

standard deviation over five seeds;

\dagger

marks configurations with

R^{2}<0.9

( Sec. A.3 ).

Neural Network Verification

Neural network verification develops methods to prove whether networks satisfy properties such as robustness, safety, and bounded output behavior.

See all 126 papers

Neural Network Verification using Partial Multi-Neuron Relaxation
May 28, 2026Ido Shmuel, Guy KatzNeural Network Verification
The Hebrew University of Jerusalem, Jerusalem, Israel
The Cost of Relaxation: Evaluating the Error in Convex Neural Network Verification
Apr 20, 2026Merkouris Papamichail, Konstantinos Varsos, Giorgos Flouris +1Neural Network Verification Certified Robustness
Foundation for Research and Technology – Hellas, Heraklion, Greece · University of Crete, Heraklion, Greece · Catalan Institution for Research and Advanced Studies, Barcelona, Spain +1
Mining Verdict Boundaries for Neural Network Verification
Jul 31, 2026Jiawei Ren, Guanqin Zhang, Zhenya Zhang +1Neural Network Verification Branch and Bound
University of New South Wales, Sydney, Australia · Kyushu University, Fukuoka, Japan · National Institute of Informatics, Tokyo, Japan

May 28, 2026J/K move · Enter open · S save

Neural Network Verification using Partial Multi-Neuron Relaxation

Ido Shmuel, Guy Katz

The Hebrew University of Jerusalem, Jerusalem, Israel

Neural Network Verification

Open paper AskPDF arXiv

The increasing integration of deep neural networks in critical systems has spawned a theoretical and practical interest in formally guaranteeing safety properties about their behavior. To achieve this, contemporary verification algorithms rely on computing linear relaxations for a network's non-linear activation functions. Existing approaches for linear relaxations typically fall into one of two categories: single-neuron relaxation, in which each activation neuron is bounded in terms of its sources; and multi-neuron relaxation, in which linear bounds involving multiple activation neurons and their sources are calculated. However, existing methods might fail to balance tightness and scalability, as single-neuron bounds might not derive sufficiently tight bounds necessary for verification to complete, whereas generating multi-neuron relaxation for all activation neurons is computationally expensive. In this paper, we present a middle-ground approach featuring partial multi-neuron relaxation, in which we generate multi-neuron bounds for only a small, heuristically selected subset of neurons. To achieve this, we build upon existing branching heuristics for selecting neurons and for optimizing bounding hyper-planes for multi-neuron bounds. We integrated our proposed method within the Marabou verifier, and obtained favorable results in comparison to existing bound tightening methods. Our experiments showcase the potential of our technique for neural network verification.

Abstract

Neural Network Verification

Explore similar work

Neural Network Verification using Partial Multi-Neuron Relaxation

The Cost of Relaxation: Evaluating the Error in Convex Neural Network Verification

Mining Verdict Boundaries for Neural Network Verification