Pith. sign in

REVIEW 3 major objections 5 minor 47 references

Creating a Formally Verified Neural Network for Autonomous Navigation: An Experience Report

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

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

Pith's one-line read This experience report argues that training a small path-centring regression network with differentiable-logic constraints improves its local adversarial robustness, but that none of the verifiers tried could formally verify the trained…

desk verdict An honest workshop report on why regression-network verification is hard, but the abstract oversells the result and the training benefit is not demonstrated. read the letter →

arxiv 2411.14163 v1 pith:UQLMIQTD submitted 2024-11-21 cs.LO cs.CVcs.LG

Syed Ali Asadullah Bukhari , Thomas Flinkow , Medet Inkarbekov , Barak A. Pearlmutter , Rosemary Monahan This is my paper · ORCID
classification cs.LOcs.CVcs.LG
keywords neuralnetworkverificationexperiencereportdifferentiablelogicsGödelfuzzylogicadversarialrobustnessautonomousnavigationregressionformaltools
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

The paper is an experience report from a case study on building a formally verified neural network for autonomous navigation. The authors train a small regression network to locate the track centre from camera images of a small robot car, and try to make it correct by construction by adding Gödel fuzzy-logic translations of a local robustness property as extra loss terms. They report that constrained training improves constraint accuracy and adversarial robustness compared with vanilla training, but that training with constraints does not guarantee the property holds. The verification half of the case study did not succeed: every verifier tried either crashed, returned unknown, or reported unsupported operations, mainly because the network is a regression network with max-pooling and tanh layers. A sympathetic reading is that the paper establishes the promise of differentiable-logic training and the current gap in verification tooling for such networks.

What carries the argument

The load-bearing mechanism is the translation of the robustness constraint into a differentiable loss term using Gödel fuzzy logic, with conjunction as min, disjunction as max, and implication $x \to y$ as 1 if $x < y$ else $y$; a projected-gradient-descent search inside the $\epsilon$-ball supplies a worst-case counterexample for the constraint, and adaptive loss balancing weighs the logical loss against the mean-squared-error loss. This turns the verification property into an extra training objective, so the network is pushed toward satisfying it during learning. The second half of the machinery is the network architecture itself: a small convolutional regression net with max-pooling and a final tanh layer, chosen for tractability but precisely the features that make post-training verification fail.

What would settle it

A concrete observation that would settle whether the central claim is right: search a held-out dataset image $x_0$ for a perturbation $x$ with $\|x_0 - x\|_\infty \le 48/255$ that moves either output coordinate by more than $0.1$; finding one refutes the robustness property at that point, and since the paper reports no verifier could decide the property, a successful decision either way would directly test its conclusion about verification tooling.

Watch

Extended reading notes

Core claim

The central claim, stated on the paper's own terms, is that the loop of differentiable-logic training followed by formal verification is a plausible pipeline for safety properties in autonomous navigation, and that the bottleneck is tooling, not the training idea. Concretely, they show that adding the constraint $\forall x.\ \|x_0 - x\|_\infty \le \epsilon \Rightarrow \|N(x_0) - N(x)\|_\infty \le \delta$ as a Gödel fuzzy-logic loss term, with $\epsilon = 48/255$ and $\delta = 0.1$, raises constraint accuracy and adversarial robustness relative to vanilla training. They do not claim the constrained network is verified; in fact they report that one verifier was unsuitable for regression tasks, and through a unified verifier interface the attempted verifiers all failed or returned unknown, while a bound-estimation toolbox produced wide, unhelpful intervals. The discovery is an experience-level one: verification tools currently support classification networks with ReLU activations but not regression networks containing max-pooling and tanh, and verification remains local to data points, giving no guarantees on unseen images.

Load-bearing premise

The load-bearing premise is that the local robustness property used in Eq. (2)—keeping the predicted track centre within $\delta = 0.1$ output units for any input perturbation of at most $\epsilon = 48/255$—is a meaningful safety condition for keeping the robot on the track, and that local checks on data points transfer to real operation.

Editorial extensions

If this is right

  • Training with differentiable-logic robustness constraints, as implemented here, improves constraint accuracy and adversarial robustness relative to standard training on the same data.
  • Adding constraints during training does not by itself guarantee that the network satisfies them after training, so a separate verification step remains necessary.
  • For regression networks with max-pooling and tanh layers, currently available verifiers do not produce a verification result; they error out or return unknown, so verification-friendly architectures are a prerequisite.
  • Formal verification of such networks is local to input data points; it does not provide guarantees on unseen images, limiting the safety case for real deployment.
  • The estimated output bounds from the bound-estimation tool were too wide to certify robustness even at small perturbations.

Reading between the lines

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

  • The report leaves implicit that swapping max-pooling for strided convolutions and the tanh output for a piecewise-linear activation would likely bring the architecture into the fragment current verifiers support; re-running the same experiment on that architecture is a direct test of this reading.
  • A stronger safety case would replace the pointwise local robustness property with a global Lipschitz bound over the set of images the car can actually encounter, addressing the paper's own caveat that local checks give no guarantees on unseen data.
  • Because the constrained training uses adversarial examples only for the constraint loss and not for the mean-squared-error term, a head-to-head comparison with ordinary adversarial training on the same network would isolate whether the logic-based loss is what drives the robustness gain.
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.

Referee Report

3 major / 5 minor

Summary. The paper reports a case study on training a small convolutional regression network for JetBot road-following using a custom 385-image LEGO dataset, comparing standard training with training augmented by Gödel fuzzy-logic robustness constraints. It then attempts formal verification of a local robustness property using α,β-CROWN, DNNV, and NNV, and reports lessons learned. The paper claims improved constraint accuracy and adversarial robustness from constrained training, while documenting that none of the verifiers successfully certified the property: DNNV backends failed or returned unknown, and NNV produced only very loose output intervals.

Significance. If the claims are appropriately scoped, the experience report has value for the verification community: it documents concrete tool failures on a regression network with max-pooling and tanh layers, makes a small dataset publicly available, and provides a falsifiable negative data point about the current readiness of neural-network verifiers for this class of networks. However, the positive claim that constrained training improves robustness is not yet supported by the evidence as presented, and the title and abstract substantially overstate the degree of formal verification achieved. With revision, this can be a solid experience report; in its current form the central claims need rebalancing.

major comments (3)
  1. [Abstract; §4.2] The title and abstract promise a “formally verified neural network” and describe “guaranteeing the behaviour of the neural network after training”, but the body reports that no verifier certified Eq. (2): DNNV’s BaB and Reluplex failed on unsupported computation graphs, ERAN returned unknown, nnenum returned a generic error, and NNV’s estimateNetworkOutputBounds produced intervals far too wide to certify δ=0.1 (Listing 2 and Table 2). The paper itself notes in §4.1, citing [12], that training with constraints does not guarantee their satisfaction. The title and abstract should be revised to match the experience-report outcome, for example by saying the work explores the use of differentiable logics and reports on verification attempts, rather than claiming a verified network.
  2. [§4.1; Figs. 4 and 5] The central positive finding—that constrained training improves constraint accuracy and adversarial robustness—rests on training-set loss/constraint-accuracy curves and a single adversarial image at epoch 45. No train/validation/test split is described; the dataset is 385 images (§3.2) and both runs use batch size 16. Since the PGD counterexamples used in constraint training are generated from the training set (§3.4), an improved training-set curve is compatible with the model memorizing those counterexamples rather than learning a generalizable robustness property. To support the generalization claim, the authors should evaluate on held-out images, report results over multiple seeds, or explicitly reframe the observation as training-set constraint accuracy without generalization language.
  3. [§3.4; Eq. (2)] The robustness property Eq. (2) is presented as a “basic safety property”, but no argument connects the chosen parameters (ε=48/255, δ=0.1) or the output-coordinate deviation to the actual navigation behaviour of the JetBot, such as track width, vehicle speed, or control-loop sensitivity. Without such a connection, Eq. (2) is a local Lipschitz-style condition whose satisfaction or violation has no demonstrated safety implication. The paper itself acknowledges in §4.3 that verification is local to data points and provides no guarantees for unseen data; the property should be scoped accordingly and its status as a safety property either justified with a concrete argument or softened.
minor comments (5)
  1. [§4.2] The text says NNV provides a “relatively simplier interface”; the intended word is “simpler”.
  2. [§4.2; Table 2] The sentence “the estimateNetworkOutputBounds function does return any tighter bounds for the network’s output” appears to be missing the word “not”, since Table 2 shows the bounds are not tight enough to certify the property.
  3. [Fig. 5 caption] The caption “Vanilla constrained-training” should include a comma or dash to separate the two legend entries.
  4. [§1; reference [10]] The claim that “the choice of a logic does not have a major impact” is based on the authors’ own preprint [10], which is listed as under review; this should be stated explicitly so readers can weigh the evidence.
  5. [§4.2] The paper states that α,β-CROWN was “not suitable for the verification of regression tasks without modification” but gives no detail on the modification needed; adding a sentence on the specific limitation encountered would make the observation more actionable.

Circularity Check

0 steps flagged · score 2.0 of 10

No significant circularity; one minor self-citation for logic choice is not load-bearing.

full rationale

We walked the paper's derivation chain and found no step in which an output quantity is identical to an input by construction, and no fitted parameter renamed as a prediction. The central empirical findings—that α,β-CROWN is unsuitable for this regression network, that DNNV backends either error or return 'unknown', and that NNV produces only coarse output intervals—are direct tool outputs and are not derived from any assumption that already contains the conclusion. The only overlapping-author citation is [10], used twice: to support the statement "Previous experimental results [10] suggest that the choice of a logic does not have a major impact" and to acknowledge that the PGD-based constraint-training code is "based on [10]". Neither use is load-bearing for the report's main observations: the Gödel-logic choice is not the reason the verifiers failed, and the code provenance is an implementation detail. The abstract's wording "guaranteeing the behaviour of the neural network after training" is stronger than what Section 4.2 actually reports (no tool certified Eq. (2)), and the constraint-accuracy improvement in Fig. 5 is shown on training curves without a held-out split or multiple seeds; these are correctness and evidentiary weaknesses, not circularity. We therefore assign score 2 for the minor non-load-bearing self-citation.

Assumptions & free parameters 2 free parameters · 3 assumptions · 0 invented entities

The paper introduces no new theoretical entities. Its load-bearing choices are the hand-set robustness thresholds epsilon and delta, and the assumptions that differentiable-logic training and PGD counterexamples lead to constraint satisfaction, plus the relevance of the local robustness property to safety.

free parameters (2)
  • Robustness perturbation bound epsilon = 48/255, approximately 0.188 in normalised pixel units
    Set by hand as the default in Listing 1; controls the size of the input region over which robustness is claimed and was not varied in the experiments.
  • Output tolerance delta = 0.1 in output coordinate units
    Set by hand in Listing 1; controls the allowed output change under perturbation and is not justified by any task requirement.
assumptions (3)
  • domain assumption Gödel fuzzy logic translation of the robustness constraint into a differentiable loss guides the network toward satisfying the constraint.
    Invoked in Section 3.1; the paper cites [9,10,12] but also states in Section 3.4, following [12], that training with constraints does not guarantee satisfaction.
  • domain assumption Projected gradient descent finds a worst-case perturbation inside the epsilon-neighbourhood for use as a training counterexample.
    Invoked in Section 3.4 to approximate the universal robustness property; PGD is a local search and may miss the true adversarial input.
  • domain assumption Local robustness at images in the dataset is the safety property of interest for the navigation task.
    Section 3.4 defines the property and Section 4.3 notes verification is limited to data points, with no guarantee for unseen data.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Creating a Formally Verified Neural Network for Autonomous Navigation: An Experience Report." pith.science (2026). https://pith.science/paper/UQLMIQTD

@misc{pith2026241114163,
  author       = {Pith},
  title        = {Pith review of: Creating a Formally Verified Neural Network for Autonomous Navigation: An Experience Report},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/UQLMIQTD}},
  note         = {Machine review of arXiv:2411.14163}
}
read the original abstract

The increased reliance of self-driving vehicles on neural networks opens up the challenge of their verification. In this paper we present an experience report, describing a case study which we undertook to explore the design and training of a neural network on a custom dataset for vision-based autonomous navigation. We are particularly interested in the use of machine learning with differentiable logics to obtain networks satisfying basic safety properties by design, guaranteeing the behaviour of the neural network after training. We motivate the choice of a suitable neural network verifier for our purposes and report our observations on the use of neural network verifiers for self-driving systems.

Figures

Figures reproduced from arXiv: 2411.14163 by the authors.

Figure 1
Figure 1. Differentiable logics allow for the use of logical constraints during training by translating them [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Samples from the LEGO road dataset showing various lighting conditions and track configura [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. The proposed neural network architecture for extracting the path centre in an input image of [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Comparison of predictions of models trained without (vanilla) and with logical constraints [PITH_FULL_IMAGE:figures/full_fig_p007_4.png]
Figure 5
Figure 5. Figure 5: The prediction loss (i.e., mean squared error; lower is better) and constraint accuracy (higher is [PITH_FULL_IMAGE:figures/full_fig_p007_5.png]
Figure 6
Figure 6. Figure 6: An image (converted to grey scale) from the LEGO dataset taken as a running example. [PITH_FULL_IMAGE:figures/full_fig_p009_6.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

47 extracted references · 22 canonical work pages

  1. [12]

    Eleonora Giunchiglia, Mihaela Catalina Stoian & Thomas Lukasiewicz (2022): Deep Learning with Logical Constraints. In: Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence , International Joint Conferences on Artificial Intelligence Organization, Vienna, Austria, pp. 5478–5485, doi:10.24963/ijcai.2022/767

    doi:10.24963/ijcai.2022/767 2022

  2. [1]

    In Aaron Dutle, Mariano M

    Stanley Bak (2021): Nnenum: Verification of ReLU Neural Networks with Optimized Abstraction Refine- ment. In Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz & Ivan Perez, editors: NASA Formal Methods, Lecture Notes in Computer Science, Springer International Publishing, Cham, pp. 19–36, doi:10.1007/978-3-030-76384-8_2

    doi:10.1007/978-3-030-76384-8_2 2021

  3. [2]

    arXiv:2109.00498

    Stanley Bak, Changliu Liu & Taylor Johnson (2021):The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results, doi:10.48550/arXiv.2109.00498. arXiv:2109.00498

    arXiv doi:10.48550/arxiv.2109.00498 2021

  4. [3]

    Johnson (2023):The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results, doi:10.48550/arXiv.2312.16760

    Christopher Brix, Stanley Bak, Changliu Liu & Taylor T. Johnson (2023):The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results, doi:10.48550/arXiv.2312.16760. arXiv:2312.16760

    arXiv doi:10.48550/arxiv.2312.16760 2023

  5. [4]

    Bunel, Ilker Turkaslan, Philip Torr, Pushmeet Kohli & Pawan K

    Rudy R. Bunel, Ilker Turkaslan, Philip Torr, Pushmeet Kohli & Pawan K. Mudigonda (2018):A Unified View of Piecewise Linear Neural Network Verification. In: Advances in Neural Information Processing Systems, 31, Curran Associates, Inc

    work page 2018

  6. [5]

    Daggitt, Wen Kokke, Guy Katz, Guy Amir & Idan Refaeli (2022): Neural Network Robustness as a Verification Property: A Principled Case Study

    Marco Casadio, Ekaterina Komendantskaya, Matthew L. Daggitt, Wen Kokke, Guy Katz, Guy Amir & Idan Refaeli (2022): Neural Network Robustness as a Verification Property: A Principled Case Study. In Sharon Shoham & Yakir Vizel, editors: Computer Aided Verification, Lecture Notes in Computer Science, Springer International Publishing, pp. 219–231, doi:10.1007...

    doi:10.1007/978-3-031-13185-1_11 2022

  7. [6]

    In: Proceedings of the 35th International Conference on Machine Learning, PMLR, pp

    Zhao Chen, Vijay Badrinarayanan, Chen-Yu Lee & Andrew Rabinovich (2018): GradNorm: Gradient Normalization for Adaptive Loss Balancing in Deep Multitask Networks . In: Proceedings of the 35th International Conference on Machine Learning, PMLR, pp. 794–803

    work page 2018

  8. [7]

    Pappas (2022): Risk verifica- tion of stochastic systems with neural network controllers

    Matthew Cleaveland, Lars Lindemann, Radoslav Ivanov & George J. Pappas (2022): Risk verifica- tion of stochastic systems with neural network controllers . Artificial Intelligence 313, p. 103782, doi:10.1016/j.artint.2022.103782

    arXiv 2022

Show all 47 references
  1. [8]

    comma.ai

    CommaAI (2024): Commaai/Openpilot. comma.ai. Available at https://github.com/commaai/ openpilot

    2024

  2. [9]

    In: Proceedings of the 36th International Conference on Machine Learning, PMLR, pp

    Marc Fischer, Mislav Balunovic, Dana Drachsler-Cohen, Timon Gehr, Ce Zhang & Martin Vechev (2019): DL2: Training and Querying Neural Networks with Logic. In: Proceedings of the 36th International Conference on Machine Learning, PMLR, pp. 1931–1941. 188 Creating a Formally Veri...

    2019

  3. [10]

    Pearlmutter & Rosemary Monahan (2024): Comparing Differentiable Logics for Learning with Logical Constraints

    Thomas Flinkow, Barak A. Pearlmutter & Rosemary Monahan (2024): Comparing Differentiable Logics for Learning with Logical Constraints. arXiv:2407.03847. (under review)

    2024 arXiv

  4. [11]

    Fremont, Johnathan Chiu, Dragos D

    Daniel J. Fremont, Johnathan Chiu, Dragos D. Margineantu, Denis Osipychev & Sanjit A. Seshia (2020): Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI. In: Computer Aided Verification: 32nd International Conference, CA V 2020, Los Ange...

    2020 doi

  5. [13]

    Habeeb, Nabarun Deka, Deepak D’Souza, Kamal Lodaya & Pavithra Prabhakar (2023): Verification of Camera-Based Autonomous Systems

    P. Habeeb, Nabarun Deka, Deepak D’Souza, Kamal Lodaya & Pavithra Prabhakar (2023): Verification of Camera-Based Autonomous Systems. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 42(10), pp. 3450–3463, doi:10.1109/TCAD.2023.3240131

    2023

  6. [14]

    (2024): LI-IMX219-MIPI-FF-NANO-H136—Leopard Imaging Inc

    Leopard Imaging Inc. (2024): LI-IMX219-MIPI-FF-NANO-H136—Leopard Imaging Inc. Available at https://leopardimaging.com/product/platform-partners/nvidia/nvidia-jetson-nano/ nano-mipi-camera-kits/li-imx219-mipi-ff-nano/li-imx219-mipi-ff-nano-h136/

    2024

  7. [15]

    Carpenter, James Weimer, Rajeev Alur, George J

    Radoslav Ivanov, Taylor J. Carpenter, James Weimer, Rajeev Alur, George J. Pappas & Insup Lee (2020):Case study: verifying the safety of an autonomous racing car with a neural network controller. In: Proceedings of the 23rd International Conference on Hybrid Systems: Computati...

    2020

  8. [16]

    (2024): JetBot

    JetBot. (2024): JetBot. Available at https://jetbot.org/master/index.html

    2024

  9. [17]

    Available at https://jetbot.org/master/examples/road_ following.html

    JetBot (2024): Road Following—JetBot. Available at https://jetbot.org/master/examples/road_ following.html

    2024

  10. [18]

    Dill, Kyle Julian & Mykel J

    Guy Katz, Clark Barrett, David L. Dill, Kyle Julian & Mykel J. Kochenderfer (2017): Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In Rupak Majumdar & Viktor Kunˇcak, editors: Computer Aided Verification, Lecture Notes in Computer Science, Springer Inter...

    2017 doi

  11. [19]

    Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zelji´c, David L

    Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zelji´c, David L. Dill, Mykel J. Kochenderfer & Clark Barrett (2019): The Marabou Framework for Verification and Analysis of Deep Neural ...

    2019 doi

  12. [20]

    Zico Kolter, Krishnamurthy Dvijotham & Huan Zhang (2023): Prov- ably Bounding Neural Network Preimages

    Suhas Kotha, Christopher Brix, J. Zico Kolter, Krishnamurthy Dvijotham & Huan Zhang (2023): Prov- ably Bounding Neural Network Preimages . In A. Oh, T. Neumann, A. Globerson, K. Saenko, M. Hardt & S. Levine, editors: Advances in Neural Information Processing Systems , 36, Curr...

    2023

  13. [21]

    IEEE/CAA Journal of Automatica Sinica 7(2), pp

    Yifang Ma, Zhenyu Wang, Hong Yang & Lin Yang (2020): Artificial intelligence applications in the de- velopment of autonomous vehicles: A survey. IEEE/CAA Journal of Automatica Sinica 7(2), pp. 315–329, doi:10.1109/JAS.2020.1003021

    2020

  14. [22]

    In: International Conference on Learning Representations

    Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras & Adrian Vladu (2018): To- wards Deep Learning Models Resistant to Adversarial Attacks. In: International Conference on Learning Representations. Available at https://openreview.net/forum?id=rJzIBfZAb

    2018

  15. [23]

    Johnson (2022): The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Results , doi:10.48550/arXiv.2212.10376

    Mark Niklas Müller, Christopher Brix, Stanley Bak, Changliu Liu & Taylor T. Johnson (2022): The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Results , doi:10.48550/arXiv.2212.10376. arXiv:2212.10376. S. A. A. Bukhari, T. Flinkow,...

    2022 doi arXiv

  16. [24]

    Available at https://www.nvidia.com/en-us/autonomous-machines/embedded-systems/jetson-nano/ product-development/

    NVIDIA (2024): Jetson Nano Brings the Power of Modern AI to Edge Devices | NVIDIA . Available at https://www.nvidia.com/en-us/autonomous-machines/embedded-systems/jetson-nano/ product-development/

    2024

  17. [25]

    Journal of Big Data 10(1), p

    Budi Padmaja, CH VKNSN Moorthy, N Venkateswarulu & Myneni Madhu Bala (2023):Exploration of issues, challenges and latest developments in autonomous cars. Journal of Big Data 10(1), p. 61, doi:10.1186/s40537- 023-00701-y

    2023 doi

  18. [26]

    Pomerleau (1988): ALVINN: An Autonomous Land Vehicle in a Neural Network

    Dean A. Pomerleau (1988): ALVINN: An Autonomous Land Vehicle in a Neural Network . In: Advances in Neural Information Processing Systems (NIPS) , 1, Morgan-Kaufmann, pp. 305–15. Available at https://proceedings.neurips.cc/paper_files/paper/1988/file/ 812b4ba287f5ee0bc9d43bbf5b...

    1988

  19. [27]

    Santora & Mohsin M

    Ratheesh Ravindran, Michael J. Santora & Mohsin M. Jamali (2020): Multi-object detection and track- ing, based on DNN, for autonomous vehicles: A review . IEEE Sensors Journal 21(5), pp. 5668–5677, doi:10.1109/JSEN.2020.3041615

    2020

  20. [28]

    Communica- tions of the ACM 65(7), pp

    Sanjit A Seshia, Dorsa Sadigh & S Shankar Sastry (2022): Toward verified artificial intelligence. Communica- tions of the ACM 65(7), pp. 46–55, doi:10.1145/3503914

    2022 doi

  21. [29]

    arXiv preprint arXiv:2405.21063

    Zhouxing Shi, Qirui Jin, Zico Kolter, Suman Jana, Cho-Jui Hsieh & Huan Zhang (2024): Neural Network Verification with Branch-and-Bound for General Nonlinearities. arXiv preprint arXiv:2405.21063

    2024 arXiv

  22. [30]

    Dwyer (2021):DNNV: A Framework for Deep Neural Network Verification

    David Shriver, Sebastian Elbaum & Matthew B. Dwyer (2021):DNNV: A Framework for Deep Neural Network Verification. In Alexandra Silva & K. Rustan M. Leino, editors: Computer Aided Verification, Lecture Notes in Computer Science, Springer International Publishing, Cham, pp. 137–...

    2021 doi

  23. [31]

    In: Advances in Neural Information Processing Systems, 32, Curran Associates, Inc

    Gagandeep Singh, Rupanshu Ganvir, Markus Püschel & Martin Vechev (2019):Beyond the Single Neuron Convex Barrier for Neural Network Certification. In: Advances in Neural Information Processing Systems, 32, Curran Associates, Inc

    2019

  24. [32]

    In: Proceedings of the 32nd International Conference on Neural Information Processing Systems, NIPS’18, Curran Associates Inc., Red Hook, NY , USA, pp

    Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel & Martin Vechev (2018): Fast and Effective Robustness Certification. In: Proceedings of the 32nd International Conference on Neural Information Processing Systems, NIPS’18, Curran Associates Inc., Red Hook, NY , USA, ...

    2018

  25. [33]

    In: International Conference on Learning Representations

    Gagandeep Singh, Timon Gehr, Markus Püschel & Martin Vechev (2018):Boosting Robustness Certification of Neural Networks. In: International Conference on Learning Representations

    2018

  26. [34]

    Proceedings of the ACM on Programming Languages 3(POPL), pp

    Gagandeep Singh, Timon Gehr, Markus Püschel & Martin Vechev (2019): An Abstract Domain for Certifying Neural Networks . Proceedings of the ACM on Programming Languages 3(POPL), pp. 1–30, doi:10.1145/3290354

    2019 doi

  27. [35]

    In: EPiC Series in Computing, 94, EasyChair, pp

    Natalia ´Slusarz, Ekaterina Komendantskaya, Matthew Daggitt, Robert Stewart & Kathrin Stark (2023): Logic of Differentiable Logics: Towards a Uniform Semantics of DL. In: EPiC Series in Computing, 94, EasyChair, pp. 473–493, doi:10.29007/c1nt

    2023 doi

  28. [36]

    Available at https://www.sparkfun.com/products/18486

    Sparkfun (2024): SparkFun JetBot AI Kit v3.0 Powered by Jetson Nano—KIT-18486—SparkFun Electronics. Available at https://www.sparkfun.com/products/18486

    2024

  29. [37]

    In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp

    Xiaowu Sun, Haitham Khedr & Yasser Shoukry (2019): Formal verification of neural network controlled autonomous systems. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 147–156

    2019

  30. [38]

    Sebastian Thrun (2010): Toward robotic cars . Commun. ACM 53(4), p. 99–106, doi:10.1145/1721654.1721679

    2010

  31. [39]

    Johnson (2020): Verification of Deep Con- volutional Neural Networks Using ImageStars

    Hoang-Dung Tran, Stanley Bak, Weiming Xiang & Taylor T. Johnson (2020): Verification of Deep Con- volutional Neural Networks Using ImageStars. In Shuvendu K. Lahiri & Chao Wang, editors: Computer Aided Verification, Lecture Notes in Computer Science, Springer International Pub...

    2020 doi

  32. [40]

    Johnson (2020): NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems

    Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak & Taylor T. Johnson (2020): NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems . In Shuvendu K. Lahiri ...

    2020

  33. [41]

    Artificial Intelligence 302, p

    Emile van Krieken, Erman Acar & Frank van Harmelen (2022): Analyzing Differentiable Fuzzy Logic Operators. Artificial Intelligence 302, p. 103602, doi:10.1016/j.artint.2021.103602. arXiv:2002.06100

    2022

  34. [42]

    Zico Kolter (2021): Beta- CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification

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

    2021

  35. [43]

    Advances in Neural Information Processing Systems 33

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

    2020

  36. [44]

    In: International Conference on Learning Representations

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

    2021

  37. [45]

    Zico Kolter (2022): General Cutting Planes for Bound-Propagation-Based Neural Network Verification

    Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh & J. Zico Kolter (2022): General Cutting Planes for Bound-Propagation-Based Neural Network Verification . Advances in Neural Information Processing Systems

    2022

  38. [46]

    In: Advances in Neural Information Processing Systems, 31, Curran Associates, Inc

    Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh & Luca Daniel (2018):Efficient Neural Network Robustness Certification with General Activation Functions. In: Advances in Neural Information Processing Systems, 31, Curran Associates, Inc

    2018

  39. [47]

    Burke (2024): Autonomous driving system: A comprehensive survey

    Jingyuan Zhao, Wenyi Zhao, Bo Deng, Zhenghong Wang, Feng Zhang, Wenxiang Zheng, Wanke Cao, Jinrui Nan, Yubo Lian & Andrew F. Burke (2024): Autonomous driving system: A comprehensive survey . Expert Systems with Applications 242, p. 122836, doi:10.1016/j.eswa.2023.122836. Avail...

    2024

Pith tools

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