























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.
| Comments: | ECOOP 2026 |
| Subjects: | Machine Learning (cs.LG); Programming Languages (cs.PL) |
| Cite as: | arXiv:2512.00164 [cs.LG] |
| (or arXiv:2512.00164v2 [cs.LG] for this version) | |
| https://doi.org/10.48550/arXiv.2512.00164 arXiv-issued DOI via DataCite |
From: Alessandro De Palma [view email]
[v1]
Fri, 28 Nov 2025 19:05:39 UTC (254 KB)
[v2]
Fri, 8 May 2026 11:21:01 UTC (343 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理,仅供阅读参考。 原文来自 — 版权归原作者所有。