An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks
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.
Ye Tao, Wanwei Liu, Fu Song, Zhen Liang, Ji Wang, Hongxu Zhu
# An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks

###### Abstract

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.
## 1 Introduction

Deep Neural Networks (DNNs) are increasingly used in a variety of applications, from image recognition to autonomous driving, due to their high accuracy in classification and prediction tasks [27, 29]. However, two critical challenges emerge, high-cost and a lack of trustworthiness, that impede their further development.

On the one hand, a modern DNN typically contains a large number of parameters which are typically stored as 32-bit floating-point numbers (e.g., GPT-4 contains about 100 trillion parameters [14]), thus an inference often demands more than a billion floating-point operations. As a result, deploying a modern DNN requires huge computing and storage resources, thus it is challenging for resource-constrained embedding devices. To tackle this issue, quantization has been introduced, which compresses a network by converting floating-point numbers to low-width fixed-point representations, so that it can significantly reduce both memory and computing costs using fixed-point arithmetic with a relatively small side-effect on the network's accuracy [23].

On the other hand, neural networks are known to be vulnerable to input perturbations, namely, slight input disturbance may dramatically change their output [12, 3, 28, 4, 35, 5, 6, 7]. In addition, NNs are often treated as black box [17], and we are truly dearth of understanding of the decision-making process inside the "box". As a result, a natural concern is whether NNs can be trustworthy, especially in some safety-critical scenarios, where erroneous behaviors might lead to serious consequences. One promising way to tackle this problem is formal verification, which defines properties that we expect the network to satisfy and rigorously checks whether the network meets our expectations. Numerous verification approaches have been proposed recently aiming at this purpose [17]. Nevertheless, these approaches in general ignore rounding errors in quantized computations, making them unable to apply for quantized neural networks (QNNs). It has been demonstrated that specifications that hold for a floating-point numbered DNN may not necessarily hold after quantizing the inputs and/or parameters of the DNN [3, 13]. For instance, a DNN that is robust to given input perturbations might become non-robust after quantization. Compared to DNN verification [17, 18, 20, 21, 19, 36, 15], verifying QNN is truly a more challenging and less explored problem. Evidences show that the verification problem for QNNs is harder than DNNs [16], and only few works are specialized for verifying QNNs [1, 8, 13, 16, 24, 26, 32, 33, 34, 31].

In this paper, we concentrate on BNNs (i.e., binarized neural networks), a special type of QNN. Although formal verification has been the primary explored approach to verifying (quantized) neural networks, we pursue another promising line, synthesizing the expected binarized neural networks directly. In other words, we aim to construct a neural network that satisfies the expected properties we specify, rather than verifying an existing network's compliance with those properties. To achieve this, we first propose, BLTL, an extension of \(\text{LTL}_{f}\) (namely, LTL defined on finite words), as the specification language. This logic can conveniently describe data-related properties of BNNs. We then provide an approach to converting a BLTL formula to an equivalent automaton. The syn
thesis task is then boiled down to find a path from an initial state to an accepting state in the automaton.

Unfortunately, such a method suffers from the state-exploration problem. To mitigate this issue, we observe that it is not necessary to synthesize the entire BNN since the desired properties are only related to some specific hyper-parameters of the network. To this end, we propose a tableau-based approach: To judge whether a path is successfully detected, we check the satisfiability of the associated BLTL formulas, and convert the problem into an IDL-solving problem, which can be efficiently solved. Besides, we prove the existence of a tracing-back threshold, which allows us to do backtracking earlier to avoid doing trace searching that is unlikely to lead to a solution. The solution given by the solver provides the hyper-parameters of the BNN, including the length of the network and crucial input-output relations of blocks. Afterwards, one can perform a block-wise training to obtain a desired BNN.

We implement a prototype synthesizing tool and evaluate our approach on local robustness and individual fairness. The experiments demonstrate that our approach can effectively improve the network's reliability compared to the baseline, especially for individual fairness.

The main contributions of this work are summarized as follows:

* We present a new temporal logic, called BLTL, for describing properties of BNNs, and provide an approach to transforming BLTL formulas into equivalent finite-state automata.
* We propose an automata-theoretic synthesis approach that determines the hyper-parameters of a BNN model before training.
* We implement a prototype synthesis tool and evaluate the effectiveness on two concerning properties, demonstrating the feasibility of our method.

**Related Work.** For BNNs, several verification approaches have been proposed. Earlier work reduces the BNN verification problem to hardware verification (i.e., verifying combinatorial circuits), for which SAT solvers are harnessed [8]. Following this line, [24] proposes a direct encoding from the BNN verification problem into the SAT problem. [25] studies the effect of BNN architectures on the performance of SAT solvers and uses this information to train SAT-friendly BNNs. [1] provides a framework for approximately quantitative verification of BNNs with PAC-style guarantees via approximate SAT model counting. Another line of BNN verification encodes a BNN and its input region into a binary decision diagram (BDD), and then one can verify some properties of the network by analyzing BDD. [26] proposes an Angluin-style learning algorithm to compile a BNN on a given input region into a BDD, and utilize a SAT solver as an equivalence oracle to query. [32] has developed a more efficient BDD-based quantitative verification framework by exploiting the internal structure of BNNs. Few work has been dedicated to QNN verification so far. [13] shows that the properties guaranteed by the DNN are not preserved after quantization. To resolve this issue, they introduce an approach to verifying QNNs by using SMT solvers in bit-vector theory. Later, [16] proves that verifying QNN with bit-vector specifications is **PSPACE**-Hard. More recently, [34, 31] reduce the verification problem
into integer linear constraint solving which are significantly more efficient than the SMT-based one.

**Outline.** The rest of the paper is organized as follows: In Section 2, we introduce preliminaries. We present the specification language BLTL in Section 3. In Section 4, we show how to translate a BLTL formula into an equivalent automaton, which is the basic of tableau-based approach for synthesis, and technical details are given in Section 5. The proposed approach is implemented and evaluated in Section 6. We conclude the paper in Section 7.

## 2 Preliminaries

We denote by \(\mathbb{R}\), \(\mathbb{N}\), and \(\mathbb{B}\) the set of real numbers, natural numbers, and Boolean domain \(\{0,1\}\), respectively. We use \(\mathbb{R}^{n}\) and \(\mathbb{B}^{n}\) to denote the set of real number vectors and binary vectors with \(n\) elements, respectively. For \(n\in\mathbb{N}\), let \([n]\) be the set \(\{0,1,2,\ldots,n-1\}\). We will interchangeably use the terminologies 0-1 vector and binary vector in this paper. For a binary vector \(\mathbf{b}\), we use \(\mathsf{dec}(\mathbf{b})\) to denote its corresponding decimal number, and conversely let \(\mathsf{bin}(d)\) be the corresponding binary vector which encodes the number \(d\). For example, let \(\mathbf{b}=(0,1,1)^{\mathrm{T}}\), then we have \(\mathsf{dec}(\mathbf{b})=3\). Note that \(\mathsf{bin}(\mathsf{dec}(\mathbf{b}))=\mathbf{b}\) and \(\mathsf{dec}(\mathsf{bin}(d))=d\). For two binary vectors \(\mathbf{a}=\left(a_{0},\ldots,a_{n-1}\right)^{\mathrm{T}}\) and \(\mathbf{b}=\left(b_{0},\ldots,b_{n-1}\right)^{\mathrm{T}}\) with the same length, we denote by \(\mathbf{a}\sim\mathbf{b}\) if \(a_{i}\sim b_{i}\) for all \(i\in[n]\), otherwise \(\mathbf{a}\not\sim\mathbf{b}\), where \(\sim\in\{>,\geq,<,\leq,=\}\). Note that \(\mathbf{a}\neq\mathbf{b}\) if \(a_{i}\neq b_{i}\) for some \(i\in[n]\).

A (vectorized) Boolean function takes a 0-1 vector as input and returns another 0-1 vector. Hence, it is essentially a mapping from integers to integers when each 0-1 vector \(\mathbf{b}\) is viewed as an integer \(\mathsf{dec}(\mathbf{b})\). We denote by \(\mathbf{I}_{n}\) the identity function such that \(\mathbf{I}_{n}\left(\mathbf{b}\right)=\mathbf{b}\), for any \(\mathbf{b}\in\mathbb{B}^{n}\), where the subscript \(n\) may be dropped when it is clear from the context. We use _composition_ operation \(\circ\) to represent the function composition among Boolean functions.

A _binarized neural network_ (BNN) is a feed-forward neural network, composed of several internal blocks and one output block [26, 32]. Each internal block is comprised of 3 layers and can be viewed as a mapping \(f:\{-1,1\}^{n}\rightarrow\{-1,1\}^{m}\). Slightly different from internal blocks, the output block outputs the classification label to which the highest activation corresponds, thus, can be seen as a mapping \(\mathsf{out}:\{-1,1\}^{n}\rightarrow\mathbb{R}^{p}\), where \(p\) is the number of classification labels of the network.

Since the binary values \(-1\) and \(+1\) can be represented as their Boolean counterparts 0 and 1 respectively, each internal block can be viewed as a Boolean function \(f:\mathbb{B}^{n}\rightarrow\mathbb{B}^{m}\)[32]. Therefore, ignoring the slight difference in the output block, an \(n\)-block BNN \(\mathcal{N}\) can be encoded via a series of Boolean functions \(f_{i}:\mathbb{B}^{\ell_{i}}\rightarrow\mathbb{B}^{\ell_{i+1}}\) (\(i=0,1,\ldots,n-1\)), and \(\mathcal{N}\) works as the combination of these Boolean functions, namely, it corresponds to the function,

\[f_{\mathcal{N}}=f_{n-1}\circ f_{n-2}\circ\cdots\circ f_{1}\circ f_{0}.\]

_Integer difference logic_ (IDL) is a fragment of linear integer arithmetic, in which atomic formulas must be of the form \(x-y\sim c\) where \(x\) and \(y\) are integer
variables, and \(c\) is an integer constant, \(\sim\in\{\leq,\geq,<,>,=,\neq\}\). All these atomic formulas can be transformed into constraints of the form \(x-y\leq c\)[2]. For example, \(x-y=c\) can be transformed into \(x-y\leq c\wedge x-y\geq c\).

The task of an IDL-problem is to check the satisfiability of an IDL formula in conjunctive normal form (CNF)

\[(x_{1}-y_{1}\leq c_{1})\wedge\cdots\wedge(x_{n}-y_{n}\leq c_{n}),\]

which can be in general converted into the cycle detection problem in a weighted, directed graph with \(O(n)\) nodes and \(O(n)\) edges, and solved by e.g., Bellman-Ford or Dijkstra's algorithm, in \(O(n^{2})\) time [22].

## 3 The Temporal Logic BLTL

### Syntax and Semantics of BLTL

Let us fix a signature \(\vec{\Sigma}\), consisting of a set of desired Boolean functions and 0-1 vectors. Particularly, let \(\vec{\Sigma}_{\mathrm{V}}\) be the subset of \(\vec{\Sigma}\) containing only 0-1 vectors.

Terms of BLTL are described via BNF as follows:

\[\vec{t}::=\vec{b}\mid f\left(\vec{t}\right)\mid\rhd^{k}\vec{t}\]

where \(\vec{b}\in\vec{\Sigma}_{\mathrm{V}}\) is a 0-1 vector, called _vector constant_, \(f\in\vec{\Sigma}\setminus\vec{\Sigma}_{\mathrm{V}}\) is a Boolean function, and \(k\in\mathbb{N}\) is a constant, and \(\rhd^{k}\) in \(\rhd^{k}\vec{t}\) denotes \(k\) placeholders for \(k\) consecutive blocks of a BNN (i.e., \(k\) Boolean functions) to be applied onto the term \(\vec{t}\). We remark that \(\rhd^{0}\vec{t}=\vec{t}\).

BLTL formulas are given via the following grammar:

\[\psi::=\top\mid\vec{t}\sim\vec{t}\mid\neg\psi\mid\psi\vee\psi\mid\mathsf{X} \psi\mid\psi\mathsf{U}\psi\]

where \(\sim\in\{\leq,\geq,<,>,=\}\), \(\mathsf{X}\) is the _Next_ operator and \(\mathsf{U}\) is the _Until_ operator.

We define the following derived Boolean operators, quantifiers with finite domain, and temporal operators:

\[\psi_{1}\wedge\psi_{2}\stackrel{{\mathrm{def}}}{{=}} \neg(\neg\psi_{1}\vee\neg\psi_{2}) \mathsf{F}\psi\stackrel{{\mathrm{def}}}{{=}}\top \mathsf{U}\psi \mathsf{G}\psi\stackrel{{\mathrm{def}}}{{=}}\neg\mathsf{F} \neg\psi\] \[\psi_{1}\rightarrow\psi_{2}\stackrel{{\mathrm{def}}}{{= }}(\neg\psi_{1})\vee\psi_{2} \mathsf{F}\psi_{1}\mathsf{R}\psi_{2}\stackrel{{\mathrm{def}}} {{=}}\neg(\neg\psi_{1}\mathsf{U}\neg\psi_{2}) \mathsf{X}\psi\stackrel{{\mathrm{def}}}{{=}}\neg \mathsf{X}\neg\psi\] \[\forall\vec{x}\in\mathbb{B}^{k}.\psi\stackrel{{ \mathrm{def}}}{{=}}\bigwedge_{\vec{b}\in\mathbb{B}^{k}\cap\vec{\Sigma}_{ \mathrm{V}}}\psi[\vec{x}/\vec{b}] \exists\vec{x}\in\mathbb{B}^{k}.\psi\stackrel{{\mathrm{ def}}}{{=}}\neg\forall\vec{x}\in\mathbb{B}^{k}.\neg\psi\]

where \(\psi[\vec{x}/\vec{b}]\) denotes the BLTL formula obtained from \(\psi\) by replacing each occurrence of \(\vec{x}\) with \(\vec{b}\).

The semantics of BLTL formulas is defined w.r.t. a BNN \(\mathcal{N}\) given by the composition of Boolean functions \(f_{\mathcal{N}}=f_{n-1}\circ f_{n-2}\circ\cdots\circ f_{1}\circ f_{0}\), and a position \(i\in\mathbb{N}\). We first define the semantics of terms, which is given by the function \(\llbracket\bullet\rrbracket_{\mathcal{N},i}\), inductively:

* \(\llbracket\vec{b}\rrbracket_{\mathcal{N},i}=\vec{b}\) for each vector constant \(\vec{b}\);
* \(\llbracket f\left(\vec{t}\right)\rrbracket_{\mathcal{N},i}=f\left(\llbracket \vec{t}\rrbracket_{\mathcal{N},i}\right)\);
* \(\llbracket\rhd^{k}\boldsymbol{t}\rrbracket_{\mathcal{N},i}=\left\{\begin{array}{ ll}(f_{i+\mathsf{slen}(\boldsymbol{t})+k-1}\circ\cdots\circ f_{i+\mathsf{slen}( \boldsymbol{t})})(\llbracket\boldsymbol{t}\rrbracket_{\mathcal{N},i}),&\text{if $k\geq 1$};\\ \llbracket\boldsymbol{t}\rrbracket_{\mathcal{N},i},&\text{if $k=0$};\end{array}\right.\)

where \(f_{i}\) is the identity Boolean function \(\boldsymbol{I}\) if \(i\geq n\), \(\mathsf{slen}(\boldsymbol{b})=0\), \(\mathsf{slen}(f(\boldsymbol{t}))=\mathsf{slen}(\boldsymbol{t})+1\) and \(\mathsf{slen}(\rhd^{k}\boldsymbol{t})=\mathsf{slen}(\boldsymbol{t})+k\).

Note that we assume the widths of Boolean functions and their argument vectors are compatible.

Proposition 1: _We have: \(\llbracket\rhd^{k}\rhd^{k^{\prime}}\boldsymbol{t}\rrbracket_{\mathcal{N},i}= \llbracket\rhd^{k+k^{\prime}}\boldsymbol{t}\rrbracket_{\mathcal{N},i}\)._

Subsequently, the semantics of BLTL formulas is characterized via the _satisfaction_ relation \(\models\), inductively:

* \(\mathcal{N},i\models\top\) always holds;
* \(\mathcal{N},i\models\boldsymbol{t}_{1}\sim\boldsymbol{t}_{2}\) iff \(\llbracket\boldsymbol{t}_{1}\rrbracket_{\mathcal{N},i}\sim\llbracket \boldsymbol{t}_{2}\rrbracket_{\mathcal{N},i}\);
* \(\mathcal{N},i\models\neg\varphi\) iff \(\mathcal{N},i\not\models\varphi\);
* \(\mathcal{N},i\models\varphi_{1}\vee\varphi_{2}\) iff \(\mathcal{N},i\models\varphi_{1}\) or \(\mathcal{N},i\models\varphi_{1}\);
* \(\mathcal{N},i\models\mathsf{X}\psi\) iff \(i<n-1\) and \(\mathcal{N},i+1\models\psi\);
* \(\mathcal{N},i\models\psi_{1}\mathsf{U}\psi_{2}\) iff there is \(j\) such that \(i\leq j<n\), \(\mathcal{N},j\models\psi_{2}\) and \(\mathcal{N},k\models\psi_{1}\) for each \(i\leq k<j\);

We may write \(\mathcal{N}\models\psi\) in the case of \(i=0\). In the sequel, we denote by \(\mathscr{L}(\psi)\) the set of BNNs \(\{\mathcal{N}\mid\mathcal{N}\models\varphi\}\) for each formula \(\varphi\), and denote by \(\psi_{1}\equiv\psi_{2}\) if \(\mathcal{N},i\models\psi_{1}\Leftrightarrow\mathcal{N},i\models\psi_{2}\) for every BNN \(\mathcal{N}\) and \(i\).

Proposition 2: _The following statements hold:_

1. \(\mathsf{G}\psi\equiv\bot\mathsf{R}\psi\)_;_
2. \(\mathsf{F}\psi\equiv\psi\vee\mathsf{X}\mathsf{F}\psi\)_;_
3. \(\mathsf{G}\psi\equiv\psi\wedge\mathsf{X}\mathsf{G}\psi\)_;_
4. \(\psi_{1}\mathsf{U}\psi_{2}\equiv\psi_{2}\vee(\psi_{1}\wedge\mathsf{X}(\psi_{1} \mathsf{U}\psi_{2}))\)_;_
5. \(\psi_{1}\mathsf{R}\psi_{2}\equiv\psi_{2}\wedge(\psi_{1}\vee\overline{\mathsf{ X}}(\psi_{1}\mathsf{R}\psi_{2}))\)_._

For a BLTL formula \(\varphi\) and a BNN \(\mathcal{N}\), the _model checking_ problem w.r.t. \(\varphi\) and \(\mathcal{N}\) is to decide whether \(\mathcal{N}\models\varphi\) holds.

With the above derived operators, together with the patterns \(\neg\neg\psi\equiv\psi\) and \(\neg(\boldsymbol{t}_{1}\sim\boldsymbol{t}_{2})\equiv\boldsymbol{t}_{1}\not \sim\boldsymbol{t}_{2}\), BLTL formulas can be transformed into _negation normal form_ (NNF) by pushing the negations (\(\neg\)) inward, till no the negations are involved.

Given two sets of formulas \(\Gamma\) and \(\Gamma^{\prime}\) in NNF, we say that \(\Gamma^{\prime}\) is a _proper closure_ of \(\Gamma\), if the following conditions hold:

* \(\Gamma\subseteq\Gamma^{\prime}\).
* \(\psi_{1}\wedge\psi_{2}\in\Gamma^{\prime}\) implies that both \(\psi_{1}\in\Gamma^{\prime}\) and \(\psi_{2}\in\Gamma^{\prime}\).
* \(\psi_{1}\vee\psi_{2}\in\Gamma^{\prime}\) implies that either \(\psi_{1}\in\Gamma^{\prime}\) or \(\psi_{2}\in\Gamma^{\prime}\).
* \(\psi_{1}\mathsf{U}\psi_{2}\in\Gamma^{\prime}\) implies \(\psi_{2}\vee(\psi_{1}\wedge\mathsf{X}(\psi_{1}\mathsf{U}\psi_{2}))\in\Gamma^{\prime}\).
* \(\psi_{1}\mathsf{R}\psi_{2}\in\Gamma^{\prime}\) implies \(\psi_{2}\wedge(\psi_{1}\vee\overline{\mathsf{X}}(\psi_{1}\mathsf{R}\psi_{2}))\in \Gamma^{\prime}\).

We denote by \(\mathsf{Cl}(\Gamma)\) the set consisting of all proper closures of \(\Gamma\) (note that \(\mathsf{Cl}(\Gamma)\) is a family of formula sets.) We also denote by \(\mathsf{Sub}(\psi)\) the set of the subformulas of \(\psi\) except that

* if \(\psi_{1}\mathsf{U}\psi_{2}\in\mathsf{Sub}(\psi)\), then \(\psi_{2}\vee(\psi_{1}\wedge\mathsf{X}(\psi_{1}\mathsf{U}\psi_{2}))\in\mathsf{ Sub}(\psi)\);
* if \(\psi_{1}\mathsf{R}\psi_{2}\in\mathsf{Sub}(\psi)\), then \(\psi_{2}\wedge(\psi_{1}\vee\overline{\mathsf{X}}(\psi_{1}\mathsf{R}\psi_{2})) \in\mathsf{Sub}(\psi)\).
### Illustrating Properties Expressed by BLTL

In this section, we demonstrate the expressiveness of BLTL. Since BLTL has the ability to express Boolean logic and arithmetic operations, we can see that many concerning properties can be specified using BLTL.

We can partition a vector into segments of varying widths, and then define a Boolean function, denoted by \(e_{i}\), to extract the \(i\)-th segment with width of \(n\), namely, \(e_{i}:\mathbb{B}^{m}\rightarrow\mathbb{B}^{n}\), where \(m\) is the width of vector \(\vec{b}\). We use \(\vec{b}[i]\) to refer to \(e_{i}\left(\vec{b}\right)\) in the case that \(e_{i}\left(\vec{b}\right)\in\mathbb{B}\).

Local Robustness.Given a BNN \(\mathcal{N}\) and a \(n\)-width input \(\vec{u}\), \(\mathcal{N}\) is robust w.r.t. \(\vec{u}\), if all inputs in the region \(B\left(\vec{u},\epsilon\right)\), are classified into the same class as \(\vec{u}\)[1]. Here, we consider \(B\left(\vec{u},\epsilon\right)\) as the set of vectors that differ from \(\vec{u}\) in at most \(\epsilon\) positions, where \(\epsilon\) is the maximum number of positions at which the values differ from those of \(\vec{u}\). The local robustness can be described as follows:

\[\forall\vec{x}\in\mathbb{B}^{n}.\sum_{i=1}^{|\vec{u}|}\left(\vec{x}[i]\oplus \vec{u}[i]\right)\leq\epsilon\rightarrow\mathcal{N}\left(\vec{x}\right)= \mathcal{N}\left(\vec{u}\right)\]

Individual Fairness.In the context of a BNN \(\mathcal{N}\) with an input of \(t\) attributes and \(n\)-width, where the \(s\)-th attribute is considered sensitive, \(\mathcal{N}\) is fair w.r.t the \(s\)-th attribute, when no two input vectors in its domain differ only in the value of the \(s\)-th attribute and yield different outputs [30, 37]. The individual fairness can be formulated as:

\[\forall\vec{a},\vec{b}\in\mathbb{B}^{n}.\left(\neg\left(e_{s}(\vec{a})=e_{s}( \vec{b})\right)\wedge\forall i\in[t]-\{s\}.e_{i}(\vec{a})=e_{i}(\vec{b}) \right)\rightarrow\mathcal{N}\left(\vec{a}\right)=\mathcal{N}\left(\vec{b}\right)\]

where \(e_{i}\) denotes the extraction of the \(i\)-th attribute, \(\mathbb{B}^{n}\) is the domain of \(\mathcal{N}\), and \(\vec{a}\), \(\vec{b}\) are input vectors.

In practice, it is possible to select inputs in the \(\mathbb{B}^{n}\), and modify the sensitive attribute to obtain the proper pairs, which only differ in the sensitive attribute. For any such pair \((\vec{b},\vec{b}^{\prime})\),we formulate the specification as \(\mathcal{N}(\vec{b})=\mathcal{N}(\vec{b}^{\prime})\).

Specification for Internal Blocks.BLTL can specify block-level properties. For instance, the formula

\[\forall\vec{x}\in\mathbb{B}^{4}.\mathsf{F}\left(\vec{x}\geq\vec{a} \rightarrow\rhd\vec{x}=\vec{a}\right)\]

states that there exists a block in the network that behaves as follows: for any 4-bit input whose value is greater than or equal to \(\vec{a}\), the corresponding output is equal to \(\vec{a}\).

## 4 From BLTL to Automata

In this section, we present both an explicit and an implicit construction that translate a BLTL formula into an equivalent finite-state automaton. We first show how to eliminate the placeholders \(\rhd^{k}\) in terms \(\rhd^{k}\vec{t}\) and atomic formulas \(\vec{t}_{1}\sim\vec{t}_{2}\).
### Eliminating Placeholders

To eliminate the placeholders \(\rhd^{k}\) in terms \(\rhd^{k}\mathbf{t}\), we define the _apply operator_\([\;]:\mathbf{T}\times\mathbf{\Sigma}\setminus\mathbf{\Sigma}_{\mathbf{V}}\to\mathbf{T}\), where \(\mathbf{T}\) denotes the set of terms. \([\mathbf{t},f]\), written as \(\mathbf{t}[f]\), is called the _application_ of the term \(\mathbf{t}\) w.r.t. the Boolean function \(f\in\mathbf{\Sigma}\), which instantiates the innermost placeholder of the term \(\mathbf{t}\) by the Boolean function \(f\). Below, we give a formal description of the application.

Let us fix a term \(\mathbf{t}\). According to Proposition 1, \(\mathbf{t}\) can be equivalently transformed into the following canonical form

\[\rhd^{\ell_{k}}g_{k-1}\left(\rhd^{\ell_{k-1}}g_{k-2}\left(\cdots g_{0}\left( \rhd^{\ell_{0}}\mathbf{b}\right)\cdots\right)\right)\]

where \(\mathbf{b}\) is a vector constant, \(\ell_{0}\geq 0\) and \(\ell_{i}>0\) for each \(i>0\). Hereafter, we assume that \(\mathbf{t}\) is in the canonical form, and let \(\mathsf{len}(\mathbf{t})=\sum_{i=0}^{k}\ell_{i}\).

When \(\mathbf{t}\) is \(\rhd\)-free, i.e., \(\mathsf{len}(\mathbf{t})=0\), we let \(\mathbf{t}[f]=\mathbf{t}\). When \(\mathsf{len}(\mathbf{t})>0\), we say that the Boolean function \(f\in\mathbf{\Sigma}\) is _applicable_ w.r.t. the term \(\mathbf{t}\), if:

1. \(\mathbf{b}\in\mathsf{dom}\,f\);
2. if \(\ell_{0}=1\), then \(\mathsf{ran}\,f=\mathsf{dom}\,g_{0}\).

Intuitively, the above two conditions ensure that \(f\left(\mathbf{b}\right)\) and \(g_{0}\circ f\) are well-defined.

If \(f\in\mathbf{\Sigma}\) is applicable w.r.t. the term \(\mathbf{t}\), we let \(\mathbf{t}[f]\) be the term:

\[\mathbf{t}[f]=\begin{cases}\rhd^{\ell_{k}}g_{k-1}\left(\rhd^{\ell_{k-1}}g_{k-2} \left(\cdots g_{0}\left(\rhd^{\ell_{0}-1}\mathbf{b}^{\prime}\right)\cdots\right) \right),&\text{if }\ell_{0}>1\\ \rhd^{\ell_{k}}g_{k-1}\left(\rhd^{\ell_{k-1}}g_{k-2}\left(\cdots g_{1}\left( \rhd^{\ell_{1}}\mathbf{b}^{\prime\prime}\right)\cdots\right)\right),&\text{if }\ell_{0}=1 \end{cases}\]

where \(\mathbf{b}^{\prime}=f\left(\mathbf{b}\right)\) and \(\mathbf{b}^{\prime\prime}=\left(g_{0}\circ f\right)\left(\mathbf{b}\right)\).

It can be seen that \(\mathsf{len}(\mathbf{t}[f])=\mathsf{len}(\mathbf{t})-1\). By iteratively applying this operator, the placeholders \(\rhd^{k}\) in the term \(\mathbf{t}\) can be eliminated. For convenience, we write \(\mathbf{t}[f_{0},f_{1},\ldots,f_{i}]\) for the shorthand of

\[\mathbf{t}[f_{0}][f_{1}]\cdots[f_{i}],\]

provided that each Boolean function \(f_{i}\) is applicable w.r.t. \(\mathbf{t}[f_{0}][f_{1}]\cdots[f_{i}]\). Likewise, we call \(\mathbf{t}[f_{0},f_{1},\ldots,f_{i}]\) the _application_ of \(\mathbf{t}\) w.r.t. the Boolean functions \(f_{0},f_{1},\cdots,f_{i}\).

In particular, the _collapsion_ of term \(\mathbf{t}\), denoted by \(\mathbf{t}\downarrow\), is the term \(\mathbf{t}[\underbrace{\mathbf{I},\ldots,\mathbf{I}}_{\mathsf{len}(\mathbf{t})}]\), namely, \(\mathbf{t}\downarrow\) is obtained from \(\mathbf{t}\) w.r.t. \(\mathsf{len}(\mathbf{t})\) identity functions.

We hereafter denote by \(\mathsf{Cons}(\mathbf{\Sigma})\) the set of constraints \(\mathbf{t}_{1}\sim\mathbf{t}_{2}\) over the signature \(\mathbf{\Sigma}\) and lift the apply operator \([\;]\) from terms to atomic formulas \(\mathbf{t}_{1}\sim\mathbf{t}_{2}\). For a constraint \(\gamma=\mathbf{t}_{1}\sim\mathbf{t}_{2}\in\mathsf{Cons}(\mathbf{\Sigma})\), we denote by \(\gamma[f]\) the constraint \(\mathbf{t}_{1}[f]\sim\mathbf{t}_{2}[f]\); and by \(\gamma\downarrow\) the constraint \(\mathbf{t}_{1}\downarrow\sim\mathbf{t}_{2}\downarrow\). Note that the former implicitly assumes that the Boolean function \(f\) is applicable w.r.t. both terms \(\mathbf{t}_{1}\) and \(\mathbf{t}_{2}\) (in this case, we call that \(f\) is applicable w.r.t. \(\gamma\)), whereas the latter requires that the terms \(\mathbf{t}_{1}\downarrow\) and \(\mathbf{t}_{2}\downarrow\) have the same width (we call that \(\mathbf{t}_{1}\) and \(\mathbf{t}_{2}\) are _compatible_ w.r.t. collapsion). In addition, we let \(\mathsf{len}(\gamma)=\max(\mathsf{len}(\mathbf{t}_{1}),\mathsf{len}(\mathbf{t}_{2}))\)
and in the case that \(\mathsf{len}(\gamma)=0\), we let \(\gamma[f]=\top\) (resp. \(\gamma[f]=\bot\)) for any Boolean function \(f\) if \(\gamma\) is evaluated to true (resp. false).

We subsequently extend the above notations to constraint sets. Suppose that \(\Gamma\subseteq\mathsf{Cons}(\boldsymbol{\Sigma})\), we let \(\Gamma[f]\stackrel{{\mathrm{def}}}{{=}}\{\gamma[f]\mid\gamma\in \Gamma\}\), and let \(\Gamma\downarrow\stackrel{{\mathrm{def}}}{{=}}\{\gamma\downarrow \mid\gamma\in\Gamma\}\). Remind that the notation \(\Gamma[f]\) makes sense only if the Boolean function \(f\) is _applicable_ w.r.t. \(\Gamma\), namely \(f\) is applicable w.r.t. each constraint \(\gamma\in\Gamma\). Likewise, the notation \(\Gamma\downarrow\) indicates that \(\boldsymbol{t}_{1}\) and \(\boldsymbol{t}_{2}\) is compatible w.r.t. collapsion for each constraint \(\boldsymbol{t}_{1}\sim\boldsymbol{t}_{2}\in\Gamma\).

Theorem 4.1: _For a BNN \(\mathcal{N}\) given by \(f_{\mathcal{N}}=f_{n-1}\circ f_{n-2}\circ\cdots\circ f_{1}\circ f_{0}\), and a constraint \(\gamma\in\mathsf{Cons}(\boldsymbol{\Sigma})\), we have:_

1. \(\mathcal{N},i\models\gamma\) _iff_ \(\mathcal{N},i+1\models\gamma[f_{i}]\) _for each_ \(i<n\)_._
2. \(\mathcal{N},i\models\gamma\) _iff_ \(\mathcal{N},i\models\gamma\downarrow\) _for each_ \(i\geq n\)_._

Indeed, since \(\gamma\downarrow\) must have the form \(\boldsymbol{b}_{1}\sim\boldsymbol{b}_{2}\), where both \(\boldsymbol{b}_{1}\) and \(\boldsymbol{b}_{2}\) are Boolean constants, then the truth value of \(\gamma\downarrow\) can always be directly evaluated.

### Automata Construction

Given a BLTL formula \(\varphi\) in NNF, we can construct a finite-state automaton \(\mathcal{A}_{\varphi}=(Q_{\varphi},\boldsymbol{\Sigma},\delta_{\varphi},I_{ \varphi},F_{\varphi})\), where:

* \(Q_{\varphi}=\bigcup_{\Gamma\subseteq\mathsf{Sub}(\varphi)}\mathsf{Cl}(\Gamma)\). Recall that \(\mathsf{Cl}(\Gamma)\subseteq 2^{\mathsf{Sub}(\varphi)}\) if \(\Gamma\subseteq\mathsf{Sub}(\varphi)\), thus each state must be a subset of \(\mathsf{Sub}(\varphi)\).
* For each \(q\in Q_{\varphi}\), let \(\mathsf{Cons}(q)\stackrel{{\mathrm{def}}}{{=}}q\cap\mathsf{Cons}( \boldsymbol{\Sigma})\), let \(q^{\prime}=\{\psi\mid\mathsf{X}\psi\in q\}\) and let \(q^{\prime\prime}=\{\psi\mid\mathsf{X}\psi\in q\}\). Then, for each Boolean function \(f\in\boldsymbol{\Sigma}\), we have \[\delta_{\varphi}(q,f)=\begin{cases}\emptyset,&\bot\in q\\ \mathsf{Cl}(q^{\prime}\cup q^{\prime\prime}\cup\mathsf{Cons}(q)[f]),&\bot\not\in q \end{cases}.\]
* \(I_{\varphi}=\{q\in Q_{\varphi}\mid\varphi\in q\}\) is the set of initial states.
* \(F_{\varphi}\) is the set of accepting states such that for every state \(q\in Q_{\varphi}\), \(q\in F_{\varphi}\) only if \(\{\psi\mid\mathsf{X}\psi\in q\}=\emptyset\), \(\bot\not\in q\) and \(\mathsf{Cons}(q)\downarrow\) is evaluated true.

For a BNN \(\mathcal{N}\) given by \(f_{\mathcal{N}}=f_{n-1}\circ f_{n-2}\circ\cdots\circ f_{1}\circ f_{0}\), we denote by \(\mathcal{N}\in\mathscr{L}(\mathcal{A}_{\varphi})\) if the sequence of the Boolean functions \(f_{0},f_{1},\cdots,f_{n-1}\), regarded as a finite word, is accepted by the automaton \(\mathcal{A}_{\varphi}\).

Intuitively, \(\mathcal{N}\) accepts an input word iff it has an accepting run \(q_{0},q_{1}\cdots,q_{n}\), where \(q_{i}\) is constituted with a set of formulas that make the specification \(\varphi\) valid at the position \(i\). In this situation, \(I_{\varphi}\) refers to the states involving \(\varphi\) and \(q_{0}\in I_{\varphi}\). For the transition \(q_{i}\stackrel{{ f_{i}}}{{\longrightarrow}}q_{i+1}\), \(q^{\prime}_{i}\) and \(q^{\prime\prime}_{i}\) indicate the sets of formulas which should be satisfied in the next position \(i+1\) according to the semantics of _next_ (\(\mathsf{X}\)) and _weak next_ (\(\overline{\mathsf{X}}\)). Additionally, \(\mathsf{Cons}(q_{i+1})\) is obtained by applying the Boolean function \(f_{i}\) to the constraints in \(q_{i}\).

The following theorem reveals the relationship between \(\varphi\) and \(\mathcal{A}_{\varphi}\).
Theorem 4.1: _Let \(\mathcal{N}\) be a BNN given by a sequence of Boolean functions for a BLTL formula \(\varphi\), we have:_

\[\mathcal{N}\models\varphi\text{ if and only if }\mathcal{N}\in\mathscr{L}( \mathcal{A}_{\varphi})\text{.}\]

The proof is given in Appendix 0.A.1 and an example of the construction is given in Appendix 0.A.2.

### Tableau-Based Construction

We have successfully provided a process for converting an BLTL formula into an automaton on finite words. At first glance, it seems that the model checking problem w.r.t. BNN can be immediately boiled down to a word-problem of finite automata. Nevertheless, a careful analysis shows that this would result in a prohibitively high cost. Actually, for a BLTL formula \(\varphi\), the state set of \(\mathcal{A}_{\varphi}\) is \(\bigcup_{\Gamma\subseteq\mathsf{Sub}(\varphi)}\mathsf{Cl}(\Gamma)\subseteq 2^{ \mathsf{Sub}(\varphi)}\), thus the number of states is exponential in the size of the length of \(\varphi\). To avoid explicit construction, we provide an "on-the-fly" approach when performing synthesis.

Suppose the BLTL \(\varphi\) is given in NNF and the BNN \(\mathcal{N}\) is given as a sequence of Boolean functions \(f_{0},f_{1},\ldots,f_{n-1}\), using the following approach, we may construct a tree \(\mathcal{T}_{\varphi,\mathcal{N}}\) which fulfills the followings:

* \(\mathcal{T}_{\varphi,\mathcal{N}}\) is rooted at \(\langle 0,\{\varphi\}\rangle\);
* For an internal node \(\langle i,\Gamma\rangle\) with \(i<n-1\), it has a child \(\langle j,\Gamma^{\prime}\rangle\) only if there is a tableau rule \[\begin{array}{c|c}i&\Gamma\\ \hline j&\Gamma^{\prime}\end{array}\] where \(j\) is either \(i\) or \(i+1\).
* A leaf \(\langle i,\Gamma\rangle\) of \(\mathcal{T}_{\varphi,\mathcal{N}}\) is a (Modal)-node with \(i=n-1\), where nodes to which only the rule (Modal) can be applied are called (Modal)-nodes.

Tableau rules are listed in Figure 1. For the rule (Modal), we require that \(\Gamma\) consists of atomic formulas being of the form \(\mathbf{t}_{1}\sim\mathbf{t}_{2}\). In the rules (True) and (False), we require that \(\mathsf{len}(\mathbf{t}_{1}\sim\mathbf{t}_{2})=0\) and it is evaluated to true and false, respectively.

Suppose \(\langle n,\Gamma\cup\{\mathsf{X}\psi_{1},\ldots,\mathsf{X}\psi_{m}\}\cup\{ \overline{\mathsf{X}}\varphi_{1},\ldots,\overline{\mathsf{X}}\varphi_{k}\}\rangle\) is a leaf of \(\mathcal{T}_{\varphi,\mathcal{N}}\). We say it is _successful_ if \(m=0\) and \(\Gamma\downarrow\) is evaluated to true. In addition, we say a path of \(\mathcal{T}_{\varphi,\mathcal{N}}\) is _successful_ if it ends with a successful leaf, and no node along this path contains \(\perp\).

In the process of the on-the-fly construction, we start by creating the root node, then apply the tableau rules to rewrite the formulas in the subsequent nodes. In addition, before the rule (Modal) or (Or-\(j\)) is applied, we preserve the set of formulas, which allows us to trace back and construct other parts of the automaton afterward. We exemplify how to achieve the synthesis task via the construction in Section 5.

Theorem 4.2: \(\mathcal{N}\models\varphi\) _if and only if \(\mathcal{T}_{\varphi,\mathcal{N}}\) has a successful path._
Proof: Let \(\mathcal{A}_{\varphi}\) be the automaton corresponding to \(\varphi\). According to Theorem 2.1, it suffices to show that \(\mathcal{N}\in\mathscr{L}(\mathcal{A}_{\varphi})\) iff \(\mathcal{T}_{\varphi,\mathcal{N}}\) has a successful path.

Suppose, \(\mathcal{N}\) is accepted by \(\mathcal{A}_{\varphi}\) with the run \(q_{0},q_{1},\ldots,q_{n}\), we also create the root node \(\langle 0,\Gamma_{0}=\{\varphi\}\rangle\). Inductively, we have the followings statements for each node \(\langle i,\Gamma_{j}\rangle\) which is already constructed:

1. \(\Gamma_{j}\subseteq q_{i}\);
2. \(\mathcal{N},i\models\psi\) for each \(\psi\in q_{i}\) (see the proof of Thm. 2.1)

Then, if \(\langle i,\Gamma_{j}\rangle\) is not a leaf, we create a new node \(\langle i^{\prime},\Gamma_{j}^{\prime}\rangle\) in the following way:

* \(i^{\prime}=i\) if \(\langle i,\Gamma_{j}\rangle\) is not a (Modal)-node, otherwise \(i^{\prime}=i+1\);
* if rule (Or-\(k\)) (\(k=1,2\)) is applied to \(\langle i,\Gamma_{j}\rangle\) to some \(\varphi_{1}\vee\varphi_{2}\in\Gamma_{j}\), we require that \(\varphi_{k}\in\Gamma_{j}\); for other cases, \(\Gamma_{j}^{\prime}\) is uniquely determined by \(\Gamma_{j}\) and the tableau rule which is applied.

It can be checked that both Items 1) and 2) still hold at \(\langle i^{\prime},\Gamma_{j}^{\prime}\rangle\). Then, we can see that the path we constructed is successful since \(q_{n}\) is an accepting state of \(\mathcal{A}_{\varphi}\).

For the other way round, suppose that \(\mathcal{T}_{\varphi,\mathcal{N}}\) involves a successful path

\[\begin{array}{l}\langle 0,\Gamma_{0,0}\rangle,\langle 0,\Gamma_{0,1} \rangle,\ldots,\langle 0,\Gamma_{0,\ell_{0}}\rangle,\langle 1,\Gamma_{1,0} \rangle,\langle 1,\Gamma_{1,1}\rangle,\ldots,\langle 1,\Gamma_{1,\ell_{1}} \rangle,\ldots,\\ \langle i,\Gamma_{i,0}\rangle,\langle i,\Gamma_{i,1}\rangle,\ldots,\langle i, \Gamma_{i,\ell_{i}}\rangle,\ldots,\langle n,\Gamma_{n,0}\rangle,\langle n, \Gamma_{n,1}\rangle,\ldots,\langle n,\Gamma_{n,\ell_{n}}\rangle\end{array}\]

then, the state sequence \(q_{0},q_{1},\ldots,\ldots,q_{n}\) yields an accepting run of \(\mathcal{A}_{\varphi}\) on \(\mathcal{N}\), where \(q_{i}=\bigcup_{j=0}^{\ell_{i}}\Gamma_{i,j}\). 

## 5 BNN Synthesis

Let us now consider a more challenging task: Given a BTL specification \(\varphi\), to find some BNN \(\mathcal{N}\) such that \(\mathcal{N}\models\varphi\). In the synthesis task, the parameters of

Figure 1: Tableau rules for Automata Construction
the desired BNN are not given, even, we are not aware of the length (i.e., the number of blocks) of the network. To address this challenge, we leverage the tableau-based method (cf. Section 4.3) to construct the automaton for the given specification \(\varphi\) and check the existence of the desired BNN at the same time. But when performing the tableau-based rewriting, we need to view each block (i.e., a Boolean function) \(f_{i}\) as an unknown variable (called _block variable_ in what follows).

The construction of the tableau-tree starts from the root node \(\langle 0,\varphi\rangle\). During the construction, for each internal node \(\langle i,\Gamma\rangle\), the following steps are followed: Initially, rules other than (Or-1) and (Modal) are applied to \(\Gamma\) until no further changes occur. Then rule (Or-\(j\)) is applied to the disjunctions in the formula set, and we always first try rule (Or-1) when the rewriting is performed. Lastly, rule (Modal) is applied to generate node \(\langle i+1,\Gamma^{\prime}\rangle\), which becomes the next node in the path, and the Boolean function \(f_{i}\) used in the rewriting is just a block variable. Particularly, we retain a stack of formula sets on each of those either (Or-\(j\)) or (Modal) is applied for tracing back. Once an X-free (Modal)-node is reached, We verify the success of the path. However, since now the blocks are no longer concrete in this setting, an atomic formula of the form \(\gamma[f_{i},\ldots,f_{i+k}]\) cannot be immediately evaluated even if it is \(\rhd\)-free. As a result, whether a path is _successful_ cannot be evaluated directly.

To settle this, we invoke an integer different logic (IDL) solver to examine the satisfiability of the atomic formulas in the (Modal)-nodes along the path, and we declare success if all of them are satisfiable and it in addition ends up with an X-free (Modal)-node. Meanwhile, the model given by the solver would reveal hyper-parameters of the BNN, which then we adopt to obtain the expected BNN. For a node \(\langle i,\Gamma\rangle\), we call \(i\) to be the _depth counter_. Once the infeasibility is reported by the IDL solver, or some specific depth counter (call it the _threshold_) is reached, a trace-back to the nearest (Or-1) node is required: nodes under that node are removed, and then use (Or-2) for that, but this time we do not push anything into the stack, because both choices for the disjunctive formula have been tried so far. If no (Or-1) nodes remains in the stack when doing trace-back, we declare the failure of the synthesis.

Now, there are two issues to deal with during that process. The first is, how to determine if the aforementioned 'threshold' is reached; second, how can we convert the satisfiability testing into IDL-solving.

### The Threshold

There exists a naive bound for the first problem, which is just the state number of \(\mathcal{A}_{\varphi}\). However, this bound is in general not compact (i.e., doubly exponential in the size of the formula \(\varphi\)), and thus we provide another tighter bound.

We first define the following notion: We call two modal nodes \(\langle i,\Gamma\rangle\) and \(\langle j,\Gamma^{\prime}\rangle\) are _isomorphic_, denoted as \(\langle i,\Gamma\rangle\cong\langle j,\Gamma^{\prime}\rangle\), if \(\Gamma\) can be transformed into \(\Gamma^{\prime}\) under a (block) variable bijection. The following lemma about isomorphic model nodes is straightforward.
Lemma 1: _If \(\langle i,\Gamma\rangle\cong\langle j,\Gamma^{\prime}\rangle\) and \(\langle i,\Gamma\rangle\) could lead to a successful leaf (i.e., satisfiable leaf), then so does \(\langle j,\Gamma^{\prime}\rangle\)._

Thus, given \(\varphi\), the threshold can be the number of equivalence classes w.r.t. \(\cong\). To make the analysis clearer, we here introduce some auxiliary notions.

* We call an atomic constraint \(\gamma\) occurring in \(\varphi\) to be an _original constraint_ (or, _non-padded constraint_); and call a formula being of the form \(\gamma[f_{i},\ldots,f_{j}]\)_padded constraint_, where \(f_{i},\ldots,f_{j}\) are block variables.
* A (padded or non-padded) constraint with length \(0\) (i.e., \(\rhd\)-free) is called _saturated_. In general, such a constraint is obtained from a non-padded constraint \(\gamma\) via applying \(k\) layer variables, where \(k=\mathsf{len}(\gamma)\).

Theorem 5.1: _Let \(\varphi\) be a closed BLTL formula, and let_

* \(c=\#(\mathsf{Cons}(\boldsymbol{\Sigma})\cap\mathsf{Sub}(\varphi))\)_, i.e., the number of (non-padded) constraints occurring in_ \(\varphi\)_;_
* \(k=\max\{\mathsf{len}(\gamma)\mid\gamma\in\mathsf{Cons}(\boldsymbol{\Sigma}) \cap\mathsf{Sub}(\varphi)\}\)_, i.e., the maximum length of non-padded constraints occurring in_ \(\varphi\)_;_
* \(p\) _be the number of temporal operators in_ \(\varphi\)__

_then, \(2^{(k+1)c+p}+1\) is a threshold for synthesis._

The proof is shown in Appendix 0.A.3.

### Encoding with IDL Problem

Another problem is how to convert the satisfiability testing into SMT-solving. To tackle this, we present a method that transforms BLTL atomic formulas to IDL constraints.

We may temporarily view a Boolean function \(g:\mathbb{B}^{m}\to\mathbb{B}^{n}\) as a (partial) integer function with domain \([2^{m}]\), namely, we equivalently view \(g\) maps \(\mathsf{dec}(\boldsymbol{b})\) to \(\mathsf{dec}(g(\boldsymbol{b}))\).

For a \(\rhd\)-free term \(\boldsymbol{t}=(f_{k}\circ f_{k-1}\circ\cdots\circ f_{0})(\boldsymbol{b})\), we say that \((f_{i}\circ f_{i-1}\circ\cdots\circ f_{0})(\boldsymbol{b})\) is an _intermediate term_ of \(\boldsymbol{t}\) where \(i\leq k\). In what follows, we denote by \(\boldsymbol{T}\) the set of all intermediate terms that may occur in the process of SMT-solving, which is a part of synthesis that check the satisfiability of atomic formulas in successful leaves.

Remind that in a term or an intermediate term, a symbol \(g\) may either be a fixed function or a variable that need to be determined by the SMT-solver (i.e., _block variables_). To make it clearer, we in general use \(g_{0},g_{1},\ldots\) to designate the former functions, whereas use \(f_{0},f_{1}\), etc for the latter cases.

The theory of IDL is limited to handling the difference constraints of the form \(x-y\sim c\), where \(x\), \(y\) are integer variables and \(c\) is an integer constant. However, since functions occur in the terms, they cannot be expressed using IDL. To this end, we note that we merely care about partial input-output relations of the functions, which consist of mappings among \(\boldsymbol{T}\), and then the finite mappings can be expressed by integer constraints. Thus, for each intermediate term \(\boldsymbol{t}\in\boldsymbol{T}\), we introduce an integer variable \(v_{\boldsymbol{t}}\).

Then, all constraints describing the synthesis task are listed as follows.
1. For each BLTL constraints \(\mathbf{t}_{1}\sim\mathbf{t}_{2}\), we have a conjunct \(v_{\mathbf{t}_{1}}\sim v_{\mathbf{t}_{2}}\).
2. For each block variable \(f:\mathbb{B}^{n}\rightarrow\mathbb{B}^{m}\) and each \(f(\mathbf{t})\in\mathbf{T}\), we add the bound constraints \(0\leq v_{f(\mathbf{t})}\) and \(v_{f(\mathbf{t})}\leq 2^{m}\).
3. For each block variable \(f\) and every \(\mathbf{t}_{1},\mathbf{t}_{2}\in\mathbf{T}\), we have \(v_{\mathbf{t}_{1}}=v_{\mathbf{t}_{2}}\to v_{f(\mathbf{v}_{1})}=v_{f(\mathbf{v}_{2})}\), which guarantees \(f\) to be a mapping.
4. For every fixed function \(g\), we impose the constraint \(v_{g(\mathbf{t})}=\mathsf{dec}(g(\mathsf{bin}(v_{\mathbf{t}})))\) for every \(\mathbf{t}\in\mathbf{T}\).

Once the satisfiability is reported by the SMT-solver, we extract partial mapping information of \(f_{i}\)'s from the solver's model, by analyzing equations of the form \(v_{\mathbf{t}}=c\), where \(c\) is an integer called the value of \(\mathbf{t}\). We iterate over the model and record the value of terms, when we encounter an equation in the form of \(v_{f_{i}(\mathbf{t})}=c\), we query the value of \(\mathbf{t}\), and obtain one input-output relation of \(f_{i}\). Eventually, we get partial essential mapping information of suc \(f_{i}\)'s.

### Utilize the Synthesis

A BNN that satisfies the specification can be obtained via block-wise training, namely, training each block independently to fulfill its generated input-output mapping relations, which is extracted by the SMT-solver during the synthesizing process. Indeed, such training is not only in general lightweight, but also able to reuse the pre-trained blocks.

Let us now consider a more general requirement that we have both high-level temporal specification (such as fairness, robustness) and data constraints (i.e., labels on a dataset), and is asked to obtain a BNN to meet all these obligations.

A straightforward idea is to express all data constraints with BLTL, and then perform a monolithic synthesis. However, such a solution seems to be infeasible, because the large amount of data constraints usually produces a rather complicated formula, and it makes the synthesis extremely difficult.

An alternative approach is to first perform the synthesis w.r.t. the high-level specification, then do a retraining upon the dataset. However, the second phase may distort the result of the first phase. In general, one need to conduct an iterative cycle composed of synthesis-training-verification, yet the convergence of such process cannot be guaranteed. Thus, we need make a trade-off between these two types of specifications.

More practically, synthesis is used as an "enhancement" procedure. Suppose, we already have some BNN trained with the given dataset, then we are aware the hyper-parameters of that. This time, we have more information when doing synthesis, e.g., the threshold is replaced by the length of the network, and the shape (i.e., the width of input and output) of each block are also given. With this, we may perform a more effective SMT-solving process, and then retrain each block individually. Definitely, this might affect the accuracy of network, and some compromise also should be done.
## 6 Experimental Evaluation

We implement a prototype tool in Python, which uses Z3 [9] as the off-the-shelf IDL solver and PyTorch to train blocks and BNNs. To the best of our knowledge, few existing work on synthesizing BNN has been done so far. Hence, we mainly investigate the feasibility of our approach by exploring how much the trustworthiness of BNN can be enhanced, and the corresponding trade-off on accuracy degradation. The first two experiments focus on evaluating the effectiveness of synthesis in enhancing the properties of BNNs We set BNNs with diverse architectures as baselines, and synthesize models via the "enhancement" procedure, wherein the threshold matches the length of the baselines, and the shape of blocks are constrained to maintain the same architecture as the baselines. Eventually, the blocks are retrained to fulfill the partial mapping, and the synthesized model is obtained through retraining on the dataset. We compare the synthesized models and their baselines on two properties: _local robustness_ and _individual fairness_.

Moreover, we study the potential of our approach to assist in determining the network architecture.

Datasets.We train models and evaluate our approach over two classical datasets, MNIST [10] and UCI Adult [11].

MNIST is a dataset of handwritten digits, which contains 70,000 gray-scale images with 10 classes, and each image has \(28\times 28\) pixels. In the experiments, we downscale the images to \(10\times 10\), and binarize the normalized images, and then transform them into 100-width vectors.

UCI Adult contains 48,842 entries with 14 attributes, such as age, gender, workclass and occupation. The classification task on the dataset is to predict whether an individual's annual salary is greater than 50K. We first remove unusable data, retain 45,221 entries, and then transform the real-value data into 66-dimension binarized vectors as input.

Experimental Setup.In the block-wise training, different loss functions are employed for internal and output blocks: the MSE loss function for internal blocks and the cross-entropy loss function for output blocks. The training process entails a fixed number of epochs, with 150 epochs for internal blocks and 30 epochs for output blocks. The experiments are conducted on a 3.6G HZ CPU with 12 cores and 32GB RAM, and the blocks and BNNs are trained using a single GeForce RTX 3070 Ti GPU.

\begin{table}
\begin{tabular}{c c c|c c c} \hline \hline
**Name** & **Arch** & **Acc** & **Name** & **Arch** & **Acc** \\ \hline
**R1** & 100-32-10 & 82.62\% & **F1** & 66-32-2 & 80.12\% \\
**R2** & 100-50-10 & 84.28\% & **F2** & 66-20-2 & 79.88\% \\
**R3** & 100-50-32-10 & 83.50\% & **F3** & 66-32-20-2 & 78.13\% \\ \hline \hline \end{tabular}
\end{table}
Table 1: BNN baselines.
Baseline.We use six neural networks with different architectures as baselines, where three models **R1**-**R3** are trained on the MNIST for 10 epochs with a learning rate of \(10^{-4}\) to study on local robustness. For individual fairness, we train 3 models (**F1**-**F3**) on the UCI Adult for 10 epochs, with a learning rate of \(10^{-3}\), and split the dataset into a training set and a test set in a 4:1 ratio.

The detailed information is listed in Table 1, Column (Name) indicates the name of BNNs, and Column (Arch) presents their architectures. The architecture of each network is described as by a sequence \(\{n_{i}\}_{i=0}^{s}\), where \(s\) is the number of the blocks in the network, and \(n_{i}\) and \(n_{i+1}\) indicate the input and output dimensions of the \(i\)-th block. For instance, 100-32-10 indicates that the BNN has two blocks, the input dimensions of these blocks are 100 and 32 respectively, and the number of classification labels is 10. Column (Acc) shows the accuracy of the models on the test set.

### Local Robustness

In this section, we evaluate the effectiveness of our approach for enhancing the robustness of models in different cases. We use the metric, called Adversarial Attack Success Rate (ASR), to measure a model's resistance to adversarial attacks. ASR is calculated as the proportion of perturbed inputs that leads to a different prediction result compared to the original input.

We choose 30 image vectors from the training set, and set the maximum perturbation to four levels, \(\epsilon\in\{1,2,3,4\}\). The value of \(\epsilon\) indicates the number of positions that can be modified in one image vector. One selected input vector, one maximum perturbation \(\epsilon\) and one baseline model constitute a case, resulting in a total of 360 cases.

For each of the 360 case, we make a synthesized model individually, and compare its ASR with the corresponding baseline. For the local robustness property (cf. Section 3.2), since the input space is too large to enumerate, we need to sample inputs within \(B\left(\mathbf{u},\epsilon\right)\) when describing the specification, which is formulated as \(\bigwedge_{i=1}^{k}\left(\mathcal{N}(\mathbf{u})=\mathcal{N}(\mathbf{b}_{i})\right)\), where each \(\mathbf{b}_{i}\) is a sample and \(k\) is the number of samples. We here sample 100 points within the maximum perturbation limit \(\epsilon\). The specification is written as \(\bigwedge_{i=1}^{k}\left(\rhd^{n}\mathbf{u}=\rhd^{n}\mathbf{b}_{i}\right)\), where \(n\) is the number of the block of the baseline. Subsequently, we use the block constraint (cf. Section 5.2), \(0\leq v_{f_{i}(\mathbf{t})}\leq 2^{m}\), to specify the range of output of each block. To make the bound tighter, we retain the maximal and minimal activations of each block using calibration data run on the baseline, and then take the recorded values as bounds. Eventually, the generated mappings are used in the block-wise training, and then the enhanced BNN is obtained through retraining on the MNIST dataset.

We also take 100 samples for each case and compare the ASR for baselines and their synthesized counterparts. The results are shown in Figure 2, blue bars represent the baselines, while orange bars represent synthesized models. We use the sign + to denote the synthesized models. Figure 2(a) (resp. Figure 2(b) and Figure 2(c)) depicts the percentage of average ASR of **R1** (resp. **R2** and **R3**) and the counterpart **R1+** (resp. **R2+** and **R3+**) (the vertical axis), with different
\(\epsilon\) (1, 2, 3, 4) (the horizontal axis). The results demonstrate a decrease in ASR by an average of 43.45%, 22.12%, and 16.95% for **R1**, **R2** and **R3**, respectively.

Whist the models' robustness are enhanced, their accuracy are slightly decreased. Table 2 shows the results of the accuracy of the models, where Acc+ represents the average accuracy for synthesized models with the same architectures.

### Individual Fairness

In this section, we investigate the individual fairness w.r.t two sensitive feature, namely sex (Male and Female) and race (White and Black) on the UCI Adult dataset.

We consider **F1**-**F3** as baselines, and randomly select 1000 entries for both **F1** and **F2**, and 200 entries for **F3** from the training set, and then generate proper pairs by modifying the value of the sensitive attribute while keeping all other attributes the same. For example, we modify the value of Male to Female. After forming specifications using the approach mentioned in Section 3.2 with the pairs, we proceed with the "enhancement" procedure and retraining to obtain the synthesized models. We then evaluate the models on the test set by the measuring the fairness score. We count the number of the fair pairs (the pairs only differ in the sensitive attribute, and get the predication): _fair num_, and compute the fairness score, \(\frac{\textit{fair num}}{\textit{test size}}\), where _test size_ is the size of the test set.

\begin{table}
\begin{tabular}{c c c c} \hline \hline  & **R1** & **R2** & **R3** \\ \hline Acc & 82.62\% & 84.28\% & 83.50\% \\ Acc+ & 81.33\% & 81.72\% & 78.75\% \\ \hline \hline \end{tabular}
\end{table}
Table 2: The average accuracy of **R1**-**R3** and their synthesized models.

Figure 2: Results of local robustness.
The results are listed in Table 3, where the baselines and the sensitive attributes shown in Column 1,2. Column 3,4 (Acc/Acc+) demonstrate the accuracy of baselines and synthesized models, and Column 5,6 (Fair/Fair+) show their fairness scores. The figure shows that the all models' individual fairness is significantly improved, with some even reach reaching 100% (Row 2, the fairness score increase from 92.92% to 100%). However, the enhancement is accompanied by the accuracy lost, Column 3,4 show that all models suffer from a certain degree of accuracy decrease. Our tool efficiently synthesized the hyper-parameters within a few minutes, as shown in Column 7.

Furthermore, we examine the ability of our approach on helping determine the architecture of the BNNs. For both sex and race, we sample 200 entries in the training set to generate proper pairs, and formulate the specification without using the bound constraints or fixing the number of block, as follows,

\[\mathsf{F}(\bigwedge_{i}^{k}(\mathbf{x}_{i}=\mathbf{y}_{i}))\wedge(\bigwedge_{i}^{k}( \mathbf{x}_{i}=\rhd^{2}\mathbf{a}_{i}\wedge\mathbf{y}_{i}=\rhd^{2}\mathbf{b}_{i})\vee(\bigwedge_ {i}^{k}(\mathbf{x}_{i}=\rhd^{3}\mathbf{a}_{i}\wedge\mathbf{y}_{i}=\rhd^{3}\mathbf{b}_{i})))\]

where \((\mathbf{a}_{i},\mathbf{b}_{i})\) is the proper pair, and \(k\) is the number of samples. The formula indicates the presence of consecutive blocks in the model, with a length of either 2 or 3. For each proper pair \((\mathbf{a}_{i},\mathbf{b}_{i})\), their respective outputs \((\mathbf{x}_{i},\mathbf{y}_{i})\) must be equal.

After synthesizing the partial input-output relation of \(f_{i}\)s,we determine the length of the network by selecting the maximum \(i\) among \(f_{i}\)s. The dimensions of the blocks are set to the maximum input and output dimensions in the partial relation obtained for the corresponding \(f_{i}\).

We make a slight adjustment to the synthesis framework, when find a group of hyper-parameters, we continue searching for one more feasible group, resulting

\begin{table}
\begin{tabular}{c c c c c c} \hline \hline
**Attr** & **Arch** & **Len** & **\#Mapping** & **Acc** & **Fair** \\ \hline sex & 66-10-10-2 & 3 & 1117 & 74.38\% & 99.51\% \\ sex & 66-8-2 & 2 & 559 & 74.69\% & 99.72\% \\ race & 66-9-8-2 & 3 & 952 & 74.38\% & 94.59\% \\ race & 66-8-2 & 2 & 567 & 74.13\% & 99.71\% \\ \hline \hline \end{tabular}
\end{table}
Table 4: The synthesized models which architecture are given by our tool.

\begin{table}
\begin{tabular}{c c c c c c c} \hline \hline
**Model** & **Feature** & **Acc** & **Acc+** & **Fair** & **Fair+** & **Synthesis Time(s)** \\ \hline
**F1** & sex & 80.12\% & 74.53\% & 92.91\% & 99.94\% & 241.67 \\
**F1** & race & 80.12\% & 74.54\% & 92.92\% & 100\% & 216.46 \\
**F2** & sex & 79.88\% & 75.71\% & 95.68\% & 97.83\% & 215.61 \\
**F2** & race & 79.88\% & 75.18\% & 94.64\% & 98.47\% & 212.46 \\
**F3** & sex & 78.13\% & 74.48\% & 89.67\% & 99.83\% & 90.39 \\
**F3** & race & 79.88\% & 74.09\% & 89.16\% & 98.27\% & 95.75 \\ \hline \hline \end{tabular}
\end{table}
Table 3: Results of individual fairness.
in two groups of hyper-parameters for sex and race. We showcase the synthesized models in Table 4. Column 1 indicates the sensitive attribute of interest, and Column 2,3 display the architecture and the length of the BNNs respectively. Column 4 shows the number of partial mappings we obtained in the synthesis task. Our tool successfully generates models with varying architectures and high individual fairness, which are presented in the Column 5,6 respectively.

## 7 Conclusion

In this paper, we have presented an automata-based approach to synthesizing binarized neural networks. Specifying BNNs' properties with the designed logic BLTL, and using the tableau-based construction approach, the synthesis framework determine hyper-parameters of BNNs and relations among some parameters, and then we may perform a block-wise training. We implemented a prototype tool and the experiments demonstrate the effectiveness of our approach in enhancing the local robustness and individual fairness of BNNs. Although our approach have shown the feasibility of synthesizing trustworthy BNNs, there is still a need to further explore this line of work. In the future, beyond the input-output relation of BNNs, we plan to focus on specifying properties between the intermediate blocks. Additionally, we aim to extend the approach to handle the synthesis task of multi-bits QNNs.

#### Acknowledgements

This work is partially supported by the National Key R & D Program of China (2022YFA1005101), the National Natural Science Foundation of China (61872371, 62072309, 62032024), CAS Project for Young Scientists in Basic Research (YSBR-040), and ISCAS New Cultivation Project (ISCAS-PYFX-202201).
