Faster Verified Explanations for Neural Networks

Alessandro De Palma; Caterina Urban; Greta Dolcetti

arxiv: 2512.00164 · v2 · submitted 2025-11-28 · 💻 cs.LG · cs.PL

Faster Verified Explanations for Neural Networks

Alessandro De Palma , Greta Dolcetti , Caterina Urban This is my paper

Pith reviewed 2026-05-17 03:27 UTC · model grok-4.3

classification 💻 cs.LG cs.PL

keywords verified explanationsneural network verificationformal explanationsscalabilityrobust explanationsverifier reuseneural network interpretability

0 comments

The pith

FaVeX speeds up verified explanations for neural networks by reusing information across verifier queries and mixing batch with sequential feature processing.

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

The paper develops FaVeX to make verified explanations practical for neural networks. Verified explanations use formal checks to confirm which input features a network's decision truly depends on. Prior approaches required many separate, expensive verifier calls whose cost grows exponentially with network size. FaVeX reduces this cost by dynamically switching between processing groups of features together and one at a time while carrying forward results from earlier checks to prove feature invariance or to locate minimal changes that flip the output. It also supplies a new definition of verifier-optimal robust explanations that records the gaps left by any incomplete verifier, allowing the method to scale to networks containing hundreds of thousands of non-linear activations.

Core claim

FaVeX accelerates the computation by dynamically combining batch and sequential processing of input features, and by reusing information from previous queries, both when proving invariances with respect to certain input features, and when searching for feature assignments altering the prediction. It further introduces verifier-optimal robust explanations, a hierarchical definition that explicitly factors the incompleteness of network verifiers within the explanation.

What carries the argument

The FaVeX algorithm, which reuses prior verifier results while alternating between batch and sequential handling of input features, paired with the verifier-optimal robust explanations definition that records verifier incompleteness.

If this is right

Verified explanations become feasible for networks orders of magnitude larger than before.
Explanations can be produced while explicitly stating the limits of the verifier used.
Repeated verification tasks in explanation generation share computation instead of restarting from scratch.
Formal guarantees on feature relevance can be obtained without requiring a complete verifier.

Where Pith is reading between the lines

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

The reuse mechanism suggests similar incremental verification could apply to other repeated formal checks such as robustness certification.
The hierarchical definition opens a path to refining an explanation once a stronger verifier becomes available without restarting the entire process.

Load-bearing premise

Reusing results across separate verifier queries preserves soundness and the new hierarchical definition accurately reflects verifier incompleteness without introducing undetected errors or overclaiming robustness.

What would settle it

A concrete falsifier would be a network and input where information reuse produces an explanation claiming a feature is irrelevant when a fresh verifier call shows it is relevant, or a timing experiment on a network with over one hundred thousand activations that shows no reduction in total verification time.

read the original abstract

Verified explanations are a principled way to explain the decisions taken by neural networks, which are otherwise black-box in nature. However, these techniques face significant scalability challenges, as they require multiple calls to neural network verifiers, each of them with an exponential worst-case complexity. We present FaVeX, a novel algorithm to compute verified explanations. FaVeX accelerates the computation by dynamically combining batch and sequential processing of input features, and by reusing information from previous queries, both when proving invariances with respect to certain input features, and when searching for feature assignments altering the prediction. Furthermore, we present a novel and hierarchical definition of verified explanations, termed verifieroptimal robust explanations, that explicitly factors the incompleteness of network verifiers within the explanation. Our comprehensive experimental evaluation demonstrates the superior scalability of both FaVeX, and of verifier-optimal robust explanations, which together can produce meaningful formal explanation on networks with hundreds of thousands of non-linear activations.

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

FaVeX gives a practical speed-up for verified explanations by mixing batch-sequential processing with query reuse and adds a hierarchical definition that accounts for verifier incompleteness, but the reuse step needs an explicit soundness argument to back the scalability claims.

read the letter

The key thing to know is that this paper presents FaVeX as a way to compute verified explanations faster by combining batch and sequential feature processing and by reusing information from earlier verifier queries. They also propose a hierarchical definition of verifier-optimal robust explanations that tries to account for the limits of the underlying verifiers. What is new here is the specific algorithm for dynamic switching and reuse, plus that definition. It extends previous work on verified explanations by focusing on efficiency through caching and batching. The paper does well in demonstrating scalability in experiments to networks with hundreds of thousands of non-linear activations. This addresses a real bottleneck in applying these methods to larger models, which is useful for safety and auditing contexts. The soft spots are around the details of the reuse. The central performance gain comes from reusing prior results for both proving feature invariances and searching for altering assignments. However, the provided description does not include an explicit argument or invariant that guarantees this reuse preserves soundness without introducing errors or missing counterexamples. If the full paper includes a formal justification or proof sketch for this, it would shore up the claims; otherwise it remains an assumption to verify. This paper is for researchers in AI verification and explainability who want to push formal methods to larger scales. Readers who work on regulatory compliance or high-stakes AI systems would get practical value from the scalability results and the new explanation definition. It deserves a serious referee because the ideas are concrete and the problem is relevant. I would recommend sending it to peer review, suggesting that reviewers pay particular attention to the correctness of the query reuse mechanism.

Referee Report

2 major / 1 minor

Summary. The paper introduces FaVeX, an algorithm for faster computation of verified explanations for neural networks. It combines dynamic batch and sequential feature processing with reuse of prior verifier query results for proving feature invariances and searching for prediction-altering assignments. A new hierarchical definition of verifier-optimal robust explanations is proposed that explicitly incorporates verifier incompleteness. Experiments claim this enables meaningful formal explanations on networks with hundreds of thousands of non-linear activations.

Significance. If the reuse mechanism is shown to preserve soundness, FaVeX would meaningfully advance scalable verified explanations, a persistent bottleneck in formal methods for neural networks. The verifier-optimal definition's explicit factoring of incompleteness is a clear strength that avoids overclaiming robustness and provides a more realistic formal guarantee.

major comments (2)

[Section 3 (FaVeX algorithm and reuse mechanism)] The central scalability claim rests on reusing cached bounds and partial assignments across verifier queries for both invariance proofs and counterexample search, yet no invariant, lemma, or inductive argument is supplied establishing that this reuse preserves soundness of the resulting verifier-optimal robust explanations (i.e., introduces neither false positives nor missed counterexamples). This is load-bearing for the reported results on networks with hundreds of thousands of activations.
[Section 5 (Experimental evaluation)] The experimental evaluation reports superior scalability but provides insufficient detail on baseline verifiers, exact network sizes and architectures, number of runs, or statistical controls, making it difficult to assess whether the observed speedups are robust or attributable to the proposed reuse and batch-sequential strategy.

minor comments (1)

[Section 2 (Preliminaries and definitions)] Notation for the hierarchical levels of verifier-optimal explanations could be clarified with an explicit example or small illustrative network to distinguish the new definition from prior robust explanation notions.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their constructive and insightful comments on our manuscript. We address each major comment in detail below and describe the revisions we intend to make.

read point-by-point responses

Referee: [Section 3 (FaVeX algorithm and reuse mechanism)] The central scalability claim rests on reusing cached bounds and partial assignments across verifier queries for both invariance proofs and counterexample search, yet no invariant, lemma, or inductive argument is supplied establishing that this reuse preserves soundness of the resulting verifier-optimal robust explanations (i.e., introduces neither false positives nor missed counterexamples). This is load-bearing for the reported results on networks with hundreds of thousands of activations.

Authors: We agree that a formal argument establishing the soundness of the reuse mechanism is necessary to support the central claims. Section 3 describes the dynamic batch-sequential processing and the reuse of cached bounds and partial assignments for invariance proofs and counterexample search, but does not include an explicit lemma or inductive invariant. In the revised manuscript we will add a new lemma (with proof) in Section 3 that shows the reuse operations preserve the soundness of the verifier-optimal robust explanations, ensuring neither false positives nor missed counterexamples are introduced. revision: yes
Referee: [Section 5 (Experimental evaluation)] The experimental evaluation reports superior scalability but provides insufficient detail on baseline verifiers, exact network sizes and architectures, number of runs, or statistical controls, making it difficult to assess whether the observed speedups are robust or attributable to the proposed reuse and batch-sequential strategy.

Authors: We acknowledge that additional experimental details are required for reproducibility and to substantiate the reported speedups. In the revised Section 5 we will expand the description to specify the exact baseline verifiers and their configurations, provide precise network architectures (number of layers, neurons, and non-linear activations), state the number of independent runs performed for each experiment, and include statistical measures such as standard deviations or confidence intervals. revision: yes

Circularity Check

0 steps flagged

No circularity in algorithmic design or new definition

full rationale

The paper presents FaVeX as a novel algorithm combining batch and sequential feature processing with reuse of prior verifier query results, plus a hierarchical verifier-optimal robust explanations definition that factors in verifier incompleteness. These are constructive algorithmic and definitional contributions evaluated experimentally on large networks. No equations, derivations, or claims in the abstract or described content reduce any result to fitted parameters, self-definitions, or load-bearing self-citations by construction. The work is self-contained as a practical acceleration technique without tautological reductions.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The paper rests on standard assumptions about neural network verifiers being sound but incomplete; no free parameters are fitted and no new physical or mathematical entities are postulated beyond the algorithmic technique and definition.

axioms (1)

domain assumption Neural network verifiers are sound but incomplete
Invoked when defining verifier-optimal robust explanations that factor in incompleteness.

invented entities (1)

verifier-optimal robust explanations no independent evidence
purpose: Hierarchical definition that explicitly accounts for verifier incompleteness
New concept introduced to make explanations robust to verifier limits.

pith-pipeline@v0.9.0 · 5453 in / 1254 out tokens · 50229 ms · 2026-05-17T03:27:28.694246+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean (AbsoluteFloorWitness) reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

verifier-optimal robust explanations... explicitly factors the incompleteness of network verifiers within the explanation

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

37 extracted references · 37 canonical work pages · 4 internal anchors

[2]

2 Ross Anderson, Joey Huchette, Will Ma, Christian Tjandraatmadja, and Juan Pablo Vielma

URL: https://arxiv.org/abs/2109.10317. 2 Ross Anderson, Joey Huchette, Will Ma, Christian Tjandraatmadja, and Juan Pablo Vielma. Strong mixed-integer programming formulations for trained neural networks.Math. Program., 183(1):3–39,

work page arXiv
[3]

On the reasons behind decisions

8 Adnan Darwiche and Auguste Hirth. On the reasons behind decisions. In Giuseppe De Giacomo, Alejandro Catalá, Bistra Dilkina, Michela Milano, Senén Barro, Alberto Bugarín, and Jérôme Lang, editors,ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020 - Inc...

work page 2020
[5]

URL: https://arxiv.org/abs/2104.06718,arXiv:2104.06718. A. De Palma and G. Dolcetti and C. Urban 23 12 Alessandro De Palma, Rudy Bunel, Krishnamurthy (Dj) Dvijotham, M. Pawan Kumar, Robert Stanforth, and Alessio Lomuscio. Expressive losses for verified robustness via convex combinations. InThe Twelfth International Conference on Learning Representations, ...

work page arXiv 2024
[6]

Towards A Rigorous Science of Interpretable Machine Learning

14 Finale Doshi-Velez and Been Kim. Towards a rigorous science of interpretable machine learning. arXiv preprint arXiv:1702.08608,

work page internal anchor Pith review Pith/arXiv arXiv
[7]

17 Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin T. Vechev. AI2: safety and robustness certification of neural networks with abstract interpretation. In2018 IEEE Symposium on Security and Privacy, SP 2018, Proceedings, 21-23 May 2018, San Francisco, California, USA, pages 3–18. IEEE Computer Society,

work page 2018
[8]

Scalable verified training for provably robust image classification

18 Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timothy Arthur Mann, and Pushmeet Kohli. Scalable verified training for provably robust image classification. In2019 IEEE/CVF International Conference on Computer Vision, ICCV 2019, Seoul, Korea (South), October 27 - November 2, 2019, pa...

work page 2019
[9]

A survey of methods for explaining black box models.ACM Comput

19 Riccardo Guidotti, Anna Monreale, Salvatore Ruggieri, Franco Turini, Fosca Giannotti, and Dino Pedreschi. A survey of methods for explaining black box models.ACM Comput. Surv., 51(5):93:1–93:42, 2019.doi:10.1145/3236009. 20 Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual. URL: https://www.gurobi. com. 21 Faisal Hamman, Erfaun Noorani, Saumi...

work page doi:10.1145/3236009 2019
[10]

Interpretation of Prediction Models Using the Input Gradient

URL: http://arxiv.org/abs/1611.07634. 23 Fred Hemery, Christophe Lecoutre, Lakhdar Sais, and Frédéric Boussemart. Extracting mucs from constraint networks. In Gerhard Brewka, Silvia Coradeschi, Anna Perini, and Paolo Traverso, editors,ECAI 2006, 17th European Conference on Artificial Intelligence, August 29 - September 1, 2006, Riva del Garda, Italy, Incl...

work page internal anchor Pith review Pith/arXiv arXiv 2006
[11]

DEEPSPLIT: an efficient splitting method for neural network verification via indirect effect analysis

24 Patrick Henriksen and Alessio Lomuscio. DEEPSPLIT: an efficient splitting method for neural network verification via indirect effect analysis. In Zhi-Hua Zhou, editor,Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021, pages 2549–2555. ijcai.org,

work page 2021
[12]

Abduction-based explanations for machine learning models

26 Alexey Ignatiev, Nina Narodytska, and João Marques-Silva. Abduction-based explanations for machine learning models. InThe Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, The Thirty-First Innovative Applications of Artificial Intelligence Conference, IAAI 2019, The Ninth AAAI Symposium on Educational Advances in Artificial Intelligen...

work page 2019
[13]

On relating explanations and adversarial examples

27 Alexey Ignatiev, Nina Narodytska, and João Marques-Silva. On relating explanations and adversarial examples. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d’Alché-Buc, Emily B. Fox, and Roman Garnett, editors,Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIP...

work page 2019
[14]

Distance-restricted explanations: Theoretical underpinnings & efficient imple- mentation

28 Yacine Izza, Xuanxiang Huang, António Morgado, Jordi Planes, Alexey Ignatiev, and João Marques-Silva. Distance-restricted explanations: Theoretical underpinnings & efficient imple- mentation. In Pierre Marquis, Magdalena Ortiz, and Maurice Pagnucco, editors,Proceedings of the 21st International Conference on Principles of Knowledge Representation and R...

work page 2024
[15]

30 Junqi Jiang, Francesco Leofante, Antonio Rago, and Francesca Toni

URL: https://proceedings.mlr.press/v222/jiang24a.html. 30 Junqi Jiang, Francesco Leofante, Antonio Rago, and Francesca Toni. Robust counterfactual explanations in machine learning: A survey.CoRR, abs/2402.01928,

work page arXiv
[16]

30 Junqi Jiang, Francesco Leofante, Antonio Rago, and Francesca Toni

URL: https: //doi.org/10.48550/arXiv.2402.01928,doi:10.48550/ARXIV.2402.01928. 31 Ulrich Junker. QUICKXPLAIN: preferred explanations and relaxations for over-constrained problems. In Deborah L. McGuinness and George Ferguson, editors,Proceedings of the Nineteenth National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applicatio...

work page doi:10.48550/arxiv.2402.01928 2004
[17]

Barrett, David L

32 Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In Rupak Majumdar and Viktor Kuncak, editors,Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, volume 10426 ofLecture No...

work page doi:10.1007/978-3-319-63387-9 2017
[18]

Zbrzezny, Nicola Paoletti, and Marta Kwiatkowska

34 Emanuele La Malfa, Rhiannon Michelmore, Agnieszka M. Zbrzezny, Nicola Paoletti, and Marta Kwiatkowska. On guaranteed optimal robust explanations for NLP models. In Zhi-Hua Zhou, editor,Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021, pages 2658–2665....

work page 2021
[19]

Promoting counterfactual robustness through diversity

36 Francesco Leofante and Nico Potyka. Promoting counterfactual robustness through diversity. InProceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence and Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence and Fourteenth Symposium on Educational Advances in Artificial Intelligence, AAAI’24/IAAI’24/EAAI’24. A...

work page doi:10.1609/aaai.v38i19.30127 2024
[20]

An approach to reachability analysis for feed-forward ReLU neural networks

38 Alessio Lomuscio and Lalit Maganti. An approach to reachability analysis for feed-forward relu neural networks.arXiv preprint arXiv:1706.07351,

work page internal anchor Pith review Pith/arXiv arXiv
[21]

De Palma and G

A. De Palma and G. Dolcetti and C. Urban 25 39 Scott M. Lundberg and Su-In Lee. A unified approach to interpreting model predictions. InAdvances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, pages 4765–4774,

work page 2017
[22]

Logic-based explainability in machine learning

42 João Marques-Silva. Logic-based explainability in machine learning. In Leopoldo E. Bertossi and Guohui Xiao, editors,Reasoning Web. Causality, Explanations and Declarative Knowledge - 18th International Summer School 2022, Berlin, Germany, September 27-30, 2022, Tutorial Lectures, volume 13759 ofLecture Notes in Computer Science, pages 24–104. Springer,

work page 2022
[23]

Logic-based explainability: Past, present and future

43 João Marques-Silva. Logic-based explainability: Past, present and future. In Tiziana Margaria and Bernhard Steffen, editors,Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodologies - 12th International Symposium, ISoLA 2024, Crete, Greece, October 27-31, 2024, Proceedings, Part IV, volume 15222 ofLectur...

work page 2024
[24]

Delivering trustworthy AI through formal XAI

45João Marques-Silva and Alexey Ignatiev. Delivering trustworthy AI through formal XAI. In Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference on Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022 Virtual Event, Februar...

work page 2022
[25]

Why should I trust you?

49 Marco Túlio Ribeiro, Sameer Singh, and Carlos Guestrin. “Why should I trust you?”: Explaining the predictions of any classifier. InProceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, 2016, pages 1135–1144. ACM,

work page 2016
[26]

A symbolic approach to explaining bayesian network classifiers

52 Andy Shih, Arthur Choi, and Adnan Darwiche. A symbolic approach to explaining bayesian network classifiers. In Jérôme Lang, editor,Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden, pages 5103–5111. ijcai.org,

work page 2018
[27]

Deep Inside Convolutional Networks: Visualising Image Classification Models and Saliency Maps

URL: https://doi.org/10.24963/ijcai.2018/708, doi:10. 24963/IJCAI.2018/708. 26 Faster Verified Explanations for Neural Networks 53 Karen Simonyan, Andrea Vedaldi, and Andrew Zisserman. Deep inside convolutional networks: Visualising image classification models and saliency maps.arXiv preprint arXiv:1312.6034,

work page internal anchor Pith review Pith/arXiv arXiv doi:10.24963/ijcai.2018/708 2018
[28]

54 Gagandeep Singh, Rupanshu Ganvir, Markus Püschel, and Martin T. Vechev. Beyond the single neuron convex barrier for neural network certification. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d’Alché-Buc, Emily B. Fox, and Roman Garnett, editors,Advances in Neural Information Processing Systems 32: Annual Conference on Neural Inform...

work page 2019
[29]

55 Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin T. Vechev. Fast and effective robustness certification. In Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi, and Roman Garnett, editors,Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Syste...

work page 2018
[30]

Evaluating robustness of neural networks with mixed integer programming

58 Vincent Tjeng, Kai Yuanqing Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9,

work page 2019
[31]

59 Shubham Ugare, Debangshu Banerjee, Sasa Misailovic, and Gagandeep Singh

URL: https://openreview.net/forum?id=HyGIdiRqtm. 59 Shubham Ugare, Debangshu Banerjee, Sasa Misailovic, and Gagandeep Singh. Incremental verification of neural networks.Proc. ACM Program. Lang., 7(PLDI):1920–1945, 2023.doi: 10.1145/3591299. 60 Caterina Urban and Antoine Miné. A review of formal methods applied to machine learning. CoRR, abs/2104.02466,

work page doi:10.1145/3591299 1920
[32]

61 Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana

URL: https://arxiv.org/abs/2104.02466. 61 Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. In Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi, and Roman Garnett, editors,Advances in Neural Information Processing Systems 31: Annual Conference on...

work page arXiv 2018
[33]

Zico Kolter

62 Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J. Zico Kolter. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. In Marc’Aurelio Ranzato, Alina Beygelzimer, Yann N. Dauphin, Percy Liang, and Jennifer Wortman Vaughan, editors,Advances in Neural Information Pro...

work page 2021
[34]

64 Min Wu, Xiaofu Li, Haoze Wu, and Clark W. Barrett. Better verified explanations with applications to incorrectness and out-of-distribution detection.CoRR, abs/2409.03060,

work page arXiv
[35]

65 Min Wu, Haoze Wu, and Clark W

arXiv:2409.03060,doi:10.48550/ARXIV.2409.03060. 65 Min Wu, Haoze Wu, and Clark W. Barrett. Verix: Towards verified explainability of deep neural networks. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine, editors,Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processi...

work page doi:10.48550/arxiv.2409.03060 2023
[36]

Fast and complete: Enabling complete neural network verification with rapid and massively A

66 Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. Fast and complete: Enabling complete neural network verification with rapid and massively A. De Palma and G. Dolcetti and C. Urban 27 parallel incomplete verifiers. In9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7,

work page 2021
[37]

Efficient neural network robustness certification with general activation functions

68 Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi, and Roman Garnett, editors,Advances in Neural Information Processing Systems 31: Annual Conference on Neural...

work page 2018
[38]

Hanasusanto, and Huan Zhang

69 Duo Zhou, Christopher Brix, Grani A. Hanasusanto, and Huan Zhang. Scalable neural network verification with branch-and-bound inferred cutting planes. In Amir Globersons, Lester Mackey, Danielle Belgrave, Angela Fan, Ulrich Paquet, Jakub M. Tomczak, and Cheng Zhang, editors,Advances in Neural Information Processing Systems 38: Annual Conference on Neura...

work page 2024
[39]

Scalable neural network verification with branch-and-bound inferred cutting planes

70 Duo Zhou, Christopher Brix, Grani A Hanasusanto, and Huan Zhang. Scalable neural network verification with branch-and-bound inferred cutting planes. InNeural Information Processing Systems, pages 29324–29353, 2024

work page 2024

[1] [2]

2 Ross Anderson, Joey Huchette, Will Ma, Christian Tjandraatmadja, and Juan Pablo Vielma

URL: https://arxiv.org/abs/2109.10317. 2 Ross Anderson, Joey Huchette, Will Ma, Christian Tjandraatmadja, and Juan Pablo Vielma. Strong mixed-integer programming formulations for trained neural networks.Math. Program., 183(1):3–39,

work page arXiv

[2] [3]

On the reasons behind decisions

8 Adnan Darwiche and Auguste Hirth. On the reasons behind decisions. In Giuseppe De Giacomo, Alejandro Catalá, Bistra Dilkina, Michela Milano, Senén Barro, Alberto Bugarín, and Jérôme Lang, editors,ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020 - Inc...

work page 2020

[3] [5]

URL: https://arxiv.org/abs/2104.06718,arXiv:2104.06718. A. De Palma and G. Dolcetti and C. Urban 23 12 Alessandro De Palma, Rudy Bunel, Krishnamurthy (Dj) Dvijotham, M. Pawan Kumar, Robert Stanforth, and Alessio Lomuscio. Expressive losses for verified robustness via convex combinations. InThe Twelfth International Conference on Learning Representations, ...

work page arXiv 2024

[4] [6]

Towards A Rigorous Science of Interpretable Machine Learning

14 Finale Doshi-Velez and Been Kim. Towards a rigorous science of interpretable machine learning. arXiv preprint arXiv:1702.08608,

work page internal anchor Pith review Pith/arXiv arXiv

[5] [7]

17 Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin T. Vechev. AI2: safety and robustness certification of neural networks with abstract interpretation. In2018 IEEE Symposium on Security and Privacy, SP 2018, Proceedings, 21-23 May 2018, San Francisco, California, USA, pages 3–18. IEEE Computer Society,

work page 2018

[6] [8]

Scalable verified training for provably robust image classification

18 Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timothy Arthur Mann, and Pushmeet Kohli. Scalable verified training for provably robust image classification. In2019 IEEE/CVF International Conference on Computer Vision, ICCV 2019, Seoul, Korea (South), October 27 - November 2, 2019, pa...

work page 2019

[7] [9]

A survey of methods for explaining black box models.ACM Comput

19 Riccardo Guidotti, Anna Monreale, Salvatore Ruggieri, Franco Turini, Fosca Giannotti, and Dino Pedreschi. A survey of methods for explaining black box models.ACM Comput. Surv., 51(5):93:1–93:42, 2019.doi:10.1145/3236009. 20 Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual. URL: https://www.gurobi. com. 21 Faisal Hamman, Erfaun Noorani, Saumi...

work page doi:10.1145/3236009 2019

[8] [10]

Interpretation of Prediction Models Using the Input Gradient

URL: http://arxiv.org/abs/1611.07634. 23 Fred Hemery, Christophe Lecoutre, Lakhdar Sais, and Frédéric Boussemart. Extracting mucs from constraint networks. In Gerhard Brewka, Silvia Coradeschi, Anna Perini, and Paolo Traverso, editors,ECAI 2006, 17th European Conference on Artificial Intelligence, August 29 - September 1, 2006, Riva del Garda, Italy, Incl...

work page internal anchor Pith review Pith/arXiv arXiv 2006

[9] [11]

DEEPSPLIT: an efficient splitting method for neural network verification via indirect effect analysis

24 Patrick Henriksen and Alessio Lomuscio. DEEPSPLIT: an efficient splitting method for neural network verification via indirect effect analysis. In Zhi-Hua Zhou, editor,Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021, pages 2549–2555. ijcai.org,

work page 2021

[10] [12]

Abduction-based explanations for machine learning models

26 Alexey Ignatiev, Nina Narodytska, and João Marques-Silva. Abduction-based explanations for machine learning models. InThe Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, The Thirty-First Innovative Applications of Artificial Intelligence Conference, IAAI 2019, The Ninth AAAI Symposium on Educational Advances in Artificial Intelligen...

work page 2019

[11] [13]

On relating explanations and adversarial examples

27 Alexey Ignatiev, Nina Narodytska, and João Marques-Silva. On relating explanations and adversarial examples. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d’Alché-Buc, Emily B. Fox, and Roman Garnett, editors,Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIP...

work page 2019

[12] [14]

Distance-restricted explanations: Theoretical underpinnings & efficient imple- mentation

28 Yacine Izza, Xuanxiang Huang, António Morgado, Jordi Planes, Alexey Ignatiev, and João Marques-Silva. Distance-restricted explanations: Theoretical underpinnings & efficient imple- mentation. In Pierre Marquis, Magdalena Ortiz, and Maurice Pagnucco, editors,Proceedings of the 21st International Conference on Principles of Knowledge Representation and R...

work page 2024

[13] [15]

30 Junqi Jiang, Francesco Leofante, Antonio Rago, and Francesca Toni

URL: https://proceedings.mlr.press/v222/jiang24a.html. 30 Junqi Jiang, Francesco Leofante, Antonio Rago, and Francesca Toni. Robust counterfactual explanations in machine learning: A survey.CoRR, abs/2402.01928,

work page arXiv

[14] [16]

30 Junqi Jiang, Francesco Leofante, Antonio Rago, and Francesca Toni

URL: https: //doi.org/10.48550/arXiv.2402.01928,doi:10.48550/ARXIV.2402.01928. 31 Ulrich Junker. QUICKXPLAIN: preferred explanations and relaxations for over-constrained problems. In Deborah L. McGuinness and George Ferguson, editors,Proceedings of the Nineteenth National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applicatio...

work page doi:10.48550/arxiv.2402.01928 2004

[15] [17]

Barrett, David L

32 Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In Rupak Majumdar and Viktor Kuncak, editors,Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, volume 10426 ofLecture No...

work page doi:10.1007/978-3-319-63387-9 2017

[16] [18]

Zbrzezny, Nicola Paoletti, and Marta Kwiatkowska

34 Emanuele La Malfa, Rhiannon Michelmore, Agnieszka M. Zbrzezny, Nicola Paoletti, and Marta Kwiatkowska. On guaranteed optimal robust explanations for NLP models. In Zhi-Hua Zhou, editor,Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021, pages 2658–2665....

work page 2021

[17] [19]

Promoting counterfactual robustness through diversity

36 Francesco Leofante and Nico Potyka. Promoting counterfactual robustness through diversity. InProceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence and Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence and Fourteenth Symposium on Educational Advances in Artificial Intelligence, AAAI’24/IAAI’24/EAAI’24. A...

work page doi:10.1609/aaai.v38i19.30127 2024

[18] [20]

An approach to reachability analysis for feed-forward ReLU neural networks

38 Alessio Lomuscio and Lalit Maganti. An approach to reachability analysis for feed-forward relu neural networks.arXiv preprint arXiv:1706.07351,

work page internal anchor Pith review Pith/arXiv arXiv

[19] [21]

De Palma and G

A. De Palma and G. Dolcetti and C. Urban 25 39 Scott M. Lundberg and Su-In Lee. A unified approach to interpreting model predictions. InAdvances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, pages 4765–4774,

work page 2017

[20] [22]

Logic-based explainability in machine learning

42 João Marques-Silva. Logic-based explainability in machine learning. In Leopoldo E. Bertossi and Guohui Xiao, editors,Reasoning Web. Causality, Explanations and Declarative Knowledge - 18th International Summer School 2022, Berlin, Germany, September 27-30, 2022, Tutorial Lectures, volume 13759 ofLecture Notes in Computer Science, pages 24–104. Springer,

work page 2022

[21] [23]

Logic-based explainability: Past, present and future

43 João Marques-Silva. Logic-based explainability: Past, present and future. In Tiziana Margaria and Bernhard Steffen, editors,Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodologies - 12th International Symposium, ISoLA 2024, Crete, Greece, October 27-31, 2024, Proceedings, Part IV, volume 15222 ofLectur...

work page 2024

[22] [24]

Delivering trustworthy AI through formal XAI

45João Marques-Silva and Alexey Ignatiev. Delivering trustworthy AI through formal XAI. In Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference on Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022 Virtual Event, Februar...

work page 2022

[23] [25]

Why should I trust you?

49 Marco Túlio Ribeiro, Sameer Singh, and Carlos Guestrin. “Why should I trust you?”: Explaining the predictions of any classifier. InProceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, 2016, pages 1135–1144. ACM,

work page 2016

[24] [26]

A symbolic approach to explaining bayesian network classifiers

52 Andy Shih, Arthur Choi, and Adnan Darwiche. A symbolic approach to explaining bayesian network classifiers. In Jérôme Lang, editor,Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden, pages 5103–5111. ijcai.org,

work page 2018

[25] [27]

Deep Inside Convolutional Networks: Visualising Image Classification Models and Saliency Maps

URL: https://doi.org/10.24963/ijcai.2018/708, doi:10. 24963/IJCAI.2018/708. 26 Faster Verified Explanations for Neural Networks 53 Karen Simonyan, Andrea Vedaldi, and Andrew Zisserman. Deep inside convolutional networks: Visualising image classification models and saliency maps.arXiv preprint arXiv:1312.6034,

work page internal anchor Pith review Pith/arXiv arXiv doi:10.24963/ijcai.2018/708 2018

[26] [28]

54 Gagandeep Singh, Rupanshu Ganvir, Markus Püschel, and Martin T. Vechev. Beyond the single neuron convex barrier for neural network certification. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d’Alché-Buc, Emily B. Fox, and Roman Garnett, editors,Advances in Neural Information Processing Systems 32: Annual Conference on Neural Inform...

work page 2019

[27] [29]

55 Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin T. Vechev. Fast and effective robustness certification. In Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi, and Roman Garnett, editors,Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Syste...

work page 2018

[28] [30]

Evaluating robustness of neural networks with mixed integer programming

58 Vincent Tjeng, Kai Yuanqing Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9,

work page 2019

[29] [31]

59 Shubham Ugare, Debangshu Banerjee, Sasa Misailovic, and Gagandeep Singh

URL: https://openreview.net/forum?id=HyGIdiRqtm. 59 Shubham Ugare, Debangshu Banerjee, Sasa Misailovic, and Gagandeep Singh. Incremental verification of neural networks.Proc. ACM Program. Lang., 7(PLDI):1920–1945, 2023.doi: 10.1145/3591299. 60 Caterina Urban and Antoine Miné. A review of formal methods applied to machine learning. CoRR, abs/2104.02466,

work page doi:10.1145/3591299 1920

[30] [32]

61 Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana

URL: https://arxiv.org/abs/2104.02466. 61 Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. In Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi, and Roman Garnett, editors,Advances in Neural Information Processing Systems 31: Annual Conference on...

work page arXiv 2018

[31] [33]

Zico Kolter

62 Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J. Zico Kolter. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. In Marc’Aurelio Ranzato, Alina Beygelzimer, Yann N. Dauphin, Percy Liang, and Jennifer Wortman Vaughan, editors,Advances in Neural Information Pro...

work page 2021

[32] [34]

64 Min Wu, Xiaofu Li, Haoze Wu, and Clark W. Barrett. Better verified explanations with applications to incorrectness and out-of-distribution detection.CoRR, abs/2409.03060,

work page arXiv

[33] [35]

65 Min Wu, Haoze Wu, and Clark W

arXiv:2409.03060,doi:10.48550/ARXIV.2409.03060. 65 Min Wu, Haoze Wu, and Clark W. Barrett. Verix: Towards verified explainability of deep neural networks. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine, editors,Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processi...

work page doi:10.48550/arxiv.2409.03060 2023

[34] [36]

Fast and complete: Enabling complete neural network verification with rapid and massively A

66 Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. Fast and complete: Enabling complete neural network verification with rapid and massively A. De Palma and G. Dolcetti and C. Urban 27 parallel incomplete verifiers. In9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7,

work page 2021

[35] [37]

Efficient neural network robustness certification with general activation functions

68 Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi, and Roman Garnett, editors,Advances in Neural Information Processing Systems 31: Annual Conference on Neural...

work page 2018

[36] [38]

Hanasusanto, and Huan Zhang

69 Duo Zhou, Christopher Brix, Grani A. Hanasusanto, and Huan Zhang. Scalable neural network verification with branch-and-bound inferred cutting planes. In Amir Globersons, Lester Mackey, Danielle Belgrave, Angela Fan, Ulrich Paquet, Jakub M. Tomczak, and Cheng Zhang, editors,Advances in Neural Information Processing Systems 38: Annual Conference on Neura...

work page 2024

[37] [39]

Scalable neural network verification with branch-and-bound inferred cutting planes

70 Duo Zhou, Christopher Brix, Grani A Hanasusanto, and Huan Zhang. Scalable neural network verification with branch-and-bound inferred cutting planes. InNeural Information Processing Systems, pages 29324–29353, 2024

work page 2024