Probabilistic Verification of Neural Networks via Efficient Probabilistic Hull Generation

Guoqiang Li; Hongfei Fu; Jingyang Li; Xin Chen

arxiv: 2604.21556 · v1 · submitted 2026-04-23 · 💻 cs.AI · cs.SE

Probabilistic Verification of Neural Networks via Efficient Probabilistic Hull Generation

Jingyang Li , Xin Chen , Hongfei Fu , Guoqiang Li This is my paper

Pith reviewed 2026-05-09 21:07 UTC · model grok-4.3

classification 💻 cs.AI cs.SE

keywords neural network verificationprobabilistic safetyregression treesprobabilistic hullssafety constraintsACAS Xurocket landerboundary-aware sampling

0 comments

The pith

A framework computes guaranteed bounds on the probability that a neural network satisfies safety constraints when inputs follow a probability distribution.

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

The paper develops a method to calculate bounds on how likely a neural network is to produce safe outputs when its inputs come from a probability distribution rather than single points. It achieves this by dividing the input space using regression trees trained on samples that focus on the safety boundary, then identifying regions that are definitely safe or definitely unsafe to narrow the possible range of the safety probability. This matters for applications where inputs vary randomly due to noise or uncertainty, such as in autonomous control systems. The process includes iterative refinement that prioritizes uncertain areas to improve the bounds efficiently. Evaluations on standard benchmarks demonstrate better performance than previous approaches.

Core claim

We propose a neural network probabilistic verification framework which computes a guaranteed range for the safe probability by efficiently finding safe and unsafe probabilistic hulls. Our approach consists of three main innovations: a state space subdivision strategy using regression trees to produce probabilistic hulls, a boundary-aware sampling method which identifies the safety boundary in the input space using samples that are later used for building regression trees, and iterative refinement with probabilistic prioritization for computing a guaranteed range for the safe probability.

What carries the argument

Probabilistic hulls, which are regions in the input space certified as entirely safe or unsafe, produced by regression-tree subdivision from boundary-aware samples.

If this is right

The method produces both lower and upper bounds on the safe probability rather than a single point estimate.
It applies directly to standard benchmarks including the ACAS Xu aircraft collision avoidance system and a rocket lander controller.
Iterative refinement with probabilistic prioritization tightens the bounds without exhaustive enumeration of the input space.
The approach handles inputs modeled by continuous probability distributions instead of requiring fixed or adversarial values.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The subdivision strategy could be adapted to verify properties other than safety constraints, such as reachability or stability in probabilistic settings.
Boundary-aware sampling may reduce computational cost in high-dimensional input spaces compared with uniform or random sampling alone.
If the hulls remain accurate for deeper networks, the framework could support verification of larger models used in real-time control.

Load-bearing premise

Regression trees built from boundary-aware samples can reliably separate safe and unsafe regions in the input space without missing critical boundary areas or requiring prohibitive numbers of samples.

What would settle it

On a benchmark where the true safe probability can be computed exactly by numerical integration over the input distribution, the method's reported range fails to contain the true value or does not narrow with additional refinement iterations.

Figures

Figures reproduced from arXiv: 2604.21556 by Guoqiang Li, Hongfei Fu, Jingyang Li, Xin Chen.

**Figure 1.** Figure 1: Workflow of our regression tree-guided probabilistic verification framework. 4 Main Approach The main idea of our approach for estimating conservative upper and lower bounds for the actual safe probability is to iteratively construct a set of safe hulls: Hs 1 , . . . , Hs N and a set of unsafe hulls: Hu 1 , . . . , Hu M, such that all hulls intersect at most on the facets. Therefore, each hull represents a… view at source ↗

**Figure 2.** Figure 2: Uniform vs. boundary-aware subdivision. Efficiently finding large safe/unsafe hulls plays a key role in our framework. A naive way could be uniformly subdivide the input state space and verify the safety of each piece. However, it is often very expensive and ignores the decision boundary. Directly considering the boundary in probabilistic hull search can be [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗

**Figure 3.** Figure 3: Boundary-aware subdivision for the toy example. Illustrative Toy Examples. Before we show the comparisons, [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗

**Figure 4.** Figure 4: Scatter plot showing the relationship between Us-Ls and runtime for 250 different parameter configurations tested in the grid search. A.2 Rocket Lander Benchmark The same systematic grid search methodology was applied to the Rocket Lander controller. The search space for this benchmark was defined as follows. – Sampling Weights (wuniform, wdistribution). The same five configurations were tested. (0.0, 1.0… view at source ↗

**Figure 5.** Figure 5: Scatter plot showing the relationship between Us-Ls and runtime for 300 different parameter configurations tested in the grid search. – Regression Tree Depth. Three values were considered. 5, 10, and 20. – Impurity Splitting (β). Five values were tested. 0, 0.25, 0.5, 0.75, and 1.0. – Impurity Coefficient (α). Five values were evaluated. 0.05, 0.1, 0.3, 0.5, and 1.0. This yielded a total of 300 parameter … view at source ↗

read the original abstract

The problem of probabilistic verification of a neural network investigates the probability of satisfying the safe constraints in the output space when the input is given by a probability distribution. It is significant to answer this problem when the input is affected by disturbances often modeled by probabilistic variables. In the paper, we propose a novel neural network probabilistic verification framework which computes a guaranteed range for the safe probability by efficiently finding safe and unsafe probabilistic hulls. Our approach consists of three main innovations: (1) a state space subdivision strategy using regression trees to produce probabilistic hulls, (2) a boundary-aware sampling method which identifies the safety boundary in the input space using samples that are later used for building regression trees, and (3) iterative refinement with probabilistic prioritization for computing a guaranteed range for the safe probability. The accuracy and efficiency of our approach are evaluated on various benchmarks including ACAS Xu and a rocket lander controller. The result shows an obvious advantage over the state of the art.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper describes a regression-tree subdivision method with boundary sampling to bound safe probabilities for neural nets on benchmarks like ACAS Xu, but the guarantees look heuristic rather than proven.

read the letter

The one thing to know is that this work proposes using regression trees built from boundary-aware samples to subdivide the input space and produce safe and unsafe probabilistic hulls, then refines them to get a range on the probability of satisfying safety constraints. The approach is new in how it combines these elements for probabilistic verification. It avoids full enumeration by focusing on boundaries and using prioritization in refinement. This could be useful for cases like disturbed inputs to controllers where you want probabilistic rather than deterministic safety. The paper does well in presenting the three innovations clearly and showing evaluation results on ACAS Xu and a rocket lander that indicate better performance than existing methods. That suggests the method is efficient enough for real benchmarks. The soft spot is the lack of a clear argument for why the hulls give true guarantees. The boundary-aware sampling is a heuristic step, and in high-dimensional spaces with potentially complicated safety boundaries, it's possible to miss regions. The claim of a guaranteed range would require showing that the subdivision and hull construction are conservative, but the abstract provides no such sketch or analysis. The stress-test concern about completeness seems valid based on what's described, as nothing forces the trees to cover all critical areas. Overall, the work shows clear thinking on making verification more scalable through sampling and trees. The math and data aren't detailed here, but the citation pattern likely builds on prior verification literature. This is for readers in AI safety and formal verification who deal with probabilistic inputs. It would be valuable to someone wanting algorithmic tools for probability estimation in neural network properties. It deserves a serious referee because the problem matters and the method is concrete, though it may need more on the guarantees to be fully convincing.

Referee Report

2 major / 2 minor

Summary. The paper proposes a neural network probabilistic verification framework that computes a guaranteed range for the safe probability under probabilistic inputs by generating safe and unsafe probabilistic hulls. The approach relies on three innovations: state-space subdivision via regression trees, boundary-aware sampling to identify safety boundaries for tree construction, and iterative refinement using probabilistic prioritization. It is evaluated on ACAS Xu and a rocket lander controller, with claims of improved accuracy and efficiency over prior methods.

Significance. If the hull-generation procedure can be shown to produce sound, conservative bounds without missing unsafe regions, the work would be significant for verification of safety-critical neural controllers under input disturbances. The combination of regression trees for subdivision and boundary-aware sampling offers a potentially scalable alternative to exhaustive or sampling-only techniques in probabilistic settings, and the choice of ACAS Xu as a benchmark is appropriate for assessing practical utility.

major comments (2)

[Abstract / innovation (2)] Abstract and the description of innovation (2): the claim that boundary-aware sampling followed by regression-tree hull construction yields a 'guaranteed range' for safe probability lacks a completeness argument. Finite sampling cannot guarantee that all non-convex decision boundaries (common in ACAS Xu) are captured; without a formal proof or conservative over-approximation step, the resulting hulls may exclude unsafe pockets and invalidate the probability bounds.
[innovation (3)] The iterative refinement procedure (innovation 3): it is unclear how probabilistic prioritization ensures that the final safe/unsafe hulls remain conservative after each subdivision. If a region is misclassified early due to insufficient boundary samples, later refinement steps appear to have no mechanism to detect or correct the error, undermining the 'guaranteed' property.

minor comments (2)

[Abstract] The abstract states that results 'show an obvious advantage' but supplies no quantitative metrics, tables, or comparison baselines; the evaluation section should include explicit probability-range widths, runtime figures, and direct comparisons to prior probabilistic verification tools.
Notation for 'probabilistic hulls' and 'safe probability range' is introduced without a precise mathematical definition or example computation; adding a small illustrative example with explicit input distribution and output constraints would improve clarity.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive and detailed feedback on our manuscript. We address each major comment point by point below, indicating the revisions we will make to strengthen the presentation of our claims.

read point-by-point responses

Referee: [Abstract / innovation (2)] Abstract and the description of innovation (2): the claim that boundary-aware sampling followed by regression-tree hull construction yields a 'guaranteed range' for safe probability lacks a completeness argument. Finite sampling cannot guarantee that all non-convex decision boundaries (common in ACAS Xu) are captured; without a formal proof or conservative over-approximation step, the resulting hulls may exclude unsafe pockets and invalidate the probability bounds.

Authors: We agree that the abstract and the description of innovation (2) do not include a formal completeness argument, and that finite sampling alone cannot provably capture all non-convex decision boundaries without additional mechanisms. The boundary-aware sampling focuses on regions near identified boundaries, and the regression-tree hulls are constructed to classify leaves only when samples are uniformly safe or unsafe, with refinement on mixed regions. However, this does not constitute a rigorous guarantee against missing unsafe pockets. We will revise the abstract to qualify the 'guaranteed range' claim and expand the innovation (2) section to discuss the soundness properties, the role of iterative refinement in mitigating boundary errors, and the limitations for highly non-convex cases. This will be a partial revision focused on clarification rather than a new formal proof. revision: partial
Referee: [innovation (3)] The iterative refinement procedure (innovation 3): it is unclear how probabilistic prioritization ensures that the final safe/unsafe hulls remain conservative after each subdivision. If a region is misclassified early due to insufficient boundary samples, later refinement steps appear to have no mechanism to detect or correct the error, undermining the 'guaranteed' property.

Authors: The referee is correct that the current description of innovation (3) does not explicitly address how early misclassifications are detected or corrected. Our probabilistic prioritization selects high-mass, high-uncertainty regions for further sampling and subdivision, and hulls are only finalized for uniformly classified leaves. Nevertheless, the manuscript lacks a clear statement on conservativeness preservation across iterations. We will revise the innovation (3) section to include a more precise explanation of the refinement loop, specifying that mixed regions are always subdivided until resolved or the computational budget is reached, and that parent-node labels are updated conservatively based on child outcomes. We will also add a short formal sketch or pseudocode to illustrate maintenance of the bounds. This addresses the concern through improved exposition. revision: partial

Circularity Check

0 steps flagged

No circularity: framework computes probability bounds via independent sampling and tree-based subdivision

full rationale

The paper's core claim is a probabilistic verification method that uses boundary-aware sampling to build regression trees for state-space subdivision, followed by probabilistic hull generation and iterative refinement to bound the safe probability. No equations, fitted parameters, or self-citations are presented that would make the output probability range reduce by construction to a quantity defined by the method itself. The sampling and tree construction steps operate on external input distributions and NN evaluations, providing an independent computational pipeline rather than a self-referential loop. This matches the default expectation of a non-circular derivation.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review supplies no explicit free parameters, axioms, or invented entities; the method implicitly assumes that regression trees can approximate safety boundaries and that sampling density suffices for hull construction.

pith-pipeline@v0.9.0 · 5463 in / 1064 out tokens · 24322 ms · 2026-05-09T21:07:00.728737+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

24 extracted references · 24 canonical work pages

[1]

Cengage Learning (1992)

Bain, L.J., Engelhardt, M.: Introduction to Probability and Mathematical Statis- tics (2nd ed.). Cengage Learning (1992)

work page 1992
[2]

CoRRabs/2405.17556(2024)

Boetius, D., Leue, S., Sutter, T.: Probabilistic verification of neural networks using branch and bound. CoRRabs/2405.17556(2024)

work page arXiv 2024
[3]

In: Proceed- ings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019

Cardelli, L., Kwiatkowska, M., Laurenti, L., Paoletti, N., Patane, A., Wicker, M.: Statistical guarantees for the robustness of bayesian neural networks. In: Proceed- ings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019. pp. 5693–5700 (2019)

work page 2019
[4]

Gou, J., Yu, B., Maybank, S.J., Tao, D.: Knowledge distillation: A survey. Int. J. Comput. Vis.129(6), 1789–1819 (2021)

work page 2021
[5]

(eds.) Proceedings of the 20th International Symposium on Automated Technology for Verification and Analysis

Huang, C., Fan, J., Chen, X., Li, W., Zhu, Q.: POLAR: A polynomial arithmetic frameworkforverifyingneural-networkcontrolledsystems.In:Bouajjani,A.,Holík, L., Wu, Z. (eds.) Proceedings of the 20th International Symposium on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 13505, pp. 414–430. Springer (2022)

work page 2022
[6]

Springer (2001)

Jaulin, L., Kieffer, M., Didrit, O., Walter, E.: Applied Interval Analysis. Springer (2001)

work page 2001
[7]

In: The 29th International Conference on Computer Aided Verification (CAV 2017)

Katz, G., Barrett, C.W., Dill, D.L., Julian, K.D., Kochenderfer, M.J.: Reluplex: An efficient SMT solver for verifying deep neural networks. In: The 29th International Conference on Computer Aided Verification (CAV 2017). vol. 10426, pp. 97–117. Springer (2017)

work page 2017
[8]

In: 2016 IEEE/AIAA 35th Digital Avionics Systems Conference (DASC)

Manfredi, G., Jestin, Y.: An introduction to acas xu and the challenges ahead. In: 2016 IEEE/AIAA 35th Digital Avionics Systems Conference (DASC). pp. 1–9 (2016)

work page 2016
[9]

In: Proceedings of the 41st International Conference on Software Engineering: New Ideas and Emerging Results, ICSE (NIER) 2019, Canada

Mangal, R., Nori, A.V., Orso, A.: Robustness of neural networks: a probabilis- tic and practical approach. In: Proceedings of the 41st International Conference on Software Engineering: New Ideas and Emerging Results, ICSE (NIER) 2019, Canada. pp. 93–96 (2019)

work page 2019
[10]

CoRRabs/2206.12227(2022)

Meng, M.H., Bai, G., Teo, S.G., Hou, Z., Xiao, Y., Lin, Y., Dong, J.S.: Adversarial robustnessofdeepneuralnetworks:Asurveyfromaformalverificationperspective. CoRRabs/2206.12227(2022)

work page arXiv 2022
[11]

McGraw-Hill Education (1997)

Mitchell, T.M.: Machine Learning. McGraw-Hill Education (1997)

work page 1997
[12]

In: Learning for Dynamics and Control Conference, L4DC 2023, 15-16 June 2023, Philadelphia, PA, USA

Pilipovsky, J., Sivaramakrishnan, V., Oishi, M., Tsiotras, P.: Probabilistic verifica- tion of relu neural networks via characteristic functions. In: Learning for Dynamics and Control Conference, L4DC 2023, 15-16 June 2023, Philadelphia, PA, USA. Proceedings of Machine Learning Research, vol. 211, pp. 966–979 (2023)

work page 2023
[13]

Tambon, F., Laberge, G., An, L., Nikanjam, A., Mindom, P.S.N., Pequignot, Y., Khomh, F., Antoniol, G., Merlo, E., Laviolette, F.: How to certify machine learning based safety-critical systems? A systematic literature review. Autom. Softw. Eng. 29(2), 38 (2022)

work page 2022
[14]

In: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Con- trol, HSCC 2023, USA,

Tran, H., Choi, S., Okamoto, H., Hoxha, B., Fainekos, G., Prokhorov, D.V.: Quan- titative verification for neural networks using probstars. In: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Con- trol, HSCC 2023, USA,. pp. 4:1–4:12 (2023)

work page 2023
[15]

In: 34th Annual Conference on Neural Information Processing Systems, (NeurIPS 2021)

Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S.S., Hsieh, C.J., Kolter, J.Z.: Beta- crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. In: 34th Annual Conference on Neural Information Processing Systems, (NeurIPS 2021). pp. 29909–29921 (2021) Probabilistic Verification of Neural Networks 17

work page 2021
[16]

In: 7th International Conference on Learning Representations, USA (2019)

Webb, S., Rainforth, T., Teh, Y.W., Kumar, M.P.: A statistical approach to as- sessing neural network robustness. In: 7th International Conference on Learning Representations, USA (2019)

work page 2019
[17]

Weng, T.W., Chen, P.Y., Nguyen, L.M., Squillante, M.S., Boopathy, A., Oseledets, I., Daniel, L.: Proven: Certifying robustness of neural networks with a probabilistic approach97(2019)

work page 2019
[18]

Wicker, M., Laurenti, L., Patane, A., Paoletti, N., Abate, A., Kwiatkowska, M.: Probabilistic reach-avoid for bayesian neural networks. Artif. Intell.334, 104132 (2024)

work page 2024
[19]

In: Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I

Wicker, M., Patane, A., Laurenti, L., Kwiatkowska, M.: Adversarial robustness certification for bayesian neural networks. In: Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14933, pp. 3–28 (2024)

work page 2024
[20]

In: Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part II

Wu, H., Isac, O., Zeljic, A., Tagomori, T., Daggitt, M.L., Kokke, W., Refaeli, I., Amir, G., Julian, K., Bassan, S., Huang, P., Lahav, O., Wu, M., Zhang, M., Komendantskaya, E., Katz, G., Barrett, C.W.: Marabou 2.0: A versatile formal analyzer of neural networks. In: Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Cana...

work page 2024
[21]

In: Advances in Neural Information Processing Systems 33: Annual Con- ference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual (2020)

Xu, K., Shi, Z., Zhang, H., Wang, Y., Chang, K., Huang, M., Kailkhura, B., Lin, X., Hsieh, C.: Automatic perturbation analysis for scalable certified robustness and beyond. In: Advances in Neural Information Processing Systems 33: Annual Con- ference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual (2020)

work page 2020
[22]

In: Formal Modeling and Analy- sis of Timed Systems - 20th International Conference, FORMATS 2022, Warsaw, Poland, September 13-15, 2022, Proceedings

Yang, X., Yamaguchi, T., Tran, H., Hoxha, B., Johnson, T.T., Prokhorov, D.V.: Neural network repair with reachability analysis. In: Formal Modeling and Analy- sis of Timed Systems - 20th International Conference, FORMATS 2022, Warsaw, Poland, September 13-15, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13465, pp. 221–236. Springer (2022)

work page 2022
[23]

In: 31st Annual Conference on Neural Information Processing Systems 2018, (NeurIPS 2018)

Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J., Daniel, L.: Efficient neural net- work robustness certification with general activation functions. In: 31st Annual Conference on Neural Information Processing Systems 2018, (NeurIPS 2018). pp. 4944–4953 (2018) A Hyperparameter and Grid Search Weperformedanextensivegridsearchtodeterminethebestconfigurationfor...

work page 2018
[24]

Each point represents a distinct configura- tion

Figure 4 presents the results, mapping the trade-off betweenUs −L s (vertical axis) and runtime (horizontal axis). Each point represents a distinct configura- tion. The red star highlights thePareto optimal configuration, which outper- forms all other combinations in both metrics. Gray points indicate configurations that are dominated by the Pareto soluti...

work page

[1] [1]

Cengage Learning (1992)

Bain, L.J., Engelhardt, M.: Introduction to Probability and Mathematical Statis- tics (2nd ed.). Cengage Learning (1992)

work page 1992

[2] [2]

CoRRabs/2405.17556(2024)

Boetius, D., Leue, S., Sutter, T.: Probabilistic verification of neural networks using branch and bound. CoRRabs/2405.17556(2024)

work page arXiv 2024

[3] [3]

In: Proceed- ings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019

Cardelli, L., Kwiatkowska, M., Laurenti, L., Paoletti, N., Patane, A., Wicker, M.: Statistical guarantees for the robustness of bayesian neural networks. In: Proceed- ings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019. pp. 5693–5700 (2019)

work page 2019

[4] [4]

Gou, J., Yu, B., Maybank, S.J., Tao, D.: Knowledge distillation: A survey. Int. J. Comput. Vis.129(6), 1789–1819 (2021)

work page 2021

[5] [5]

(eds.) Proceedings of the 20th International Symposium on Automated Technology for Verification and Analysis

Huang, C., Fan, J., Chen, X., Li, W., Zhu, Q.: POLAR: A polynomial arithmetic frameworkforverifyingneural-networkcontrolledsystems.In:Bouajjani,A.,Holík, L., Wu, Z. (eds.) Proceedings of the 20th International Symposium on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 13505, pp. 414–430. Springer (2022)

work page 2022

[6] [6]

Springer (2001)

Jaulin, L., Kieffer, M., Didrit, O., Walter, E.: Applied Interval Analysis. Springer (2001)

work page 2001

[7] [7]

In: The 29th International Conference on Computer Aided Verification (CAV 2017)

Katz, G., Barrett, C.W., Dill, D.L., Julian, K.D., Kochenderfer, M.J.: Reluplex: An efficient SMT solver for verifying deep neural networks. In: The 29th International Conference on Computer Aided Verification (CAV 2017). vol. 10426, pp. 97–117. Springer (2017)

work page 2017

[8] [8]

In: 2016 IEEE/AIAA 35th Digital Avionics Systems Conference (DASC)

Manfredi, G., Jestin, Y.: An introduction to acas xu and the challenges ahead. In: 2016 IEEE/AIAA 35th Digital Avionics Systems Conference (DASC). pp. 1–9 (2016)

work page 2016

[9] [9]

In: Proceedings of the 41st International Conference on Software Engineering: New Ideas and Emerging Results, ICSE (NIER) 2019, Canada

Mangal, R., Nori, A.V., Orso, A.: Robustness of neural networks: a probabilis- tic and practical approach. In: Proceedings of the 41st International Conference on Software Engineering: New Ideas and Emerging Results, ICSE (NIER) 2019, Canada. pp. 93–96 (2019)

work page 2019

[10] [10]

CoRRabs/2206.12227(2022)

Meng, M.H., Bai, G., Teo, S.G., Hou, Z., Xiao, Y., Lin, Y., Dong, J.S.: Adversarial robustnessofdeepneuralnetworks:Asurveyfromaformalverificationperspective. CoRRabs/2206.12227(2022)

work page arXiv 2022

[11] [11]

McGraw-Hill Education (1997)

Mitchell, T.M.: Machine Learning. McGraw-Hill Education (1997)

work page 1997

[12] [12]

In: Learning for Dynamics and Control Conference, L4DC 2023, 15-16 June 2023, Philadelphia, PA, USA

Pilipovsky, J., Sivaramakrishnan, V., Oishi, M., Tsiotras, P.: Probabilistic verifica- tion of relu neural networks via characteristic functions. In: Learning for Dynamics and Control Conference, L4DC 2023, 15-16 June 2023, Philadelphia, PA, USA. Proceedings of Machine Learning Research, vol. 211, pp. 966–979 (2023)

work page 2023

[13] [13]

Tambon, F., Laberge, G., An, L., Nikanjam, A., Mindom, P.S.N., Pequignot, Y., Khomh, F., Antoniol, G., Merlo, E., Laviolette, F.: How to certify machine learning based safety-critical systems? A systematic literature review. Autom. Softw. Eng. 29(2), 38 (2022)

work page 2022

[14] [14]

In: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Con- trol, HSCC 2023, USA,

Tran, H., Choi, S., Okamoto, H., Hoxha, B., Fainekos, G., Prokhorov, D.V.: Quan- titative verification for neural networks using probstars. In: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Con- trol, HSCC 2023, USA,. pp. 4:1–4:12 (2023)

work page 2023

[15] [15]

In: 34th Annual Conference on Neural Information Processing Systems, (NeurIPS 2021)

Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S.S., Hsieh, C.J., Kolter, J.Z.: Beta- crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. In: 34th Annual Conference on Neural Information Processing Systems, (NeurIPS 2021). pp. 29909–29921 (2021) Probabilistic Verification of Neural Networks 17

work page 2021

[16] [16]

In: 7th International Conference on Learning Representations, USA (2019)

Webb, S., Rainforth, T., Teh, Y.W., Kumar, M.P.: A statistical approach to as- sessing neural network robustness. In: 7th International Conference on Learning Representations, USA (2019)

work page 2019

[17] [17]

Weng, T.W., Chen, P.Y., Nguyen, L.M., Squillante, M.S., Boopathy, A., Oseledets, I., Daniel, L.: Proven: Certifying robustness of neural networks with a probabilistic approach97(2019)

work page 2019

[18] [18]

Wicker, M., Laurenti, L., Patane, A., Paoletti, N., Abate, A., Kwiatkowska, M.: Probabilistic reach-avoid for bayesian neural networks. Artif. Intell.334, 104132 (2024)

work page 2024

[19] [19]

In: Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I

Wicker, M., Patane, A., Laurenti, L., Kwiatkowska, M.: Adversarial robustness certification for bayesian neural networks. In: Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14933, pp. 3–28 (2024)

work page 2024

[20] [20]

In: Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part II

Wu, H., Isac, O., Zeljic, A., Tagomori, T., Daggitt, M.L., Kokke, W., Refaeli, I., Amir, G., Julian, K., Bassan, S., Huang, P., Lahav, O., Wu, M., Zhang, M., Komendantskaya, E., Katz, G., Barrett, C.W.: Marabou 2.0: A versatile formal analyzer of neural networks. In: Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Cana...

work page 2024

[21] [21]

In: Advances in Neural Information Processing Systems 33: Annual Con- ference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual (2020)

Xu, K., Shi, Z., Zhang, H., Wang, Y., Chang, K., Huang, M., Kailkhura, B., Lin, X., Hsieh, C.: Automatic perturbation analysis for scalable certified robustness and beyond. In: Advances in Neural Information Processing Systems 33: Annual Con- ference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual (2020)

work page 2020

[22] [22]

In: Formal Modeling and Analy- sis of Timed Systems - 20th International Conference, FORMATS 2022, Warsaw, Poland, September 13-15, 2022, Proceedings

Yang, X., Yamaguchi, T., Tran, H., Hoxha, B., Johnson, T.T., Prokhorov, D.V.: Neural network repair with reachability analysis. In: Formal Modeling and Analy- sis of Timed Systems - 20th International Conference, FORMATS 2022, Warsaw, Poland, September 13-15, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13465, pp. 221–236. Springer (2022)

work page 2022

[23] [23]

In: 31st Annual Conference on Neural Information Processing Systems 2018, (NeurIPS 2018)

Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J., Daniel, L.: Efficient neural net- work robustness certification with general activation functions. In: 31st Annual Conference on Neural Information Processing Systems 2018, (NeurIPS 2018). pp. 4944–4953 (2018) A Hyperparameter and Grid Search Weperformedanextensivegridsearchtodeterminethebestconfigurationfor...

work page 2018

[24] [24]

Each point represents a distinct configura- tion

Figure 4 presents the results, mapping the trade-off betweenUs −L s (vertical axis) and runtime (horizontal axis). Each point represents a distinct configura- tion. The red star highlights thePareto optimal configuration, which outper- forms all other combinations in both metrics. Gray points indicate configurations that are dominated by the Pareto soluti...

work page