Automatic Tensor-level Execution of Abstract Interpreters for Neural Networks

Avaljot Singh; Yasmin Chandini Sarita; Aditya Mishra; Gagandeep Singh; Charith Mendis

cs.CLJul 26, 2025

Automatic Tensor-level Execution of Abstract Interpreters for Neural Networks

Authors: Avaljot Singh, Yasmin Chandini Sarita, Aditya Mishra, Gagandeep Singh, Charith Mendis

Organizations: University of Illinois Urbana-Champaign, USA

Abstract

Developing new abstract interpretation-based DNN certifiers is difficult because their mathematical design is expressed at the neuron level, while implementations must operate at the tensor level. Existing libraries such as auto_LiRPA, IVAN, and ERAN support fixed sets of certifiers; extending them requires expertise in formal methods and tensor programming. Domain-specific languages such as ConstraintFlow let researchers specify certifiers at the neuron level, but cannot run them on real DNNs. We present Neuton, a framework that automatically translates neuron-level certifier specifications into tensor-level executables, enabling new DNN certifiers without manual tensor programming. Neuton makes three contributions. First, a stack-based intermediate representation (IR) and shape analysis infer implicit tensor operations, including broadcasts, dimension expansions, and reductions, required for correct execution. Second, domain-specific rewrite rules optimize common tensor operation sequences into more efficient equivalents. Third, gBCSR is a sparse tensor format using variable-sized, layer-aligned blocks over a non-zero default value, tailored to DNN certifier sparsity. We prove that translation preserves neuron-level semantics. We evaluate Neuton on 8 certifiers and 32 DNN benchmarks. Neuton compiles four existing certifiers and produces the first executable implementations of four others: two previously specified but never run, and two new designs. These expose precision-runtime trade-offs unavailable in existing libraries. For example, SkipPoly matches DeepPoly's precision on all 32 DNNs while running as fast or faster on half. Neuton's runtime on existing certifiers is competitive with hand-optimized libraries. Code: https://github.com/uiuc-focal-lab/constraintflow.git

Figures & tables

Required Features	Libraries	Specification DSLs	Neuton
	(e.g., auto_LiRPA, ERAN, IVAN)	(e.g., ConstraintFlow )	(This Work)
Execution on real DNNs	✓	✗	✓
Supports user-defined certifiers	✗	✓	✓
Certifiers specified without tensor programming	✗	✓	✓
Automatically derived tensor implementation	✗	✗	✓

Table 1. Comparison of existing tool classes and Neuton across key capabilities.

Panel of Figure 2 — Figure 2. Tensorized computation of g( prev . dot ( curr [w] )).

Figure 3. Overview of the compilation pipeline.

Figure 4. Neuton IR for g( prev . dot ( curr [w] )) applied to

m

neurons. Each node carries stack-based metadata. Each element of the stack is

\langle\text{intrinsic shape},\text{broadcast factor}\rangle

. The top element also records the type of the expression. Purple nodes arise from the map construct; orange nodes are tensor operations inserted automatically by shape analysis.

P\equiv\texttt{\footnotesize{\color[rgb]{0,0.5,0}{PolyExp}}}

R\equiv\texttt{\footnotesize{\color[rgb]{0,0.5,0}{Real}}}

N\equiv\texttt{\footnotesize{\color[rgb]{0,0.5,0}{Neuron}}}

Panel of Figure 5 — Figure 5. Code generated by Neuton corresponding to the IR in Fig. 4 . Purple calls are ConstraintFlow -specific (operations on polyhedral expressions); orange calls are the g-BCSR tensor API.

Panel of Figure 6 — Figure 6. Examples of tensor sparsity patterns observed across different certifiers and DNN architectures. Blue = dense block (fully connected layer); red = diagonal block (ReLU); green = stencil block.

\frac{\Gamma,\sigma,F\vdash e^{\prime}\leadsto(i_{s_{1}},\,i_{e_{1}},\,m_{1})\hskip 9.24994ptF(f)=(n_{f},\,c_{f},\,e_{f})\hskip 9.24994ptm_{e}^{\mathrm{map}}=\langle\texttt{\footnotesize{\color[rgb]{0,0.5,0}{Neuron}}},\;\mathsf{false},\;[\textsf{polySize}],\;[1]\rangle\hskip 9.24994pt\sigma^{+}=\sigma\bigl[n_{f}\mapsto(\textsf{IrMapNeuron}(i_{e_{1}}),\;m_{e}^{\mathrm{map}}{::}m_{1}^{bc}),\;c_{f}\mapsto(\textsf{IrMapCoeff}(i_{e_{1}}),\;m_{e}^{\mathrm{map}}{::}m_{1})\bigr]\hskip 9.24994pt\Gamma,\;\sigma^{+},\;F\;\vdash\;e_{f}\;\leadsto\;(i_{s_{f}},\;i_{e_{f}},\;m_{e}^{f}{::}m_{\mathit{out}})\hskip 9.24994pti_{e_{pc}}=\textsf{IrReduce}(i_{e_{f}}.C,\;m_{e}^{f})\hskip 9.24994pti_{e_{pz}}=\textsf{IrReduce}(i_{e_{f}}.k,\;m_{e}^{f})\hskip 9.24994pt\textsf{alignShapes}(i_{e_{1}}.k,\;m_{1}[t{\mapsto}\texttt{\footnotesize{\color[rgb]{0,0.5,0}{Real}}}],\;i_{e_{pz}},\;m_{\mathit{out}})=(i_{e_{k}}^{\prime},\;i_{e_{pz}}^{\prime},\;m^{\prime})}{\Gamma,\;\sigma,\;F\;\vdash\;e^{\prime}.\texttt{\footnotesize{\color[rgb]{0.05,0.05,0.9}{map}}}(f)\;\leadsto\;\Bigl(\textsf{IrSeq}(i_{s_{1}},\;i_{s_{f}}),\;\textsf{IrCombineToPoly}\bigl(i_{e_{pc}},\;\textsf{IrBinary}(i_{e_{k}}^{\prime},\;i_{e_{pz}}^{\prime},\;{+})\bigr),\;m^{\prime}\Bigr)}\hskip 9.24994pt\textsc{Left={Map}}

Figure 8. Shape analysis of map on a polyhedral expression. Notation:

i_{e}.C\triangleq\textsf{IrExtractPolyCoeff}(i_{e})

;

i_{e}.k\triangleq\textsf{IrExtractPolyConst}(i_{e})

;

m^{bc}

: metadata stack with the polySize dimension moved to the broadcast factor.

Panel of Figure 9 — Figure 9. Domain-specific rewrite rules. Preconditions appear beneath each rule.

Panel of Figure 10 — Figure 10. Dense and sparse representations of Stencil, Window, and Diagonal blocks. Different colors represent different values. In each pair, the left shows the dense block and the right shows its g-BCSR form.

DNN	Dataset	Model	Training Method	Architecture	Layers	Perturbation ( $\epsilon$ )	Batch Size
$N{10}$	MNIST	6x500	PGD	FCN	6	0.005	100
$N{11}$	MNIST	4x1024	Standard	FCN	3	0.004	100
$N{14}$	MNIST	ConvSmall	DiffAI	Convolutional	3	0.1	100
$N{22}$	CIFAR10	6x500	Standard	FCN	6	4e-5	100
$N{30}$	CIFAR10	ConvMed	PGD	Convolutional	3	5e-4	10
$N{32}$	CIFAR10	ConvBig	DiffAI	Convolutional	6	0.002	10

Table 2. Six representative DNNs for evaluation.

	Existing Implementations				Prototype Specifications		New Designs
	IBP	CROWN-IBP	DeepZ	DeepPoly	ReuseCert	PolyZono	SkipPoly	ZID
ConstraintFlow LOCs	11	27	14	27	25	35	22	67
auto_LiRPA	✓	✓	✗	✓	✗	✗	✗	✗
IVAN	✓	✗	✓	✓	✗	✗	✗	✗
ERAN	✗	✗	✓	✓	✗	✗	✗	✗
Neuton	✓	✓	✓	✓	✓	✓	✓	✓

Table 3. Certifiers supported by Neuton vs. existing libraries, and their ConstraintFlow specification sizes.

Figure 11. Runtime and precision of new and existing DNN certifiers across various DNNs.

Figure 12. Runtime and Precision of running the DeepPoly algorithm by the number of layers backsubstituted.

Figure 13. Per-DNN runtime of Neuton vs. (a) existing libraries (

=

auto_LiRPA,

=

IVAN,

=

ERAN) and (b) its variants (

=

N–S ,

=

N–R ,

=

N–R–S ). Each point is one of the 32 DNNs (log–log axes); a point below the dashed diagonal means Neuton is faster. x markers denote that the variant times out (200 s).

Appendix figures & tables16 assets

Supplementary material from the paper’s appendix.

Appendix

\frac{m_{k}=m_{e_{k}}::m_{k}^{\prime}\hskip 18.49988ptm_{e_{k}}^{*}=\mathrm{ext}(m_{e_{k}},\;m_{e_{3-k}})\hskip 9.24994ptk=1,2\hskip 9.24994pt\hskip 9.24994pti_{e_{k}}^{*}=\textsf{IrAddDimension}(i_{e_{k}},\,m_{e_{k}}^{*})\;\text{if}\;|m_{e_{k}}|<|m_{e_{3-k}}|,\;\text{else}\;i_{e_{k}}\hskip 9.24994ptk=1,2\hskip 9.24994pt\hskip 9.24994ptm=\textsf{LCM}(m_{e_{1}}^{*}::m_{1}^{\prime},\;m_{e_{2}}^{*}::m_{2}^{\prime})}{\textsf{alignShapes}(i_{e_{1}},\;i_{e_{2}},\;m_{1},\;m_{2})=\bigl(\textsf{IrRepeat}(i_{e_{1}}^{*},\,m),\;\textsf{IrRepeat}(i_{e_{2}}^{*},\,m),\;m\bigr)}\hskip 9.24994pt\textsc{Left={AlignShapes}}

Appendix

Figure 16. Shape alignment rule.

\frac{}{\varrho\vdash\textsf{IrConst}(c)\Downarrow^{\mathrm{ir}}\bar{c}}\hskip 9.24994pt\textsc{lab={E-Const}}\frac{}{\varrho\vdash x\Downarrow^{\mathrm{ir}}\varrho(x)}\hskip 9.24994pt\textsc{lab={E-Var}}\frac{\varrho\vdash i_{e_{1}}\Downarrow^{\mathrm{ir}}T_{1}\hskip 9.24994pt\varrho\vdash i_{e_{2}}\Downarrow^{\mathrm{ir}}T_{2}}{\varrho\vdash\textsf{IrBinary}(i_{e_{1}},i_{e_{2}},\oplus)\Downarrow^{\mathrm{ir}}T_{1}\mathbin{\oplus}T_{2}}\hskip 9.24994pt\textsc{lab={E-Bin}}\frac{\varrho\vdash i_{e}\Downarrow^{\mathrm{ir}}T}{\varrho\vdash\textsf{IrReduce}(i_{e},m_{e})\Downarrow^{\mathrm{ir}}\mathrm{sum}(T,\,\mathrm{axis}(m_{e}))}\hskip 9.24994pt\textsc{lab={E-Reduce}}\\ \\ \frac{}{\varrho\vdash\textsf{IrSkip}\Downarrow^{\mathrm{ir}}\varrho}\hskip 9.24994pt\textsc{lab={S-Skip}}\frac{\varrho\vdash i_{e}\Downarrow^{\mathrm{ir}}T}{\varrho\vdash\textsf{IrAssignment}(x,i_{e})\Downarrow^{\mathrm{ir}}\varrho[x\mapsto T]}\hskip 9.24994pt\textsc{lab={S-Assign}}\frac{\varrho\vdash i_{s_{1}}\Downarrow^{\mathrm{ir}}\varrho^{\prime}\hskip 9.24994pt\varrho^{\prime}\vdash i_{s_{2}}\Downarrow^{\mathrm{ir}}\varrho^{\prime\prime}}{\varrho\vdash\textsf{IrSeq}(i_{s_{1}},i_{s_{2}})\Downarrow^{\mathrm{ir}}\varrho^{\prime\prime}}\hskip 9.24994pt\textsc{lab={S-Seq}}\\ \\ \frac{\varrho\vdash i_{e}\Downarrow^{\mathrm{ir}}\mathbf{true}\hskip 9.24994pt\varrho\vdash i_{s}\Downarrow^{\mathrm{ir}}\varrho^{\prime}\hskip 9.24994pt\varrho^{\prime}\vdash\textsf{IrWhile}(i_{e},i_{s})\Downarrow^{\mathrm{ir}}\varrho^{\prime\prime}}{\varrho\vdash\textsf{IrWhile}(i_{e},i_{s})\Downarrow^{\mathrm{ir}}\varrho^{\prime\prime}}\hskip 9.24994pt\textsc{lab={S-While-T}}\frac{\varrho\vdash i_{e}\Downarrow^{\mathrm{ir}}\mathbf{false}}{\varrho\vdash\textsf{IrWhile}(i_{e},i_{s})\Downarrow^{\mathrm{ir}}\varrho}\hskip 9.24994pt\textsc{lab={S-While-F}}

Appendix

Figure 17. IR execution semantics: expression evaluation

\varrho\vdash i_{e}\Downarrow^{\mathrm{ir}}T

(reads

\varrho

) and statement execution

\varrho\vdash i_{s}\Downarrow^{\mathrm{ir}}\varrho^{\prime}

(updates

\varrho

\bar{c}

is the scalar tensor

c

;

\oplus

is applied element-wise; IrITE is analogous to S-While . Nodes not shown evaluate to the like-named backend op on their evaluated arguments.

Panel of Figure 18 — Figure 18. Dense and g-BCSR forms of the Broadcast (Fig. 18a ) and Uniform (Fig. 18b ) blocks. In each pair the left is the dense block and the right is its g-BCSR representation.

Name	Dataset	Model	Training Method	Architecture	Layers	$\epsilon$	Batch
$N_{1}$	MNIST	3x50	Standard	FCN	3	0.004	100
$N_{2}$	MNIST	3x100	Standard	FCN	3	0.004	100
$N_{3}$	MNIST	5x100	DiffAI	FCN	6	0.004	100
$N_{4}$	MNIST	6x100	Standard	FCN	6	0.004	100
$N_{5}$	MNIST	9x100	Standard	FCN	9	0.004	100
$N_{6}$	MNIST	6x200	Standard	FCN	6	0.004	100

Appendix

Table 4. Details of all 32 DNNs used in the evaluation (§ 6 ). Table 2 lists the six representative networks.

Figure 19. Per-network precision–runtime design space, networks N1–N16. For each certifier, the green bar is its precision (left axis) and the blue marker is its runtime (right axis; log scale, shared with Fig. 20 ).

Figure 20. Per-network precision–runtime design space, networks N17–N32 (continued from Fig. 19 , same axes).

Figure 21.

\mathit{DeepPoly}_{p}

on networks N1–N16: precision (green) and runtime (blue, log) as backsubstitution depth

p

increases; the red dashed line marks the smallest

p

at which precision saturates. Continued in Fig. 22 .

Figure 22.

\mathit{DeepPoly}_{p}

on networks N17–N32 (continued from Fig. 21 ).

Certifier	Baseline	Mean	GeoMean	Median	$n$
IBP	auto_LiRPA	3.0	1.6	1.0	32
	IVAN	2.7	1.1	0.60	31
DeepZ	IVAN	1.3	0.96	1.0	31
	ERAN	25	17	16	17
DeepPoly	auto_LiRPA	0.73	0.58	0.63	32
	IVAN	7.5	3.5	3.4	24

Appendix

Table 5. Aggregate speedup of Neuton over each baseline (speedup

=

baseline

/

Neuton runtime;

{>}1

means Neuton is faster), summarising Table 6 . Each row aggregates over the

n

DNNs on which both Neuton and the baseline finished within the

200

s timeout. Table 6 gives the underlying per-DNN times.

	IBP				DeepZ				DeepPoly				CROWN-IBP
Network	n	aL	IV	ER	n	aL	IV	ER	n	aL	IV	ER	n	aL	IV	ER
$N_{1}$	0.04	0.04	0.03	–	0.16	–	0.19	6.45	0.45	0.12	0.41	3.73	0.17	0.10	–	–
$N_{2}$	0.04	0.04	0.03	–	0.23	–	0.23	13.3	0.60	0.18	0.65	8.05	0.17	0.10	–	–
$N_{3}$	0.09	0.05	0.03	–	0.60	–	0.41	30.7	1.61	0.38	1.32	27.3	0.39	0.11	–	–
$N_{4}$	0.08	0.05	0.03	–	0.59	–	0.33	28.3	2.00	0.37	1.29	13.3	0.39	0.11	–	–
$N_{5}$	0.13	0.06	0.03	–	1.18	–	0.47	38.7	3.58	0.91	2.07	21.3	0.68	0.13	–	–

Appendix

Table 6. Per-DNN runtime (seconds) with the four baseline-supported certifiers placed side by side, so Neuton and the baselines can be compared across certifiers on each DNN. Tool codes: n

=

Neuton , aL

=

auto_LiRPA, IV

=

IVAN, ER

=

ERAN. Each certifier lists all four tools; for each certifier, the fastest tool on each DNN is shown in bold . TO

=

exceeded the

200

s threshold; –

=

the baseline does not implement that certifier (or errored). The final row is the per-column geometric mean over runs completed within the threshold. Aggregate speedups are in Table 5 .

Certifier	Variant	Mean	GeoMean	Median	$n$	fail
IBP	N $-$ S	49	24	24	28	4
	N $-$ R	51	8.0	3.3	32	0
	N $-$ R $-$ S	55	25	26	28	4
CROWN-IBP	N $-$ S	10	5.7	6.2	28	4
	N $-$ R	25	6.9	4.1	29	3
	N $-$ R $-$ S	20	8.7	8.8	28	4

Appendix

Table 7. Ablation slowdown of each variant relative to full Neuton (slowdown

=

variant

/

Neuton runtime;

{>}1

means the disabled optimization was helping). Variants: N

-

S removes g-BCSR, N

-

R removes rewrites, N

-

-

S removes both. Each row aggregates over the

n

DNNs the variant completed; fail counts DNNs where the variant crashed, ran out of memory, or timed out but full Neuton succeeded. Table 8 and Table 9 give the per-DNN times.

	IBP				CROWN-IBP				DeepZ				DeepPoly
Network	n	$-$ S	$-$ R	$-$ RS	n	$-$ S	$-$ R	$-$ RS	n	$-$ S	$-$ R	$-$ RS	n	$-$ S	$-$ R	$-$ RS
$N_{1}$	0.03	0.09	0.04	0.08	0.19	0.26	0.21	0.23	0.07	0.12	0.10	0.12	0.33	0.44	0.42	0.44
$N_{2}$	0.03	0.10	0.04	0.10	0.19	0.27	0.24	0.27	0.07	0.13	0.10	0.14	0.32	0.46	0.80	0.79
$N_{3}$	0.05	0.19	0.08	0.17	0.47	0.50	0.66	0.60	0.25	0.32	0.31	0.34	1.27	1.55	3.52	3.29
$N_{4}$	0.06	0.16	0.08	0.17	0.58	0.60	0.65	0.60	0.24	0.31	0.33	0.34	1.17	1.54	3.52	3.28
$N_{5}$	0.09	0.27	0.15	0.27	0.84	0.83	1.49	1.16	0.58	0.75	0.79	0.76	2.97	3.18	8.21	6.95

Appendix

Table 8. Per-DNN ablation runtime (seconds, batch size 10) for IBP, CROWN-IBP, DeepZ, DeepPoly, with Neuton and its ablated variants side by side. Variant codes relative to full Neuton ( n ):

-

S removes g-BCSR,

-

R removes rewrites,

-

RS removes both. For each certifier, the fastest variant on each DNN is shown in bold . TO

=

exceeded the

200

s threshold; ✗

=

crashed or ran out of memory; –

=

no data. The final row is the per-column geometric mean over runs completed within the threshold. Remaining certifiers are in Table 9 ; aggregate slowdowns in Table 7 .

	ReuseCert				PolyZono				ZID				SkipPoly
Network	n	$-$ S	$-$ R	$-$ RS	n	$-$ S	$-$ R	$-$ RS	n	$-$ S	$-$ R	$-$ RS	n	$-$ S	$-$ R	$-$ RS
$N_{1}$	0.17	0.25	0.36	0.38	0.50	0.46	0.52	0.49	0.21	0.26	0.23	0.24	0.27	0.33	0.34	0.34
$N_{2}$	0.18	0.26	0.65	1.01	0.50	0.59	0.91	0.86	0.20	0.28	0.27	0.29	0.28	0.36	0.67	0.75
$N_{3}$	0.45	0.58	2.35	2.35	1.82	1.86	3.76	3.42	0.50	0.58	0.67	0.60	0.93	1.07	3.00	2.87
$N_{4}$	0.45	0.57	2.38	2.36	1.93	1.43	3.84	3.49	0.49	0.53	0.70	0.61	0.79	1.02	2.95	2.88
$N_{5}$	0.93	1.43	4.10	4.05	3.68	4.33	9.12	7.79	0.85	1.03	1.49	1.15	1.87	1.84	6.60	6.06

Appendix

Table 9. Per-DNN ablation runtime (seconds, batch size 10) for ReuseCert, PolyZono, ZID, SkipPoly, with Neuton and its ablated variants side by side. Variant codes relative to full Neuton ( n ):

-

S removes g-BCSR,

-

R removes rewrites,

-

RS removes both. For each certifier, the fastest variant on each DNN is shown in bold . TO

=

exceeded the

200

s threshold; ✗

=

crashed or ran out of memory; –

=

no data. The final row is the per-column geometric mean over runs completed within the threshold. Remaining certifiers are in Table 8 ; aggregate slowdowns in Table 7 .

Figure 23. Per-DNN peak memory of Neuton vs. existing libraries on all 32 DNNs (

=

auto_LiRPA,

=

IVAN; log–log axes). A point below the dashed diagonal means Neuton uses less memory on that DNN. x markers denote DNNs on which the baseline exceeded the

200

s timeout while Neuton finished.

Baseline	IBP	CROWN-IBP	DeepZ	DeepPoly
auto_LiRPA	$0.98\times$	$0.95\times$	–	$1.14\times$
IVAN	$0.94\times$	–	$1.64\times$	$2.26\times$ (4 TO)
ERAN ( $b{=}1$ )	–	–	$2.05\times$	$2.13\times$

Appendix

Table 10. Peak memory of hand-optimized libraries relative to Neuton on all 32 DNNs (geometric mean of baseline / Neuton over the DNNs both complete;

>1

means Neuton uses less memory). ERAN is measured at batch size

1

on the six representative DNNs. TO

=

DNNs on which the baseline timed out.

Variant	IBP	CROWN-IBP	DeepZ	DeepPoly	ReuseCert	PolyZono	ZID	SkipPoly	Overall
N–S	$18.1\times$ (1)	$17.3\times$ (1)	$6.3\times$ (1)	$6.7\times$ (1)	$6.8\times$ (1)	$4.8\times$ (1)	$11.5\times$ (1)	$5.8\times$ (1)	$8.6\times$ (8)
N–R	$3.4\times$	$9.5\times$	$1.3\times$	$46.7\times$ (3)	$129.8\times$ (2)	$31.5\times$ (3)	$6.3\times$	$71.3\times$ (2)	$11.1\times$ (10)
N–R–S	$18.1\times$ (1)	$17.8\times$ (1)	$6.3\times$ (1)	$75.5\times$ (2)	$134.8\times$ (2)	$53.5\times$ (2)	$11.9\times$ (1)	$75.9\times$ (2)	$28.5\times$ (12)

Appendix

Table 11. Peak memory of each ablated variant relative to Neuton on the six representative DNNs (geometric mean over the DNNs on which the variant completes). Parentheses count the DNNs on which the variant ran out of memory while Neuton completed.

Neural Network Verification

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

See all 125 papers

Mar 25, 2026

The Luna Bound Propagator for Formal Analysis of Neural Networks

The parameterized CROWN analysis, a.k.a., alpha-CROWN has emerged as a practically successful abstract interpretation method for neural network verification. However, existing implementations of alpha-CROWN are limited to Python, which complicates integration into existing DNN verifiers and long-term production-level systems. We introduce Luna, a new abstract-interpretation-based bound propagator implemented in C++. Luna supports Interval Bound Propagation, the DeepPoly/CROWN analysis, and the alpha-CROWN analysis over a general computational graph. We describe the architecture of Luna and show that it outperforms the state-of-the-art alpha-CROWN implementation in terms of both bound tightness and computational efficiency on supported benchmarks from VNN-COMP 2025. Luna is publicly available at https://github.com/ai-ar-research/luna.

Henry LeCates, Haoze Wu

Amherst College, USA

Abstract Interpretation Neural Network Verification Neural Network Robustness

Ask PDF

Feb 26, 2026

TorchLean: Formalizing Neural Networks in Lean

Neural networks are increasingly deployed in scientific, safety critical, and mission critical pipelines, yet verification and analysis are often performed outside the programming environment that defines and runs the model. This creates a semantic gap between the executed network and the analyzed artifact: guarantees can depend on implicit conventions about operator semantics, tensor layouts, preprocessing, floating-point behavior, graph transformations, accelerated kernels, and external certificates. We present TorchLean, a unified framework for formalizing, executing, and verifying neural networks in Lean 4. TorchLean treats learned models as executable programs and mathematical objects with a shared semantics for computation, verification, and theorem proving. The framework provides a PyTorch style API for typed tensors, layers, objectives, optimizers, automatic differentiation, and graph programs, with eager and compiled execution paths that lower to a common computation-graph representation. TorchLean supports exact and finite-precision tensor semantics, verified reverse-mode differentiation, interval and affine bound propagation, CROWN/LiRPA style certificate checking, import/export workflows, and CUDA-backed execution through explicit FFI boundaries. It also includes semantic layers for attention and FlashAttention, state-space sequence models, diffusion and sampling processes, probability kernels, reinforcement-learning objectives and Markov decision processes, and self-supervised objectives such as masked autoencoding, JEPA-style predictive views, and variance/correlation-based anti-collapse losses. Together, these components provide a semantic foundation for verified machine learning, where executable neural network artifacts, verification procedures, runtime boundaries, and mathematical claims can be stated and related inside one theorem-proving environment.

Robert Joseph George, Jennifer Cruden, Will Adkisson +3

California Institute of Technology · Washington University in St. Louis · University of Illinois Urbana-Champaign

Neural Network Verification

Ask PDF

Aug 25, 2026

$(\text{DNN})^2$ : Doubly Non-Negative Relaxations for Deep Neural Networks

Existing linear program (LP) and semidefinite program (SDP) relaxations for rectified linear unit (ReLU) neural network (NN) verification yield overly-conservative safety guarantees due to significant relaxation gaps. While the completely positive program (CPP) formulation closes this gap, it is NP-hard to solve. Its cheapest tractable relaxation, the doubly non-negative program (DNN), retains critical constraints as an SDP, but one whose size exceeds the reach of interior-point methods at practical scale. While Burer-Monteiro (BM) factorization has been applied to make SDP-based verification scalable, no such result exists for the strictly tighter DNN formulation. A key obstacle is that additional non-negativity constraints in the DNN cause dual multipliers for optimality certification to be non-unique, making standard certification methods inapplicable. We propose a novel eigenvalue maximization procedure that searches the non-unique multiplier space for a valid certificate, i.e. a global optimality guarantee. Experiments demonstrate that our approach

(\text{DNN})^2

produces bounds consistently tighter than the standard SDP method, often matching the exact solution, and that our certification procedure confirms global optimality when a valid certificate exists. These results are a key step toward providing tight, certifiable, and computationally scalable verification guarantees needed to deploy neural network controllers and perception modules in safety-critical autonomous systems.

Hanna Jiamei Zhang, Alan Papalia, Michael Everett +1

Departments of Computer Science, Electrical and Computer Engineering, and Mathematics Northeastern University, Boston, MA. · Department of Naval Architecture and Marine Engineering, University of Michigan, Ann Arbor, MI.

Neural Network Verification ReLU Neural Networks Semidefinite Programming Nonconvex Optimization

Ask PDF

Abstract

Neural Network Verification

Explore similar work

The Luna Bound Propagator for Formal Analysis of Neural Networks

TorchLean: Formalizing Neural Networks in Lean

(DNN)2(\text{DNN})^2(DNN)2: Doubly Non-Negative Relaxations for Deep Neural Networks

$(\text{DNN})^2$ : Doubly Non-Negative Relaxations for Deep Neural Networks