CRISP: A Framework for Clause-Reconstructed Interpretable NeuroSymbolic Propositions
Authors: Alex Chan, Shafi Muhtasim Chowdhury, Ekin Can Erkuş, Ole-Christoffer Granmo, Alex Yakovlev, Rishad Shafik
Organizations: School of Engineering, Newcastle University, Newcastle upon Tyne, UK · Northumbria University, Newcastle upon Tyne, UK · Centre for Artificial Intelligence Research, University of Agder, Grimstad, Norway
Deep neural networks achieve high accuracy through layered numerical transformations, yet their decisions remain difficult to audit because decision evidence is encoded in hidden activations rather than explicit rules. This paper introduces CRISP, a framework that reconstructs the last-layer activation vector (LLAV) of binary neural teachers as Tsetlin Machine (TM) clauses. CRISP sign-binarizes the teacher's penultimate pre-logit activations, and assigns one Individual TM (ITM) to each LLAV neuron. Each reconstructed hidden bit is represented by propositional clauses over Booleanized input features, which gives a direct symbolic trace from named input thresholds to a named teacher neuron. CRISP is evaluated on MNIST, KMNIST, FashionMNIST (FMNIST), SVHN, and CIFAR10 using a BinaryConnect convolutional neural network (BCCNN) teacher and a fully binary neural network (BNN) teacher, with an additional study on binary thresholding, thermometer encoding, and quartile binning at multiple bit depths. The results show that LLAV sign-binarization does not reduce teacher-head accuracy in the tested BNN setting, while ITM reconstruction error is the main limiting factor. Quartile one-bit Booleanization gives the strongest reconstruction fidelity on SVHN at 87.52% test fidelity and is competitive on CIFAR10, and the reconstructed LLAV preserves 78.41% teacher-head accuracy on FMNIST. Pooled clause-evidence visualizations show that the learned ITM literals concentrate on the object region in centered benchmarks. CRISP therefore provides a clause-level route for inspecting the final hidden representation of binary neural teachers.
Figures & tables
Fig. 1 : CRISP workflow. A binary neural teacher is trained on the image task, the teacher’s LLAV is extracted and sign-binarized, the original input is Booleanized, and one ITM is trained per LLAV coordinate to form a clause-based hidden-state surrogate.
Dataset
Size
Channels
Train
Val
Test
MNIST
28×28
1
55,000
5,000
10,000
KMNIST
28×28
1
55,000
5,000
10,000
FMNIST
28×28
1
55,000
5,000
10,000
SVHN
32×32
3
68,257
5,000
26,032
CIFAR10
32×32
3
45,000
5,000
10,000
TABLE I : Summary of the five benchmark datasets used.
Teacher
Dataset
Teacher accuracy (%)
ITM test fidelity (%)
BCCNN
MNIST
99.65
85.99
BCCNN
KMNIST
98.86
74.63
BCCNN
FMNIST
94.20
83.92
BCCNN
SVHN
95.01
67.77
BCCNN
CIFAR10
91.06
71.54
BNN
MNIST
98.98
84.31
TABLE II : CRISP performance across datasets and two binary teacher architectures using 8-bit thermometer input encoding.
Dataset
Input to fc_out
Accuracy (%)
κ
MCC
MNIST
BNN baseline
98.98
0.9887
0.9887
LLAV binarized
98.98
0.9887
0.9887
ITM reconstruction
84.68
0.8297
0.8302
FMNIST
BNN baseline
87.83
0.8648
0.8649
LLAV binarized
87.83
0.8648
0.8649
ITM reconstruction
78.41
0.7601
0.7623
TABLE III : Three-way LLAV injection test with the BNN teacher and 8-bit thermometer input encoding.
Fig. 2 : Collective clause evidence pooled across all 256 ITMs for representative test samples. Each panel separates positive- and negative-polarity clauses and maps positive literals Xi and negated literals Xi back to image coordinates. Color intensity denotes pooled literal count within each row.
Dataset
Enc.
Bits
Input Bits
Train acc. (%)
Test fid. (%)
Inf. Time (s)
SVHN
Bin
1
3072
82.94
86.03
275.8
SVHN
Th
1
3072
82.66
85.70
274.4
SVHN
Th
2
6144
79.19
79.98
499.1
SVHN
Th
4
12288
81.49
83.82
1231.0
SVHN
Q
1
3072
84.93
87.52
275.7
SVHN
Q
2
6144
82.16
84.06
414.1
TABLE IV : Effect of Booleanization strategy on ITM reconstruction fidelity for SVHN and CIFAR10.
Neural network interpretability studies how models represent information and make predictions, and how to explain, test, or control their internal computations.