We describe the transformation of binary neural networks (BNNs) for classification into deterministic and decomposable Boolean circuits by means of knowledge compilation techniques. The resulting circuit is used, as an open-box model, to compute Shap scores taking advantage of a recent eficient algorithm for Shap on this class of circuits. We show experimental results that corroborate the huge improvement in score computation time in comparison with the computation that directly uses the BNN as a black-box model.
Explanations for the outcomes from classification models come in diferent forms, and can be obtained through diferent approaches. A common one assigns attribution scores to the features values associated to an input that goes through an ML-based model, to quantify their relevance for the obtained outcome. We concentrate on local scores, i.e. associated to a particular input, as opposed to global scores that indicates the overall relevance of a feature. In this work, we also concentrate on explanations for binary classification models, whose features take binary values, so as the classification label, say 0 or 1.
A popular local score is Shap [10], which is based on the Shapley value that has introduced and used in coalition game theory and practice for a long time [15, 13]. Shap scores can be computed with a black-box or an open-box model [14]. With the former, we do not know or use its internal components, but only its input/output relation. This is the most common approach. In the latter case, we can have access to its internal structure and components, and we can use them for score computation. It is common to consider neural-network-based models as black-box models, because their internal gates and structure may be dificult to understand or process when it comes to explaining classification outputs. However, a decision-tree model, due to its much simpler structure and use, is considered to be open-box for the same purpose.
Even for binary classification models, the complexity of Shap computation is provably hard, actually # -hard for several kinds of binary classification models, independently from whether the internal components of the model are used when computing Shap [3, 1, 2]. However, there are classes of classifiers for which, using the model components and structure, the complexity of Shap computation can be brought down to polynomial time [11, 2, 18].
A polynomial time algorithm for Shap computation with deterministic and decomposable Boolean circuits (dDBCs) was presented in [2]. From this result, the tractability of Shap computation can be obtained for a variety of Boolean circuit-based classifiers than can be represented as (or compiled into) them. In particular, this holds for Ordered Binary Decision Diagrams (OBDDs) [5], decision trees, and other established classification models that can be compiled into OBDDs [16, 6, 12]. Similar results can be obtained for Sentential Decision Diagrams (SDDs) [9], which can be seen as dDBCs, and form a convenient knowledge compilation target language [7, 17]. In [18], through a diferent approach, tractability of Shap computation was obtained for a collection of classifiers that intersect with that in [2].
In this work, we concentrate on explicitly developing this approach to the eficient computation of Shap for binary neural networks (BNNs). For this, and inspired by [16], a BNN is transformed into a dDBC using techniques from knowledge compilation [7], an area that investigates the transformation of (usually) propositional theories into an equivalent one with a canonical syntactic form that has some good computational properties, e.g. tractable model counting. The compilation may incur in a relatively high computational cost [7, 8], but it may still be worth the efort when a particular property will be checked often, as is the case of explanations for the same BNN.
We also make experimental comparisons between this open-box and circuit-based Shap computation and that based directly on the BNN treated as a black-box, i.e. using only its input/output relation. We perform comparisons in terms of computation time and alignment of Shap scores. We confirm that Shap computation via the dDBC vastly outperforms the direct Shap computation on the BNN. It is also the case that the scores obtained are fully aligned, as expected since the dDBC represents the BNN. A detailed account of our work can be found in [4].
Consider a fixed entity e = ⟨1(e), . . . , (e)⟩ subject to classification. It has values (e) for features ℱ = {1, . . . , }. In [10, 11], the Shapley value is applied with {1(e), . . . , (e)} as the set of players, and the game function e() := E((e′) | e′ = e), giving rise to the Shap score. Here, e is the projection (or restriction) of e on (to) the subset of features, is the label. The e′ inside the expected value is an entity whose values coincides with those of e for the features in . For ∈ ℱ , and entity e:
Shap(ℱ , e, ) =
∑︁ ⊆ℱ∖{ } ||!(|ℱ | − | | − 1)! |ℱ |!
× [ E((e′) | e′∪{ } = e∪{ }) − E((e′) | e′ = e) ].
The expected value is defined on the basis of an underlying probability distribution on the
entity population. Shap quantifies the contribution of feature value (e) to the outcome label.
of the comparison in (
This number can be computed in general by: (Narodytska et al. 2018)
|¯i|
d = (−b + X wj )/2+# of negative weights in w¯. (
In order to compute Shap, we only need function ,ja=n1d noneof the internal components of the classifier. Given that all possible subsIentstohfefecaatsuereosfaphp1e,arwinithits 2definneitgioatniv,e wSheaigphtiss: boudnd = to be hard to compute. Actually, for so m(−e0c.l1a6ss+ifier(s−, 1its c1om+p1u)t)a/t2io⌉n+m2ay=b2e.comWeith #this-,hwaerdcan ⌈ − (c.f. [2] for some cases). However, in [2]im,itpoisseshcoowndnittihoantsSohnatpwocainpbuet cvoamriapbulteesdwinithptohlyenriogmhtiaslign time for every deterministic and decomaptoasatbimleeB, ocoolneasindecririncugital(ldpDoBssCib)luesecodnavsenaicelnatspsiafieirr.s.ThFeor h1 circuit’s internal structure is used in thweecoombtpauintaittsiocno.ndition to be true:
h1 ←→ (−x1 ∧ −x2) ∨ (−x1 ∧ x3) ∨ (−x2 ∧ x3). (
This is DNF formula, directly obtained from considering all possible convenient pairs (which is already better that trying A BNN is first compiled into a propositionalall cfoarsmesuolaf itnhrCeeonvjaurniacbtilvees Natoarmtiaml Fe)o.rmHo(CwNevFe),r,wthhiecrhe, is a in its turn, is compiled into an SDD, mwohriechexisp efindailtley, citoemraptiivledmientthooda dthDatBCst.illWuseescotmhepunutember Shap on the resulting circuit via the eficoifencotnavlgeonireitnht minpinut[s. 2In].oTrhdeisr ctoomcopnilvaetyiotnheisbpigegrfeorrpmicetdure, once, and is independent from any inwpeutpotostpthoenecltahsesidfieert.aiTlehdedfineasclrcipirtciounitocfatnhibsemuestheoddto(that is compute Shap scores for diferent input aelnstoituiesse.d Wineosuhroewxptehreimcoemntps)ilautniotinl ApaptphenbdyixmAea.nUs soifnga this algorithm, we obtain an equivalent formula defining h1: simple example.
In our BNNs we used, for each gate , a stehp1 fu←n→ction(xa3s∧ac(t−ivxa2ti∨on−fuxn1)c)ti∨on(,−oxf2th∧e −foxrm1):. (
− 1 otherwise, Replacing the definitions of h1, h2, h3 into (8), we finally obtain: o ←→ (−[(x3 ∧ (x2 ∨ x1)) ∨ (x2 ∧ x1)] ∧ ([(−x3 ∧ (−x2 ∨ −x1)) ∨ (−x2 ∧ −x1)] ∨ [(x3 ∧ (−x2 ∨ −x1)) ∨ (−x2 ∧ −x1)])) ∨ ([(−x3 ∧ (−x2 ∨ −x1)) ∨ (−x2 ∧ −x1)] ∧ [(x3 ∧ (−x2 ∨ −x1)) ∨ (−x2 ∧ −x1)]).
(9)
The final pIanrtCoNfFst:ep (a) in path (
(− 1∨− 2)∧(− 1∨− 3)∧(− 2∨− 3).
The BNN on the LHS above is transformed into the propositional formula on the RHS. After that, it is transformed into a simplified CNF formula, which is shown right below. In its turn, the CNF is transformed into the SDD on the RHS below. In general, this is the most expensive step during the overall compilation time, but it has an upper bound that is exponential in the tree-width of the formula [9]. 4 straightfor is, in its tu formula by For this ex
o ←→ ( Having a conversion
Followi
formula is
(SDD) (D
2015), whi
lig and Bu
popular O
can be use
ular, prop
per se pro
Example
SDD, S, t
Nakamura,
nitions.) A
sented wit
Broeck an
alternative
are also n
structs of t
the sub, re
ing ⊤ and
The sub ca
node. [ℓ1|
ifed simulta
without • i
An SDD
FS : ⟨x1,
FS (
4For our
does this jo
too much (c
ider gate h1, with
pa0.16, and input ¯i =
conveniently
instantid then, contributing to
the comparison in (
This
is 1 wFohr ethnistehxeamopultep,tuhte issim1p. lIifietdisCdNeFcfoomrmpuolsaaibslaes ifnolltohwast:, for every ∧-gate, the inputs do not share
tive weights in w¯. (
conversion steps along path (
Following with step (b) along path (
For o(SuDrDe)x(pDearriwmicehnets2,01w1eb; cVoannsiddeenrBrreoaelckesatnadteDaarswaicnheapplication domain, where house prices
3) ∨ (−x2 ∧ x3). (
Example 3. (example 2 cont.) Figure 3(a) shows an of this method (that is i.e. uSsDinDg, oSn,ltyo ibtse iunspedutf/ooruitlpluusttrarteiolant.io(nC.ffo. r m(Buovltaip2l0e1c6a;lls; (b) Similarly, using the circuit as a ppendix A. Using this blackN-abkoamxumrao,dDeeln;zaunmdi, (acn)dWNiisthhintohe20e2fic0i)e nfotraplrgeocirsiethdmefi- in [ 2] for smooth dDBCs with fan-in 2, rmula defining h1: treatniintigons.) An SDDashas doifpfeerenn-tbkoinxd. s of nodes. Those repre
circuit an
sented with encircled numbers are decision nodes (Van den
∨ (−x2 ∧ −x1). (
An SDD represents (or defines) a total Boolean function
2 ∧ x1)] ∧ ratheFrS n:ai⟨vxe1,txra2,nxs3f⟩or∈ma{t0io,1n}a3lg7→orit{h0m,1}l.eavFeosr ceoxanmsipdlee,rable room for improvement.
(−x2 ∧ −x1)] ∨ FS (
underneath, with x2 = 1, we reach the instantiated leaf (−x2 ∧ −x1)] ∧ node labeled with [1|0], a “conjunction”, with the second ext to the right. In this rmula for the output NF. The participating reated as true or false, r −1, resp.
4For our experiments, we programmed a simple algorithm that 1We udsoeesththeisCjaolbif,owrhniilae making sure the generated CNF doesantohttgtprosw://www.kaggle.com/datasets/camnugent/california
Housing Prices dataset available houstoinogm-purcihce(sc..f. Appendix A). −x2 ∧ −x1)]).
(9) , requires transformample, it can be taken
We are grateful, for their scientific and technical help, to: Arthur Choi, Andy Shih, Norbert
Manthey, Maximilian Schleich, and Adnan Darwiche. Part of this work was funded by ANID
Millennium Science Initiative Program - Code ICN17002; and “Centro Nacional de Inteligencia
Artificial” CENIA, FB210017 (Financiamiento Basal para Centros Científicos y Tecnológicos
de Excelencia de ANID), Chile. Both CENIA and SKEMA Canada funded Jorge León’s visit to
Montreal. L. Bertossi is a Professor Emeritus at Carleton University, Ottawa, Canada; and a
Senior Fellow of the Universidad Adolfo Ibáñez (UAI), Chile.
[8] Darwiche, A. On the Tractable Counting of Theory Models and its Application to Truth
Maintenance and Belief Revision. Journal of Applied Non-Classical Logics, 2011, 11(
In Proceedings of the 22th International Joint Conference on Artificial Intelligence (IJCAI-11) ,
2011, 819–826.
[10] Lundberg, S. M. and Lee, S.-I. A Unified Approach to Interpreting Model Predictions. In
Proceedings of the 31st International Conference on Neural Information Processing Systems,
2017, 4768–4777. ArXiv paper 1705.07874.
[11] Lundberg, S., Erion, G., Chen, H., DeGrave, A., Prutkin, J., Nair, B., Katz, R., Himmelfarb, J.,
Bansal, N. and Lee, S.-I. From Local Explanations to Global Understanding with Explainable
AI for Trees. Nature Machine Intelligence,2020, 2(
Press, 1988. [14] Rudin, C. Stop Explaining Black Box Machine Learning Models for High Stakes Decisions and Use Interpretable Models Instead. Nature Machine Intelligence, 2019, 1:206–215. ArXiv paper 1811.10154. [15] Shapley, L. S. A Value for n-Person Games. In Contributions to the Theory of Games (AM-28), 1953, vol. 2, 307–318. [16] Shi, W., Shih, A., Darwiche, A. and Choi, A. On Tractable Representations of Binary Neural Networks. In Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, 2020, 882–892. ArXiv paper 2004.02082. [17] Van den Broeck, G. and Darwiche, A. On the Role of Canonicity in Knowledge Compilation.
In Proceedings of the 29th AAAI Conference on Artificial Intelligence , 2015, 1641–1648. [18] Van den Broeck, G., Lykov, A., Schleich, M. and Suciu, D. On the Tractability of SHAP Explanations. In Proceedings of the 35th AAAI Conference on Artificial Intelligence , 2021, 6505–6513.