Scalable and Interpretable Verification of Image-based Neural Network Controllers for Autonomous Vehicles

Aditya Parameshwaran; Yue Wang

REVIEW 5 major objections 5 minor 41 references

Scalable and Interpretable Verification of Image-based Neural Network Controllers for Autonomous Vehicles

T0 review · 5 major / 5 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read SEVIN verifies image-based neural network controllers by checking low-dimensional latent polytopes instead of raw images, reducing formal verification to sub-second runs.

desk verdict A clean engineering recipe whose formal-verification claim doesn't survive contact with the decoder's nonlinearity. read the letter →

arxiv 2501.14009 v2 pith:TZE552DC submitted 2025-01-23 cs.LG cs.AIcs.SYeess.SY

Aditya Parameshwaran , Yue Wang This is my paper · ORCID

classification cs.LGcs.AIcs.SYeess.SY

keywords formalverificationneuralnetworkcontrollervariationalautoencoderlatentspaceconvexpolytopeautonomousvehiclesrobustnessinterpretability

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

SEVIN aims to make formal verification of image-based neural network controllers tractable by moving the verification problem out of pixel space. A variational autoencoder compresses front-camera images into a low-dimensional latent space, where points are labeled by the vehicle's steering action and grouped into convex polytopes. The decoder and the controller are composed into one network $H(z)=F(D(z))$, so properties can be checked over latent polytopes instead of over raw images. The paper claims that finding the minimum of $F$ over the decoded image region is equivalent to finding the minimum of $H$ over the latent polytope, which is what licenses the much cheaper verification. If the equivalence holds, image controller verification drops to well under a second while also yielding human-readable regions tied to actions.

What carries the argument

The load-bearing objects are a Gaussian-mixture variational autoencoder whose 8-dimensional latent space clusters images by steering action, convex polytopes $C_i = \operatorname{conv}\{z_j : z_j=E(x_j), x_j\in X_i\}$ enlarged by a Minkowski sum to tolerate edge cases, and the composed network $H(z)=F(D(z))$, which is piecewise linear because both $F$ and $D$ use ReLU activations. The mechanism is Theorem 1, which asserts that optimizing $F$ over the image region $D(C_i)$ reduces to optimizing $H$ over $C_i$, so a bound-propagation verifier only needs to solve a low-dimensional optimization problem. Interpretability enters because each polytope is paired with an action set $A_i$, making a SAT result read as "all latent inputs in this turn region produce turn actions in the specified range."

What would settle it

Compute the actual maximum of $\|F(D(z))-F(x)\|_2$ over each enlarged latent polytope and check the controller output $F(D(z))$ against the action-set bounds $A_i$ for sampled $z$ inside the polytope; if a single decoded image inside a claimed region produces an action outside $A_i$, the Lemma 2 premise is false and the verification result does not transfer to $F$ on real images.

Watch

Extended reading notes

Core claim

The central claim is Theorem 1: for a ReLU controller $F$ and ReLU decoder $D$, with $C_i$ a convex polytope constructed as the convex hull of latent samples from one action class, $\min_{x\in D(C_i)} F(x) \equiv \min_{z\in C_i} H(z)$. The paper states that verifying the composed network $H$ over the low-dimensional latent polytope therefore constitutes formal verification of the image-based controller $F$ over the corresponding decoded images. The framework treats this as a route to scalability: the input dimension drops from an $80\times 64$ image to an 8-dimensional latent variable, and the same polytopes double as interpretable specifications because each polytope is labeled by the action it should produce.

Load-bearing premise

The central premise is that every latent point inside a polytope built from one action class decodes to an image whose controller output stays in that same action class, and that reconstruction error changes controller outputs by less than a small epsilon; the paper assumes this rather than measures it.

Editorial extensions

If this is right

Verification time for the tested controllers drops to under a second per specification, with the paper reporting roughly 0.3 to 0.9 seconds for vanilla and robustness checks.
The same framework covers robustness: by retraining the VAE on brightness- and motion-blur-augmented datasets, the polytopes shift and the verifier certifies or refutes the same safety and performance specifications over perturbed input classes.
SEVIN exposes architecture differences, since the paper reports one controller failing a performance specification under augmentation while the other passes until the strongest perturbation level, suggesting verifiable screening of controller architectures.
Because the input dimension is roughly 600 times smaller than pixel space, the approach scales to larger controllers without abandoning formal guarantees, at the cost of a deeper composed network $H$.
The safety and performance specifications, expressed in the VNN-LIB format, provide reusable and human-readable contracts linking latent regions to permitted control actions.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Editorial extension: the core equivalence is directly testable by sampling latent points inside each $C_i$, decoding them, and comparing $F(\hat{x})$ with the action bounds $A_i$; the paper never reports this measurement, so a reader cannot yet tell how often Lemma 2's premise holds.
Editorial extension: if the equivalence holds only approximately in practice, the framework still yields a useful screening tool: polytopes could be iteratively shrunk or the decoder fine-tuned until action-class mismatches vanish.
Editorial extension: the same latent-polytope recipe could be extended to temporal specifications, checking whether a trajectory of latent points stays inside safe polytopes, which would connect this static verification to reachability analysis.
Editorial extension: the sub-second robustness checks suggest a design loop where several decoder-controller pairs are compared across augmentation levels, and a failing specification becomes a targeted signal for retraining.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Short version: this is a plausible engineering framework that is not, as written, a formal verification method. The core reduction from image-space verification to latent-space verification is a tautology on the decoder's output set; the missing bridge to real camera images is assumed (Assumption 1) and not measured, and Lemma 2's convexity argument would be wrong even if measured.

What's genuinely here: the paper takes the known idea of generative-model verification (Katz et al.) and makes a workable pipeline: train a GM-VAE, label latent codes by control action, compute convex polytopes, compose decoder with controller, and run alpha-beta-CROWN on the composite. The action-labeled polytope construction is transparent, and the timing comparison (sub-second verification vs. ~4s for the general method) is a real, reproducible data point. The writing is clear and the experimental setup is simple enough to follow.

Where it falls apart: Theorem 1 only equates min over D(C_i) of F with min over C_i of F∘D. That is true by definition, but the paper then claims this verifies F over X_i, the original image subset. There is no argument that X_i ⊆ D(C_i) and no error bound that covers the convex hull points. Assumption 1 is stated but never measured; even if it held pointwise on training encodings, it doesn't extend to arbitrary convex combinations. Lemma 2's proof asserts that because each sampled z_j has an action in A_i and A_i is continuous, any convex combination in latent space decodes to an image with an action in A_i. That is exactly the kind of leap that fails for nonlinear decoders: D(∑λ_j z_j) ≠ ∑λ_j D(z_j), and action membership is not affine.

I also flag the SAT/UNSAT labeling. Their Section 2.3 defines SAT as 'specification satisfied,' but standard SMT-based verification semantics use 'unsat' for that. If alpha-beta-CROWN follows VNN-COMP convention, their reported SAT/UNSAT columns may be inverted, which would flip the robustness conclusions. That needs a careful check before anything is built on these tables.

Net: the paper is a useful engineering heuristic, and the experiments show the runtime benefits clearly. But as a formal verification contribution it does not hold as stated. A heavy revision that replaces Assumption 1 with a measured, verified reconstruction bound (or with a validated upper bound on D(C_i) error) and that either proves or clearly drops Lemma 2 would be worth another look. I would not cite it as a verification result, but I would point students to it as an example of how to set up latent-space verification, with the caveats above.

Recommendation: send it to peer review — the topic is timely, the framework is presented honestly, and the flaws are the kind a good referee can catch and potentially help fix. But the verdict should be reject unless the formal gap is closed.

Referee Report

5 major / 5 minor

Summary. The paper proposes SEVIN, a framework for formal verification of image-based neural network controllers. SEVIN trains a Gaussian-mixture VAE on image-action pairs, encodes images into a low-dimensional latent space, labels the latent codes by control actions, and constructs convex polytopes C_i as convex hulls of sampled latent codes belonging to each action set, optionally enlarged by a Minkowski sum. The decoder D is then concatenated with the controller F to form the composite network H = F∘D, and the α-β-CROWN verifier is used to check safety and performance specifications over the polytopes. The paper claims that verifying H over C_i is equivalent to formally verifying F over the original image input space, and reports runtime results for two controller architectures (NvidiaNet and ResNet18) on CARLA data with brightness and motion-blur augmentations.

Significance. If the central equivalence were valid, the work would be a significant practical contribution: latent-space abstraction could reduce verification cost substantially and provide human-interpretable input regions. The paper also has strengths: it uses a standard complete verifier, reports a concrete runtime comparison on image-based controllers, and the experimental setup with multiple augmentation levels is reasonable. However, the transfer argument is not established: Theorem 1 is a definitional identity over the decoder's image, Lemma 2's convexity argument is invalid for nonlinear decoders, Assumption 1 is unmeasured and does not cover the polytope interior, and the SAT/UNSAT convention appears reversed relative to VNN-COMP, which would invert the reported verification outcomes. These issues undermine the paper's central claim as submitted.

major comments (5)

[Section 4.4, Theorem 1] Theorem 1 states that minimizing F(x) over x in D(C_i) is equivalent to minimizing H(z) over z in C_i, which is true by substitution: H(z) = F(D(z)). The paper then concludes that verifying H over C_i is equivalent to verifying F over the original image subset X_i. This conclusion does not follow: no argument shows that X_i is contained in D(C_i), nor that D(C_i) consists of images whose control actions lie in A_i. Since D is a nonlinear transposed-convolution network, D(C_i) is not the original front-camera input set; the verification performed is of the surrogate H on reconstructed images, not of F on real images.
[Section 4.3, Lemma 2] The proof of Lemma 2 argues that because each sampled latent code z_j is paired with an action in A_i and A_i is a continuous action set, any convex combination z = sum λ_j z_j decodes to an image with an action in A_i. This is invalid: D is a ReLU/transposed-convolution network, so D(sum λ_j z_j) is not equal to sum λ_j D(z_j), and action-label membership is not an affine function of the latent code. Convexity of A_i does not imply that the preimage of A_i under the nonlinear map z ↦ F(D(z)) is convex. Without Lemma 2, the correspondence between C_i and A_i used throughout Sections 4.4–4.6 is unsupported.
[Section 4.1, Assumption 1] Assumption 1 postulates that ||F(D(E(x))) - F(x)||_2 ≤ ε and states the target ε ≈ ||F(x)||/100, but no experiment in Section 5 reports a measured value of ε or a procedure for measuring it. Moreover, the assumption, even if measured, applies only to reconstructions D(E(x)) of the finite set of training or validation images; it does not bound the error for arbitrary z in the convex hull C_i or in its Minkowski enlargement, which is the actual input set of H. A pointwise bound on encoded samples cannot be extended to the polytope without additional Lipschitz or uniform-convergence analysis.
[Section 2.3 and Tables 1, 3] The paper defines 'SAT' as the specification being satisfied and 'UNSAT' as unsatisfied. In VNN-COMP/VNN-LIB usage, the solver query is for a counterexample: SAT means a violation exists, and UNSAT means the property is verified. Table 3 reports all results as SAT, and Section 5.3.3 concludes that the controllers satisfy all specifications; under the standard convention these entries would mean the properties were violated. This inversion affects the reported safety conclusions and the interpretation of the comparison in Table 4.
[Section 4.3, Eq. (10)] The convex polytope C_i is constructed as the convex hull of encoded images whose controller outputs already lie in A_i. The property z ∈ C_i ⇒ H(z) ∈ A_i is then satisfied at the vertices by construction, and verifying the hull and Minkowski enlargement checks the composite on a region defined by the same action labels. This does not constitute an independent safety guarantee for the controller on real camera inputs unless an explicit relation between latent-space neighborhoods and image-space perturbations is established, which the paper does not provide.

minor comments (5)

[Section 4.2, Lemma 1] The proof of Lemma 1 states that p(z ∈ Z_a) > 0 for the set Z_a of encoded points associated with action a, but a finite set of points has measure zero under a continuous Gaussian-mixture prior; the argument requires positive-measure neighborhoods around those points or a different sampling formulation.
[Section 4.4, Theorem 1 statement] The theorem statement says 'finding the local minimum of F(x) over x ∈ D(z)' where D(z) is a single point; the intended set is D(C_i). The same notation issue appears in the paragraph before the statement.
[Section 5.2] The encoder description is unclear: it says the encoder 'begins with a linear layer, followed by three convolutional layers with increasing channel sizes: from 1 to 64, then 128, 256, and finally 512 channels,' but four channel sizes are listed. The decoder and controller architectures are not described, which hinders reproducibility.
[Table 1] Some cells contain 'UNSAT -' with no runtime; the meaning of '-' should be clarified. The table would also benefit from reporting verifier settings such as timeout or bound-propagation splits.
[Section 5.3.5] The comparison with general robustness verification uses the same specification formulas but different input sets (pixel-bounded boxes for the general method versus latent polytopes for SEVIN); the statement that 'all specifications are SAT for both methods' is therefore not a like-for-like comparison of the verified properties.

Circularity Check

3 steps flagged · score 6.0 of 10

SEVIN's central equivalence is definitional: Theorem 1 only relates F on D(C_i) to H on C_i, while the transfer to real camera images rests on an unmeasured reconstruction bound and a Lemma 2 that assumes label-convexity in latent space.

self definitional [Section 3 and Section 4.4, Theorem 1 with its concluding paragraph]
"The combined network H(z) = F(D(z)) maps variables directly from the latent space to control actions. ... The equivalence between verifying F(x) and H(z) is established in Theorem 1. Theorem 1. ... Formally, min_{x∈D(C_i)} F(x) ≡ min_{z∈C_i} H(z) ... Consequently, Theorem 1 demonstrates that minimizing F(x) over x∈X_i is equivalent to minimizing H(z) over z∈C_i."

Since H is defined as F∘D, the displayed equivalence min over z∈C_i of H(z) equals min over x∈D(C_i) of F(x) holds by the definition of the image set D(C_i); no property of the controller is derived from it. The load-bearing claim is the final sentence, which silently replaces D(C_i) with X_i. That replacement is not supplied by the theorem; it needs Lemma 2 and Assumption 1. The claimed equivalence between verifying F on real images and verifying H on C_i therefore reduces to a change of variables plus an unproven identification of D(C_i) with the original input set.
fitted input called prediction [Section 4.3, Equation (10) and Section 4.4, Equation (12)]
"C_i = conv({z_j | z_j = E(x_j), x_j∈X_i, j=1,...,n}) ... X_i = {x∈X | F(x)∈A_i} ... the verification process thus for the combined network H(z) can be formalized as: z∈C_i =⇒ H(z)∈A_i"

The input polytope is the convex hull of encoded images selected by the condition F(x)∈A_i, and the verified property is that outputs over that polytope remain in the same A_i. At the vertices, H(z_j)=F(D(E(x_j))) is close to F(x_j)∈A_i only under the unmeasured Assumption 1, and the extension to the hull is asserted by Lemma 2. Thus the specification is the same label set used to define the input region, and verifying H over C_i is an interpolation of training labels rather than an independent statement about arbitrary front-camera inputs.

1 more flagged steps

other [Section 4.3, Lemma 2 and its proof]
"The decoder D(z) is assumed to be a continuous function mapping latent variables to high-dimensional images. ... Specifically, since each latent variable z_j corresponds to an action a_j∈A_i, and A_i is a continuous action set, the convex combination ensures that xhat is associated with an action a∈A_i."

This lemma is the bridge that makes C_i action-consistent, and its proof assumes the conclusion. Continuity of D does not imply that action labels are preserved under convex combinations: D is a nonlinear stack of transposed convolutions, ReLU, and sigmoid, so D(Σλ_j z_j) is not Σλ_j D(z_j) in general, and membership of the decoded image in A_i is not an affine function of z. The lemma asserts exactly the label-convexity property that verification of H over C_i is supposed to establish, so it cannot transfer a bound on the latent hull to a guarantee about real images.

full rationale

No self-citation chain is load-bearing here; the circularity is in the theoretical reduction, not in the references. Theorem 1's displayed equivalence is definitional because H is F∘D, and the concluding sentence silently replaces D(C_i) by X_i. The stated bridges do not close the gap: Section 4.1's Assumption 1 postulates ||F(V(x))−F(x)||_2 ≤ ε with a target of about ||F(x)||_2/100, but the paper never measures ε and the assumption concerns encoded training samples, not arbitrary z∈C_i; Lemma 2's proof derives label preservation under convex combinations from continuity of D and of A_i, which is invalid for a nonlinear decoder. Because C_i is generated from images that already satisfy F(x)∈A_i, the verified property over C_i is an interpolation of the labels used to construct C_i, so the tables certify H on latent hulls rather than F on the original image set X_i. The experiments are genuine computations and contain UNSAT cases, so the evaluation is not vacuous, and the scalability comparison has independent content; however, the paper's own derivation that these results formally verify the image-based controller is circular at the equivalence step and unsupported at the transfer step. Score 6: partial circularity.

Assumptions & free parameters 8 free parameters · 4 assumptions · 0 invented entities

The central claim rests on unverified assumptions about VAE fidelity and latent geometry, plus a questionable interpretation of the verifier's output.

free parameters (8)

Latent dimension d_z = 8
Chosen by the authors to compress 80x64 images; not justified by a trade-off study.
Number of Gaussian components K = 16
Chosen to enhance expressiveness, no ablation.
VAE loss beta = 0.01
Hyperparameter balancing reconstruction and KL divergence, chosen without sensitivity analysis.
Minkowski sum radius epsilon = 0.05 in Example 2, unspecified for experiments
Used to enlarge polytopes; no procedure for setting it.
Monte Carlo sample count n for polytope construction = not stated
Number of latent samples per polytope not reported.
Two-standard-deviation sampling threshold = 2
Chosen to define the sample region; arbitrary.
Reconstruction error bound eps in Assumption 1 = target 1/100 ||F(x)||, not measured
The paper aims for this but provides no measurement.
Augmentation levels delta1, delta2, delta3 = brightness 80-120%, 60-140%, 50-150%; blur kernels 1-2, 3-4, 5-6
Chosen perturbation magnitudes, no justification.

assumptions (4)

ad hoc to paper Assumption 1: ||F(hat x) - F(x)||_2 <= eps for VAE reconstructions
Load-bearing for the transfer of verification results from latent space to real images; unverified.
ad hoc to paper Lemma 2: decoding any convex combination of latent samples from action set A_i yields an image in A_i
Assumes action labels are preserved under convex combinations in latent space, not true for nonlinear decoders.
domain assumption The latent space is structured so each action set corresponds to a convex region
The polytope construction presupposes that action classes are separable by convex hulls in the VAE latent space.
domain assumption alpha-beta-CROWN output semantics: SAT means the specification holds
The paper interprets SAT as property satisfied; this is opposite to the usual VNN-COMP convention where UNSAT means the property is verified.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Scalable and Interpretable Verification of Image-based Neural Network Controllers for Autonomous Vehicles." pith.science (2026). https://pith.science/paper/TZE552DC

@misc{pith2026250114009,
  author       = {Pith},
  title        = {Pith review of: Scalable and Interpretable Verification of Image-based Neural Network Controllers for Autonomous Vehicles},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/TZE552DC}},
  note         = {Machine review of arXiv:2501.14009}
}

read the original abstract

Existing formal verification methods for image-based neural network controllers in autonomous vehicles often struggle with high-dimensional inputs, computational inefficiency, and a lack of explainability. These challenges make it difficult to ensure safety and reliability, as processing high-dimensional image data is computationally intensive and neural networks are typically treated as black boxes. To address these issues, we propose SEVIN (Scalable and Explainable Verification of Image-Based Neural Network Controllers), a framework that leverages a Variational Autoencoders (VAE) to encode high-dimensional images into a lower-dimensional, explainable latent space. By annotating latent variables with corresponding control actions, we generate convex polytopes that serve as structured input spaces for verification, significantly reducing computational complexity and enhancing scalability. Integrating the VAE's decoder with the neural network controller allows for formal and robustness verification using these explainable polytopes. Our approach also incorporates robustness verification under real-world perturbations by augmenting the dataset and retraining the VAE to capture environmental variations. Experimental results demonstrate that SEVIN achieves efficient and scalable verification while providing explainable insights into controller behavior, bridging the gap between formal verification techniques and practical applications in safety-critical systems.

Figures

Figures reproduced from arXiv: 2501.14009 by the authors.

**Figure 1.** The SEVIN model can be decomposed into two sub-modules for conducting formal verification of any neural network [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗

**Figure 2.** t-SNE plot of an 8D latent space representation [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗

**Figure 3.** 2D latent space representation of the front camera [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗

Figures from the paper (2 more)

**Figure 4.** Figure 4: Illustration of the data pre-processing, augmen [PITH_FULL_IMAGE:figures/full_fig_p008_4.png]

**Figure 5.** Figure 5: t-SNE plot of an 8D latent space representation [PITH_FULL_IMAGE:figures/full_fig_p008_5.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

41 extracted references · 25 canonical work pages

[1]

Takumi Akazaki and Yang Liu. 2018. Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning. In International Symposium on Formal Methods. Springer, 456–465

work page 2018
[2]

Mohammed Al-Nuaimi, Sapto Wibowo, Hongyang Qu, Jonathan Aitken, and Sandor Veres. 2021. Hybrid Verification Technique for Decision-Making of Self-Driving Vehicles. Journal of Sensor and Actuator Networks 10, 3 (2021), 42. https://doi.org/10.3390/jsan10030042

work page doi:10.3390/jsan10030042 2021
[3]

C Bradford Barber, David P Dobkin, and Hannu Huhdanpaa. 1996. The Quickhull Algorithm for Convex Hulls. ACM Transactions on Mathematical Software (TOMS) (1996)

work page 1996
[4]

Michael M Bronstein, Joan Bruna, Yann LeCun, Arthur Szlam, and Pierre Van- dergheynst. 2017. Geometric Deep Learning: Going Beyond Euclidean Data. IEEE Signal Processing Magazine (2017)

work page 2017
[5]

Rudy Bunel, Isil Dillig Turkaslan, and Philip HS Torr. 2018. A Unified View of Piecewise Linear Neural Network Verification. Advances in Neural Information Processing Systems (2018)

work page 2018
[6]

Anna Choromanska, Mikael Henaff, Michael Mathieu, Gerard Ben Arous, and Yann LeCun. 2015. The Loss Surfaces of Multilayer Networks. Proceedings of the Eighteenth International Conference on Artificial Intelligence and Statistics (2015)

work page 2015
[7]

Frank H Clarke. 1998. Nonsmooth Analysis and Control Theory . Springer

work page 1998
[8]

Nat Dilokthanakul, Pedro AM Mediano, Marta Garnelo, Matthew CH Lee, Hugh Salimbeni, Kai Arulkumaran, and Murray Shanahan. 2016. Deep Unsupervised Clustering with Gaussian Mixture Variational Autoencoders. arXiv preprint arXiv:1611.02648 (2016)

arXiv 2016

Show all 41 references

[9]

Rüdiger Ehlers. 2017. Formal Verification of Piecewise Linear Feed-Forward Neural Networks. arXiv preprint arXiv:1705.01320 (2017)

2017 arXiv
[10]

Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, and Mar- tin Vechev. 2018. AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. 2018 IEEE Symposium on Security and Privacy (SP) (2018)

2018
[11]

Branko Grünbaum. 2003. Convex Polytopes. Vol. 221. Springer Science & Business Media

2003
[12]

Dario Guidotti, Stefano Demarchi, Armando Tacchella, and Luca Pulina. 2023. The Verification of Neural Networks Library (VNN-LIB). https://www.vnnlib.org Accessed: 2023

2023
[13]

Irina Higgins, Loic Matthey, Arka Pal, Christopher Burgess, Alexander Glorot- Xavier, and Matthew Botvinick. 2017. beta-VAE: Learning Basic Visual Concepts with a Constrained Variational Framework. International Conference on Learning Representations (2017)

2017
[14]

Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. 2017. Safety Verification of Deep Neural Networks. arXiv preprint arXiv:1610.06940 (2017)

2017 arXiv
[15]

Julian, Ritchie Lee, and Mykel J

Kyle D. Julian, Ritchie Lee, and Mykel J. Kochenderfer. 2020. Validation of Image-Based Neural Network Controllers through Adaptive Stress Testing. IEEE Transactions on Intelligent Transportation Systems 22, 5 (2020), 2862–2871. https: //doi.org/10.1109/TITS.2020.2988147

2020
[16]

Eli Kaiser, Saif Ahmed, and Tommaso Dreossi. 2021. SMT-Based Verification of Neural Network Controllers for Autonomous Systems. IEEE Transactions on Cybernetics (2021)

2021
[18]

Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer
[19]

Katz, Anthony L

Sydney M. Katz, Anthony L. Corso, Christopher A. Strong, and Mykel J. Kochen- derfer. 2021. Verification of Image-based Neural Network Controllers Using Generative Models. IEEE Transactions on Neural Networks and Learning Systems 33, 7 (2021), 3106–3120. https://doi.org/10.110...

2021
[20]

arXiv preprint arXiv:1702.01135 (2017)

Towards Scalable Verification for All Neural Networks. arXiv preprint arXiv:1702.01135 (2017)

2017 arXiv
[21]

Diederik P Kingma and Max Welling. 2013. Auto-Encoding Variational Bayes. arXiv preprint arXiv:1312.6114 (2013)

2013 arXiv
[22]

Kenji Kawaguchi. 2016. Deep Learning without Poor Local Minima.arXiv preprint arXiv:1605.07110 (2016)

2016 arXiv
[23]

Guido F Montufar, Razvan Pascanu, Kyunghyun Cho, and Yoshua Bengio. 2014. On the Number of Linear Regions of Deep Neural Networks. arXiv preprint arXiv:1402.1869 (2014)

2014 arXiv
[24]

Changliu Liu, Tamar Arnon, Christopher Lazarus, Alexander Strong, Clark Bar- rett, and Mykel J Kochenderfer. 2019. Algorithms for Verifying Neural Networks. arXiv preprint arXiv:1903.06758 (2019)

2019 arXiv
[25]

Maithra Raghu, Ben Poole, Jon Kleinberg, Surya Ganguli, and Jascha Sohl- Dickstein. 2017. On the Expressive Power of Neural Networks with Relu Activa- tions. arXiv preprint arXiv:1711.02060 (2017)

2017 arXiv
[26]

Amir Pnueli. 1977. The Temporal Logic of Programs. 18th Annual Symposium on Foundations of Computer Science (sfcs 1977) (1977)

1977
[27]

Wenjie Ruan, Xinming Huang, and Marta Kwiatkowska. 2018. Reachability Analysis of Deep Neural Networks with Provable Guarantees. arXiv preprint arXiv:1805.02242 (2018)

2018 arXiv
[28]

Danilo Jimenez Rezende, Shakir Mohamed, and Daan Wierstra. 2014. Stochastic Backpropagation and Approximate Inference in Deep Generative Models. (2014)

2014
[29]

Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. 2018. Fast and Effective Robustness Certification. Advances in Neural Information Processing Systems (2018)

2018
[30]

Rolf Schneider. 1993. Convex Bodies: The Brunn-Minkowski Theory. Cambridge University Press (1993)

1993
[31]

Vincent Tjeng, Kai Xiao, and Russ Tedrake. 2019. Evaluating Robustness of Neural Networks with Mixed Integer Programming. arXiv preprint arXiv:1711.07356 (2019)

2019 arXiv
[32]

Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. 2019. An Abstraction-Based Framework for Neural Network Verification. arXiv preprint arXiv:1810.09031 (2019)

2019 arXiv
[33]

Hoang Dung Tran, Stanley Bak, Weiming Xiang, and Taylor T. Johnson. 2020. Verification of Deep Convolutional Neural Networks Using ImageStars. In Com- puter Aided Verification: 32nd International Conference, CA V 2020. Springer, 18–42. https://doi.org/10.1007/978-3-030-53288-8_2

2020 doi
[34]

Jakub M Tomczak and Max Welling. 2018. VAE with a VampPrior. Proceedings of the 21st International Conference on Artificial Intelligence and Statistics (2018)

2018
[35]

Andrei Vasilache, Lucas Brodbeck, and Tommaso Dreossi. 2022. Verifying Tem- poral Logic Specifications in Neural Network Controllers. 2022 ACM/IEEE 6th International Conference on Formal Methods in Software Engineering (FormaliSE) (2022)

2022
[36]

Laurens van der Maaten and Geoffrey Hinton. 2008. Visualizing Data using t-SNE. Journal of Machine Learning Research (2008)

2008
[37]

Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. 2020. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Infor- mation Processing Systems 33 (2020)

2020
[38]

Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. 2021. Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. Ad- vances in Neural Information Processing Systems...

2021
[39]

Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel
[40]

Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. 2021. Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers. InInterna- tional Conference on Learning Representations . https...

2021
[2018]

Advances in Neural Information Processing Systems 31 (2018), 4939–

Efficient Neural Network Robustness Certification with General Activation Functions. Advances in Neural Information Processing Systems 31 (2018), 4939–

2018
[4948]

https://arxiv.org/pdf/1811.00866.pdf Received 31 October 2024

2024 arXiv

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.

[1] [1]

Takumi Akazaki and Yang Liu. 2018. Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning. In International Symposium on Formal Methods. Springer, 456–465

work page 2018

[2] [2]

Mohammed Al-Nuaimi, Sapto Wibowo, Hongyang Qu, Jonathan Aitken, and Sandor Veres. 2021. Hybrid Verification Technique for Decision-Making of Self-Driving Vehicles. Journal of Sensor and Actuator Networks 10, 3 (2021), 42. https://doi.org/10.3390/jsan10030042

work page doi:10.3390/jsan10030042 2021

[3] [3]

C Bradford Barber, David P Dobkin, and Hannu Huhdanpaa. 1996. The Quickhull Algorithm for Convex Hulls. ACM Transactions on Mathematical Software (TOMS) (1996)

work page 1996

[4] [4]

Michael M Bronstein, Joan Bruna, Yann LeCun, Arthur Szlam, and Pierre Van- dergheynst. 2017. Geometric Deep Learning: Going Beyond Euclidean Data. IEEE Signal Processing Magazine (2017)

work page 2017

[5] [5]

Rudy Bunel, Isil Dillig Turkaslan, and Philip HS Torr. 2018. A Unified View of Piecewise Linear Neural Network Verification. Advances in Neural Information Processing Systems (2018)

work page 2018

[6] [6]

Anna Choromanska, Mikael Henaff, Michael Mathieu, Gerard Ben Arous, and Yann LeCun. 2015. The Loss Surfaces of Multilayer Networks. Proceedings of the Eighteenth International Conference on Artificial Intelligence and Statistics (2015)

work page 2015

[7] [7]

Frank H Clarke. 1998. Nonsmooth Analysis and Control Theory . Springer

work page 1998

[8] [8]

Nat Dilokthanakul, Pedro AM Mediano, Marta Garnelo, Matthew CH Lee, Hugh Salimbeni, Kai Arulkumaran, and Murray Shanahan. 2016. Deep Unsupervised Clustering with Gaussian Mixture Variational Autoencoders. arXiv preprint arXiv:1611.02648 (2016)

arXiv 2016