Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Formal Local Implication Between Two Neural Networks

Baninajjar, Anahita LU orcid ; Rezine, Ahmed and Aminifar, Amir LU orcid (2025)
Abstract
Given two neural network classifiers with the same in-
put 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
D=⇒ 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 implica-
tions. The proposed formulation is relevant in the context of several
application domains, e.g., for comparing... (More)
Given two neural network classifiers with the same in-
put 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
D=⇒ 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 implica-
tions. 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 (Less)
Please use this url to cite or link to this publication:
author
; and
organization
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
in press
subject
host publication
European Conference on Artificial Intelligence (ECAI)
pages
9 pages
language
English
LU publication?
yes
id
263d33a6-4271-46de-91af-97551a4bd864
date added to LUP
2025-09-04 23:46:24
date last changed
2025-09-11 11:46:42
@inproceedings{263d33a6-4271-46de-91af-97551a4bd864,
  abstract     = {{Given two neural network classifiers with the same in-<br/>put and output domains, our goal is to compare the two networks<br/>in relation to each other over an entire input region (e.g., within a<br/>vicinity of an input sample). To this end, we establish the foundation<br/>of formal local implication between two networks, i.e., N2<br/>D=⇒ N1, in an entire input region D. That is, network N1 consistently makes<br/>a correct decision every time network N2 does, and it does so in an<br/>entire input region D. We further propose a sound formulation for<br/>establishing such formally-verified (provably correct) local implica-<br/>tions. The proposed formulation is relevant in the context of several<br/>application domains, e.g., for comparing a trained network and its<br/>corresponding compact (e.g., pruned, quantized, distilled) networks.<br/>We evaluate our formulation based on the MNIST, CIFAR10, and two<br/>real-world medical datasets, to show its relevance}},
  author       = {{Baninajjar, Anahita and Rezine, Ahmed and Aminifar, Amir}},
  booktitle    = {{European Conference on Artificial Intelligence (ECAI)}},
  language     = {{eng}},
  title        = {{Formal Local Implication Between Two Neural Networks}},
  url          = {{https://lup.lub.lu.se/search/files/227035490/FLI.pdf}},
  year         = {{2025}},
}