# Formal Local Implication Between Two Neural Networks

arXiv: https://arxiv.org/abs/2409.16726 · HTML: https://mlsanity.com/paper/2409.16726/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 14 of its 27 references that are in the map.
- First posted on arXiv 25 Sep 2024.

## Builds on (most cited first, 14 of 14)

- [Distilling the Knowledge in a Neural Network](https://mlsanity.com/paper/1503.02531/) (2015)
- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Certified Defenses for Adversarial Patches](https://mlsanity.com/paper/2003.06693/) (2020)
- [Verifying Properties of Binarized Deep Neural Networks](https://mlsanity.com/paper/1709.06662/) (2017)
- [ReluDiff: Differential Verification of Deep Neural Networks](https://mlsanity.com/paper/2001.03662/) (2020)
- [On the Effect of Pruning on Adversarial Robustness](https://mlsanity.com/paper/2108.04890/) (2021)
- [NeuroDiff: Scalable Differential Verification of Neural Networks using Fine-Grained Approximation](https://mlsanity.com/paper/2009.09943/) (2020)
- [Can pruning improve certified robustness of neural networks?](https://mlsanity.com/paper/2206.07311/) (2022)
- [On Neural Network Equivalence Checking using SMT Solvers](https://mlsanity.com/paper/2203.11629/) (2022)
- [VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees](https://mlsanity.com/paper/2312.09748/) (2023)

## Abstract (arXiv)

Given two neural network classifiers with the same input and output domains, our goal is to compare the two networks in relation to each other over an entire input region (e.g., within a vicinity of an input sample). To this end, we establish the foundation of formal local implication between two networks, i.e., N2 implies N1, in an entire input region D. That is, network N1 consistently makes a correct decision every time network N2 does, and it does so in an entire input region D. We further propose a sound formulation for establishing such formally-verified (provably correct) local implications. The proposed formulation is relevant in the context of several application domains, e.g., for comparing a trained network and its corresponding compact (e.g., pruned, quantized, distilled) networks. We evaluate our formulation based on the MNIST, CIFAR10, and two real-world medical datasets, to show its relevance.