# An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 19 of its 42 references that are in the map.
- First posted on arXiv 29 Jul 2023.

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

- [Very Deep Convolutional Networks for Large-Scale Image Recognition](https://mlsanity.com/paper/1409.1556/) (2014)
- [A White Paper on Neural Network Quantization](https://mlsanity.com/paper/2106.08295/) (2021)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Verifying Properties of Binarized Deep Neural Networks](https://mlsanity.com/paper/1709.06662/) (2017)
- [Who is Real Bob? Adversarial Attacks on Speaker Recognition Systems](https://mlsanity.com/paper/1911.01840/) (2019)
- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [NeuronFair: Interpretable White-Box Fairness Testing through Biased Neuron Identification](https://mlsanity.com/paper/2112.13214/) (2021)
- [Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification](https://mlsanity.com/paper/1902.09866/) (2019)
- [Scalable Verification of Quantized Neural Networks (Technical Report)](https://mlsanity.com/paper/2012.08185/) (2020)
- [Towards Understanding and Mitigating Audio Adversarial Examples for Speaker Recognition](https://mlsanity.com/paper/2206.03393/) (2022)
- [BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks](https://mlsanity.com/paper/2103.07224/) (2021)
- [Advanced Evasion Attacks and Mitigations on Practical ML-Based Phishing Website Classifiers](https://mlsanity.com/paper/2004.06954/) (2020)
- [Taking Care of The Discretization Problem: A Comprehensive Study of the Discretization Problem and A Black-Box Adversarial Attack in Discrete Integer Domain](https://mlsanity.com/paper/1905.07672/) (2019)
- [Attack as Defense: Characterizing Adversarial Examples using Robustness](https://mlsanity.com/paper/2103.07633/) (2021)
- [QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks](https://mlsanity.com/paper/2212.11138/) (2022)
- [AS2T: Arbitrary Source-To-Target Adversarial Attack on Speaker Recognition Systems](https://mlsanity.com/paper/2206.03351/) (2022)
- [QEBVerif: Quantization Error Bound Verification of Neural Networks](https://mlsanity.com/paper/2212.02781/) (2022)
- [QFA2SR: Query-Free Adversarial Transfer Attacks to Speaker Recognition Systems](https://mlsanity.com/paper/2305.14097/) (2023)
- [Safety Verification for Neural Networks Based on Set-boundary Analysis](https://mlsanity.com/paper/2210.04175/) (2022)

## Abstract (arXiv)

Deep neural networks, (DNNs, a.k.a. NNs), have been widely used in various tasks and have been proven to be successful. However, the accompanied expensive computing and storage costs make the deployments in resource-constrained devices a significant concern. To solve this issue, quantization has emerged as an effective way to reduce the costs of DNNs with little accuracy degradation by quantizing floating-point numbers to low-width fixed-point representations. Quantized neural networks (QNNs) have been developed, with binarized neural networks (BNNs) restricted to binary values as a special case. Another concern about neural networks is their vulnerability and lack of interpretability. Despite the active research on trustworthy of DNNs, few approaches have been proposed to QNNs. To this end, this paper presents an automata-theoretic approach to synthesizing BNNs that meet designated properties. More specifically, we define a temporal logic, called BLTL, as the specification language. We show that each BLTL formula can be transformed into an automaton on finite words. To deal with the state-explosion problem, we provide a tableau-based approach in real implementation. For the synthesis procedure, we utilize SMT solvers to detect the existence of a model (i.e., a BNN) in the construction process. Notably, synthesis provides a way to determine the hyper-parameters of the network before training.Moreover, we experimentally evaluate our approach and demonstrate its effectiveness in improving the individual fairness and local robustness of BNNs while maintaining accuracy to a great extent.