Interpreting Robustness Proofs of Deep Neural Networks
In recent years numerous methods have been developed to formally verify the robustness of deep neural networks (DNNs). Though the proposed techniques are effective in providing mathematical guarantees about the DNNs behavior, it is not clear whether the proofs generated by these methods are human-interpretable. In this paper, we bridge this gap by developing new concepts, algorithms, and representations to generate human understandable interpretations of the proofs. Leveraging the proposed method, we show that the robustness proofs of standard DNNs rely on spurious input features, while the proofs of DNNs trained to be provably robust filter out even the semantically meaningful features. The proofs for the DNNs combining adversarial and provably robust training are the most effective at selectively filtering out spurious features as well as relying on human-understandable input features.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
ProoFVer: Natural Logic Theorem Proving for Fact Verification
Fact verification systems typically rely on neural network classifiers for veracity prediction which lack explainability. This paper proposes ProoFVer, which uses a seq2seq model to generate natural logic-based inference…
Automated Theorem ProvingcounterfactualDecision MakingFact Verification+1Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code
In the realm of formal theorem proving, the Coq proof assistant stands out for its rigorous approach to verifying mathematical assertions and software correctness. Despite the advances in artificial intelligence and mach…
Automated Theorem ProvingCode GenerationLEMMAvalidLearning Axioms to Compute Verifiable Symbolic Expression Equivalence Proofs Using Graph-to-Sequence Networks
We target the problem of proving the semantic equivalence between two complex expressions represented as typed trees, and demonstrate our system on expressions from a rich multi-type symbolic language for linear algebra.…
Graph-to-SequencePhilosophy-Guided Mathematical Formalism for Complex Systems Modelling
We recently presented the so-called allagmatic method, which includes a system metamodel providing a framework for describing, modelling, simulating, and interpreting complex systems. Its development and programming was …
PhilosophyCertified Interpretability Robustness for Class Activation Mapping
Interpreting machine learning models is challenging but crucial for ensuring the safety of deep networks in autonomous driving systems. Due to the prevalence of deep learning based perception models in autonomous vehicle…
Autonomous DrivingAutonomous Vehicles