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.
In this article, we establish a precise connection between binarized neural networks (BNNs) and Sugeno integrals. The advantage of the Sugeno integral is that it provides a framework for representing the importance of inputs and their interactions, while being equivalent to a set of if-then rules. For a hidden BNN neuron at inference time, we show that the activation threshold test can be written as a Sugeno integral on binary inputs. This yields an explicit set-function representation of each neuron decision, and an associated rule-based representation. We also provide a Sugeno-integral expression for the last-layer score. Finally, we discuss how the same framework can be adapted to support richer input interactions and how it can be extended beyond the binary case induced by binarized neural networks.
Ismaïl Baaj, Henri Prade
LEMMA, Paris-Panthéon-Assas University · IRIT - Toulouse University
We develop a method for training neural networks on Boolean data in which the values at all nodes are strictly ±1, and the resulting models are typically equivalent to networks whose nonzero weights are also ±1. The method replaces loss minimization with a nonconvex constraint formulation. Each node implements a Boolean threshold function (BTF), and training is expressed through a divide-and-concur decomposition into two complementary constraints: one enforces local BTF consistency between inputs, weights, and output; the other imposes architectural concurrence, equating neuron outputs with downstream inputs and enforcing weight equality across training-data instantiations of the network. The reflect-reflect-relax (RRR) projection algorithm is used to reconcile these constraints. Each BTF constraint includes a lower bound on the margin. When this bound is sufficiently large, the learned representations are provably sparse and equivalent to networks composed of simple logical gates with ±1 weights. Across a range of tasks -- including multiplier-circuit discovery, binary autoencoding, logic-network inference, and cellular automata learning -- the method achieves exact solutions or strong generalization in regimes where standard gradient-based methods struggle. These results demonstrate that projection-based constraint satisfaction provides a viable and conceptually distinct foundation for learning in discrete neural systems, with implications for interpretability and efficient inference.
Veit Elser, Manish Krishan Lal
Department of Physics, Cornell · Mathematics, Independent Researcher, India
Every neuron in a trained network outputs a number that can be separated into its sign (positive or negative) and its magnitude (absolute size). We call the set of all neuron signs the sign code. This raises a key question: does classification depend more on the sign code or on the magnitudes? For overparameterized vision classifiers with sign-preserving activations, the answer is overwhelmingly the sign code. A k-nearest neighbor classifier operating only on this binary sign code achieves accuracy comparable to the full model across different architectures, activation functions, and datasets. Moreover, replacing all magnitudes in every layer with random noise while keeping the original signs barely changes residual network performance. In contrast, flipping just 20% of the signs reduces accuracy to chance. Models generalize well when same-class inputs share similar sign codes. When this overlap is disrupted by a regularizer, training accuracy remains high, but test performance collapses. A margin decomposition helps explain these results: the sign-only contribution to each logit grows as d in network width, dominating the magnitude residual. The natural unit of analysis for these networks may not be through their continuous weight space but instead through their discrete sign codes.
Niclas Göring, Shuofeng Zhang, Roi Holtzman +2
Rudolf Peierls Centre for Theoretical Physics, University of Oxford, Oxford, UK · Kim Jaechul Graduate School of AI, KAIST, Seoul, South Korea