{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T21:14:41Z","timestamp":1783545281489,"version":"3.55.0"},"reference-count":0,"publisher":"AI Access Foundation","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["jair"],"abstract":"<jats:p>As deep neural networks are deployed in safety-critical domains such as autonomous driving and medical diagnosis, stakeholders need explanations of model behavior that are not only interpretable but also trustworthy with formal guarantees. Existing XAI methods fall short of this requirement: heuristic attribution techniques (e.g., LIME, Integrated Gradients) highlight influential features for individual predictions but offer no mathematical guarantees about decision boundaries, while formal explanation methods verify robustness properties yet remain untargeted, analyzing the nearest boundary regardless of whether it represents a critical risk. In safety-critical systems, however, not all misclassifications carry equal consequences; confusing a \u201cStop\u201d sign for a \u201c60 kph\u201d sign is far more dangerous than confusing it with a \u201cNo Passing\u201d sign.\u00a0 Practitioners therefore lack a principled way to answer a fundamental safety question: how resilient is a model\u2019s classification against a specific, high-risk alternative?\u00a0 We introduce ViTaX (Verified and Targeted Explanations), a formal XAI framework that addresses this gap by generating targeted semifactual explanations with mathematical guarantees.\u00a0 For a given input (class y) and a user-specified critical alternative (class t), ViTaX performs two key steps: (1) it identifies the minimal feature subset most sensitive to the y \u2192\u00a0t transition using class-specific sensitivity heuristics, and (2) it applies formal reachability analysis to guarantee that perturbing these features by \u03b5 is insufficient to flip the classification to t. This guarantee constitutes a verified semifactual: \u201ceven if these critical features change by \u03b5 classification y persists against t.\" We formalize this reasoning through Targeted \u03b5-Robustness, a formal property that certifies whether an identified feature subset remains robust under perturbation toward a specific target class. By unifying semifactual explanations, class-specific targeting, and formal verification, ViTaX is the first method to provide formally guaranteed explanations of a model\u2019s resilience against specific, user-identified alternatives. Our evaluations on image classification (MNIST, GTSRB, EMNIST) and regression (TaxiNet) demonstrate that ViTaX achieves significantly higher fidelity (e.g., over 30% improvement) and minimal explanation cardinality compared to existing methods. These results establish ViTaX as a scalable and trustworthy foundation for verifiable, targeted XAI.<\/jats:p>","DOI":"10.1613\/jair.1.20924","type":"journal-article","created":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T20:20:42Z","timestamp":1783542042000},"source":"Crossref","is-referenced-by-count":0,"title":["Towards Verified and Targeted Explanations through Formal Methods"],"prefix":"10.1613","volume":"86","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5990-5865","authenticated-orcid":false,"given":"Hanchen David","family":"Wang","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0721-1241","authenticated-orcid":false,"given":"Diego","family":"Lopez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4906-2179","authenticated-orcid":false,"given":"Preston","family":"Robinette","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1403-2420","authenticated-orcid":false,"given":"Ipek","family":"Oguz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8021-9923","authenticated-orcid":false,"given":"Taylor","family":"Johnson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6916-8774","authenticated-orcid":false,"given":"Meiyi","family":"Ma","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"16860","published-online":{"date-parts":[[2026,7,8]]},"container-title":["Journal of Artificial Intelligence Research"],"original-title":[],"link":[{"URL":"https:\/\/www.jair.org\/index.php\/jair\/article\/download\/20924\/27323","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.jair.org\/index.php\/jair\/article\/download\/20924\/27323","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T20:20:43Z","timestamp":1783542043000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jair.org\/index.php\/jair\/article\/view\/20924"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7,8]]},"references-count":0,"URL":"https:\/\/doi.org\/10.1613\/jair.1.20924","relation":{},"ISSN":["1076-9757"],"issn-type":[{"value":"1076-9757","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,7,8]]}}}