Formal Explanations of Logic Gate Networks

Logic Gate Networks (LGNs) are a Boolean alternative to conventional neural networks (NNs) offering competitive accuracy while enabling highly efficient inference. While their Boolean circuit nature is attractive from an implementation perspective, it also raises a natural question: are LGNs more amenable to formal reasoning and explainability than conventional NNs? In this work, we answer this question through the computation of formal abductive explanations (AXps). We develop a propositional encoding of LGNs that captures their complete inference mechanism, including standard hidden layers, convolutional layers, and the voting mechanism. This enables us to test feature relevance underlying any AXp computation by querying a SAT solver. Since encoding the voting mechanism requires potentially expensive cardinality constraints, we additionally develop a MaxSAT-based reasoning approach that avoids their explicit CNF representation. Experiments across a range of datasets demonstrate that formal explanations of LGNs can be computed several orders of magnitude faster than explanations of conventional NNs using a dedicated state-of-the-art formal explainer. Moreover, we observe that LGNs tend to admit substantially shorter explanations. Hence, our results suggest that, beyond efficient inference, the inherently Boolean structure of LGNs offers significant advantages for formal explainability.