AI2030 Responsible AI Tools Marketplace

Key Takeaways

Existing explanation methods lack safety guarantees: Current popular XAI techniques like LIME and Integrated Gradients can identify which features influence a model's decision, but they provide no mathematical proof that the model will behave safely—a critical gap for high-stakes applications like autonomous vehicles and medical diagnosis.
Not all AI errors are equally dangerous: The paper highlights that confusing a "Stop" sign for a "60 kph" sign poses far greater risk than confusing it with a "No Passing" sign. ViTaX addresses this by allowing stakeholders to specify which misclassifications matter most, rather than treating all errors the same way.
ViTaX provides formal guarantees about specific risks: Unlike previous methods, ViTaX identifies the minimal set of features most likely to cause a specific dangerous misclassification (e.g., Stop→60 kph) and mathematically proves that small perturbations to those features won't trigger that particular failure mode.
Formal methods can be made practical for real-world AI: By combining formal verification with targeted explanations, ViTaX demonstrates that mathematical guarantees—traditionally limited to small, simple systems—can now address realistic deep neural network safety concerns in critical domains.
Stakeholder input improves AI safety verification: The framework's ability to incorporate user-specified "critical alternatives" means domain experts (engineers, doctors, regulators) can guide verification toward the failure modes that matter most in their specific context, rather than relying on generic robustness measures.

Abstract

As deep neural networks are deployed in safety-critical domains such as autonomous driving and medical diagnosis, stakeholders need explanations that are interpretable but also trustworthy with formal guarantees. Existing XAI methods fall short: heuristic attribution techniques (e.g., LIME, Integrated Gradients) highlight influential features but offer no mathematical guarantees about decision boundaries, while formal methods verify robustness yet remain untargeted, analyzing the nearest boundary regardless of whether it represents a critical risk. In safety-critical systems, not all misclassifications carry equal consequences; confusing a "Stop" sign for a "60 kph" sign is far more dangerous than confusing it with a "No Passing" sign. We introduce ViTaX (Verified and Targeted Explanations), a formal XAI framework that generates targeted semifactual explanations with mathematical guarantees. For a given input (class y) and a user-specified critical alternative (class t), ViTaX: (1) identifies the minimal feature subset most sensitive to the y->t transition, and (2) applies formal reachability analysis to guarantee that perturbing these features by epsilon cannot flip the classification to t. We formalize this through Targeted epsilon-Robustness, certifying whether a feature subset remains robust under perturbation toward a specific target class. ViTaX is the first method to provide formally guaranteed explanations of a model's resilience against user-identified alternatives. Evaluations on MNIST, GTSRB, EMNIST, and TaxiNet demonstrate over 30% fidelity improvement with minimal explanation cardinality.

Paper has been accepted at JAIR

Key Takeaways

Existing explanation methods lack safety guarantees: Current popular XAI techniques like LIME and Integrated Gradients can identify which features influence a model's decision, but they provide no mathematical proof that the model will behave safely—a critical gap for high-stakes applications like autonomous vehicles and medical diagnosis.
Not all AI errors are equally dangerous: The paper highlights that confusing a "Stop" sign for a "60 kph" sign poses far greater risk than confusing it with a "No Passing" sign. ViTaX addresses this by allowing stakeholders to specify which misclassifications matter most, rather than treating all errors the same way.
ViTaX provides formal guarantees about specific risks: Unlike previous methods, ViTaX identifies the minimal set of features most likely to cause a specific dangerous misclassification (e.g., Stop→60 kph) and mathematically proves that small perturbations to those features won't trigger that particular failure mode.
Formal methods can be made practical for real-world AI: By combining formal verification with targeted explanations, ViTaX demonstrates that mathematical guarantees—traditionally limited to small, simple systems—can now address realistic deep neural network safety concerns in critical domains.
Stakeholder input improves AI safety verification: The framework's ability to incorporate user-specified "critical alternatives" means domain experts (engineers, doctors, regulators) can guide verification toward the failure modes that matter most in their specific context, rather than relying on generic robustness measures.

Abstract

Paper has been accepted at JAIR

Towards Verified and Targeted Explanations through Formal Methods

Key Takeaways

Abstract

Paper Info

Responsible AI Topics

Links

Towards Verified and Targeted Explanations through Formal Methods

Key Takeaways

Abstract

Paper Info

Responsible AI Topics

Links