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

• URL: http://arxiv.org/abs/2602.13128v1
• Date: Fri, 13 Feb 2026 17:25:47 GMT
• Title: Eventizing Traditionally Opaque Binary Neural Networks as 1-safe Petri net Models
• Authors: Mohamed Tarraf, Alex Chan, Alex Yakovlev, Rishad Shafik,
• Abstract summary: Binary Neural Networks (BNNs) offer a low-complexity and energy-efficient alternative to traditional full-precision neural networks.<n>Their discrete, highly non-linear behavior makes them difficult to explain, validate and formally verify.<n>We introduce a Petri net (PN)-based framework that captures the BNN's internal operations as event-driven processes.
• Score: 0.5499796332553707
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Efficient Certified Reasoning for Binarized Neural Networks [25.20597060311209]
  Binarized Neural Networks (BNNs) are a type of neural network where each neuron is constrained to a Boolean value.<n>Existing methods for BNN analysis suffer from limited scalability or susceptibility to soundness errors.<n>We present a scalable and trustworthy approach for both qualitative and quantitative verification of BNNs.
  arXiv  Detail & Related papers  (2025-06-25T09:27:02Z)
• Neural Network Verification with Branch-and-Bound for General Nonlinearities [63.39918329535165]
  Branch-and-bound (BaB) is among the most effective techniques for neural network (NN) verification.<n>We develop a general framework, named GenBaB, to conduct BaB on general nonlinearities to verify NNs with general architectures.<n>Our framework also allows the verification of general nonlinear graphs and enables verification applications beyond simple NNs.
  arXiv  Detail & Related papers  (2024-05-31T17:51:07Z)
• An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks [13.271286153792058]
  Quantized neural networks (QNNs) have been developed, with binarized neural networks (BNNs) restricted to binary values as a special case. This paper presents an automata-theoretic approach to synthesizing BNNs that meet designated properties.
  arXiv  Detail & Related papers  (2023-07-29T06:27:28Z)
• Quantization-aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks [58.195261590442406]
  We study the problem of training and certifying adversarially robust quantized neural networks (QNNs) Recent work has shown that floating-point neural networks that have been verified to be robust can become vulnerable to adversarial attacks after quantization. We present quantization-aware interval bound propagation (QA-IBP), a novel method for training robust QNNs.
  arXiv  Detail & Related papers  (2022-11-29T13:32:38Z)
• Recurrent Bilinear Optimization for Binary Neural Networks [58.972212365275595]
  BNNs neglect the intrinsic bilinear relationship of real-valued weights and scale factors. Our work is the first attempt to optimize BNNs from the bilinear perspective. We obtain robust RBONNs, which show impressive performance over state-of-the-art BNNs on various models and datasets.
  arXiv  Detail & Related papers  (2022-09-04T06:45:33Z)
• Towards Accurate Binary Neural Networks via Modeling Contextual Dependencies [52.691032025163175]
  Existing Binary Neural Networks (BNNs) operate mainly on local convolutions with binarization function. We present new designs of binary neural modules, which enables leading binary neural modules by a large margin.
  arXiv  Detail & Related papers  (2022-09-03T11:51:04Z)
• A Mixed Integer Programming Approach for Verifying Properties of Binarized Neural Networks [44.44006029119672]
  We propose a mixed integer programming formulation for BNN verification. We demonstrate our approach by verifying properties of BNNs trained on the MNIST dataset and an aircraft collision avoidance controller.
  arXiv  Detail & Related papers  (2022-03-11T01:11:29Z)
• Robustness of Bayesian Neural Networks to White-Box Adversarial Attacks [55.531896312724555]
  Bayesian Networks (BNNs) are robust and adept at handling adversarial attacks by incorporating randomness. We create our BNN model, called BNN-DenseNet, by fusing Bayesian inference (i.e., variational Bayes) to the DenseNet architecture. An adversarially-trained BNN outperforms its non-Bayesian, adversarially-trained counterpart in most experiments.
  arXiv  Detail & Related papers  (2021-11-16T16:14:44Z)
• BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks [7.844146033635129]
  We study verification problems for Binarized Neural Networks (BNNs), the 1-bit quantization of general real-numbered neural networks. Our approach is to encode BNNs into Binary Decision Diagrams (BDDs), which is done by exploiting the internal structure of the BNNs. Based on the encoding, we develop a quantitative verification framework for BNNs where precise and comprehensive analysis of BNNs can be performed.
  arXiv  Detail & Related papers  (2021-03-12T12:02:41Z)
• S2-BNN: Bridging the Gap Between Self-Supervised Real and 1-bit Neural Networks via Guided Distribution Calibration [74.5509794733707]
  We present a novel guided learning paradigm from real-valued to distill binary networks on the final prediction distribution. Our proposed method can boost the simple contrastive learning baseline by an absolute gain of 5.515% on BNNs. Our method achieves substantial improvement over the simple contrastive learning baseline, and is even comparable to many mainstream supervised BNN methods.
  arXiv  Detail & Related papers  (2021-02-17T18:59:28Z)
• Incorporating Interpretable Output Constraints in Bayesian Neural Networks [34.103445420814644]
  Output-Constrained BNN (OC-BNN) is fully consistent with the Bayesian framework for uncertainty quantification. We demonstrate the efficacy of OC-BNNs on real-world datasets, spanning multiple domains such as healthcare, criminal justice, and credit scoring.
  arXiv  Detail & Related papers  (2020-10-21T13:00:05Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.