Experiments (Spexplain)

Benchmarks:
We run experiments on 5 different classification tasks in different domains with different input sizes:
  • Heart attack risk prediction: focuses on predicting the risk of heart attacks based on various medical indicators of patients, such as age, cholesterol, blood pressure, etc. it contains 13 input features and 2 possible classification outcomes: high or low risk.
  • Obesity prediction: provides data for estimating obesity levels in individuals based on their eating habits and physical condition, resulting in 15 input features and 7 classes.
  • MNIST: A collection of grayscale images of handwritten digits (0–9), with 28x28 inputs, commonly used within image classification tasks as a reference for training, evaluation, and verification of machine learning models.
  • CIFAR10: a dataset that consists of small color images, each with a resolution of 32x32 pixels. These are divided into 10 Classes. The categories are mutually exclusive and represent objects and animals.
  • GTSRB: A multi-class classification dataset containing images of 43 different types of traffic signs captured in real-world conditions with a resolution of 32x32 pixels. It is widely used for training computer vision models to recognize road signs, accounting for challenges like varying lighting, weather, and motion blur.

 

Results:

Experiment result reported in [1]:

In [1], the usefulness of the Craig interpolation and unsatifiable core in computing explanations for neural networks is studied. It showcases the computation of space explanations using the bellow strategies for heart attach, obesity, and mnist datasets:

  • Generalize (G). Compute Craig interpolants (with different interpolation algorithm) on a sample point.
  • Reduce (R). Weaken the formula and reduce size by computing a irreducible (Rmin) or reducible unsatisfiable core. 
  • Capture (C). Partition the sample formula, and Generalize.

All the bellow tables are taken from [1].

Table 1 shows the average number of relaxed features, average number of term in the explanation, and average runtime for explanations with different interpolation algorithms.

Table 1: Average performance of strategy G using different Itp algorithms.

  Heart attack Obesity MNIST
Itp algorithm relaxed #terms time[s] relaxed #terms time[s] relaxed #terms time[s]
stronger 0% 20.1 0.03 0% 29.0 0.30 0% 927.3 9.17
strong 97% 51.0 0.04 72% 45.8 0.30 100% 209.0 10.12
mid 100% 51.0 0.04 100% 45.8 0.34 100% 209.0 10.25
weak 100% 51.0 0.04 100% 46.1 0.30 100% 209.0 10.42
weaker 100% 198.2 0.04 100% 64.1 0.42 100% 67330.6 10.55
Table 2 shows the time overhead of the Reduce strategy. It demonstrates that that Rmin significantly reduces the formula but with a high cost, while R offers a convenientbalance. The reduction times-out (X) with more complex models.

Table 2: Time overhead and impact of Reduce on top of Generalize(R ∘ G).

    #terms time [s]
  Itp algorithm G R ∘ G Rmin ∘ G G R ∘ G Rmin ∘ G
Heart attack stronger 20.1 20.1 9.5 0.03 0.03 3.14
strong 51.0 44.6 3.8 0.04 0.83 16.77
mid 51.0 39.4 4.6 0.04 0.66 11.80
weak 51.0 38.8 6.4 0.04 0.56 7.95
weaker 198.2 197.9 25.9 0.04 0.08 7.14
Obesity stronger 29.0 29.0 X 0.30 0.38 X
strong 45.8 41.7 X 0.30 7.94 X
mid 45.8 42.7 X 0.34 20.62 X
weak 46.1 41.7 X 0.30 35.37 X
weaker 64.1 58.0 X 0.42 23.44 X
MNIST stronger 927.3 927.3 X 9.17 10.45 X
strong 209.0 X X 10.12 X X
mid 209.0 X X 10.25 X X
weak 209.0 X X 10.42 X X
weaker 67330.6 X X 10.55 X X
Table 3 shows the comparision with the state of the art explanation algorithms, abductive and interval explanations.

Table 3: Average performance of G vs. A (Abductive) and I (Interval) strategies in heart‑attack model.

  relaxed #terms #solver calls time [s]
A 38% 8.1 13 0.08
I ∘ A 79% 9.3 40.4 0.53
G 100% 51.0 1 0.04
G ∘ A 100% 45.3 1 0.39
G ∘ I ∘ A 100% 63.5 1 2.53

Experiment results reported in [2]:

 

Other results:

The experiment results on the benchmarks with different setups are listed here.
 
 
Refrences:
  1. Space Explanations of Neural Network Classification, Faezeh Labbaf, Tomáš Kolárik, Martin Blicha, Grigory Fedyukovich, Michael Wand, Natasha Sharygina, 37th CAV 2025
  2. Interpreting Logical Explanations of Classifying Neural Networks, Fabrizio Leopardi, Faezeh Labbaf, Tomáš Kolárik, Michael Wand, Natasha Sharygina, ESANN 2026