# Eventizing Traditionally Opaque Binary Neural Networks as 1-safe Petri net Models

arXiv: https://arxiv.org/abs/2602.13128 · HTML: https://mlsanity.com/paper/2602.13128/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 16 of its 34 references that are in the map.
- First posted on arXiv 13 Feb 2026.

## Builds on (most cited first, 16 of 16)

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [A Unified Approach to Interpreting Model Predictions](https://mlsanity.com/paper/1705.07874/) (2017)
- ["Why Should I Trust You?": Explaining the Predictions of Any Classifier](https://mlsanity.com/paper/1602.04938/) (2016)
- [Estimating or Propagating Gradients Through Stochastic Neurons for Conditional Computation](https://mlsanity.com/paper/1308.3432/) (2013)
- [Speech Commands: A Dataset for Limited-Vocabulary Speech Recognition](https://mlsanity.com/paper/1804.03209/) (2018)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Quantized Neural Networks: Training Neural Networks with Low Precision Weights and Activations](https://mlsanity.com/paper/1609.07061/) (2016)
- [Understanding Straight-Through Estimator in Training Activation Quantized Neural Nets](https://mlsanity.com/paper/1903.05662/) (2019)
- [FINN: A Framework for Fast, Scalable Binarized Neural Network Inference](https://mlsanity.com/paper/1612.07119/) (2016)
- [The Tsetlin Machine -- A Game Theoretic Bandit Driven Approach to Optimal Pattern Recognition with Propositional Logic](https://mlsanity.com/paper/1804.01508/) (2018)
- [BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks](https://mlsanity.com/paper/2103.07224/) (2021)
- [Seeking Interpretability and Explainability in Binary Activated Neural Networks](https://mlsanity.com/paper/2209.03450/) (2022)
- [Arrhythmia Classifier Based on Ultra-Lightweight Binary Neural Network](https://mlsanity.com/paper/2304.01568/) (2023)
- [Minimizing Classification Energy of Binarized Neural Network Inference for Wearable Devices](https://mlsanity.com/paper/1903.11381/) (2019)
- [Lower Bound Proof for the Size of BDDs representing a Shifted Addition](https://mlsanity.com/paper/2209.12477/) (2022)

## Abstract (arXiv)

Binary Neural Networks (BNNs) offer a low-complexity and energy-efficient alternative to traditional full-precision neural networks by constraining their weights and activations to binary values. However, their discrete, highly non-linear behavior makes them difficult to explain, validate and formally verify. As a result, BNNs remain largely opaque, limiting their suitability in safety-critical domains, where causal transparency and behavioral guarantees are essential. In this work, we introduce a Petri net (PN)-based framework that captures the BNN's internal operations as event-driven processes. By "eventizing" their operations, we expose their causal relationships and dependencies for a fine-grained analysis of concurrency, ordering, and state evolution. Here, we construct modular PN blueprints for core BNN components including activation, gradient computation and weight updates, and compose them into a complete system-level model. We then validate the composed PN against a reference software-based BNN, verify it against reachability and structural checks to establish 1-safeness, deadlock-freeness, mutual exclusion and correct-by-construction causal sequencing, before we assess its scalability and complexity at segment, component, and system levels using the automated measurement tools in Workcraft. Overall, this framework enables causal introspection of transparent and event-driven BNNs that are amenable to formal reasoning and verification.