Truth Table Net: Scalable, Compact & Verifiable Neural Networks with a Dual Convolutional Small Boolean Circuit Networks Form

1 Introduction

DNNs' success in various machine learning tasks has been remarkable [Goodfellow et al., 2016], but their opacity has raised concerns about their security [AI, 2023; Commission, 2021], necessitating the development of formal verification processes to ensure safety and reliability [Driscoll, 2020]. Formal verification employs mathematical techniques to prove that a system satisfies predefined properties; however, the complexity of DNNs poses significant challenges for verification [Wang et al., 2021; Brix et al., 2023]. Traditional DNNs struggle to simultaneously achieve scalability, verifiability, and compactness in terms of logic gates [Petersen et al., 2022]. Ideally, a natural goal is to design a DNN that can be transformed into a compact Boolean logic circuit without sacrificing high accuracy on large-scale datasets. This approach holds the potential to enhance the compactness of DNNs and facilitate their verification processes [Jia and Rinard, 2020].

Our approach. DNNs, similar to ciphers, represent complex black-box functions that must be trustworthy. Drawing inspiration from a popular design principle of symmetric-key encryption algorithms (so-called Substitution-Permutation Networks or SPN [Daemen and Rijmen, 2002]), our paper proposes compact and small learnable filter Convolutional Neural Networks (CNNs) equivalent by design into small truth tables (from 6 to 16 bits of input). To achieve that goal, we adopt a divideand-conquer strategy. In the divide phase, before training, we reduce the input size of each DNN building block function, enabling the computation of its complete distribution within a practical time, independent of its overall architecture. In the conquer phase, after training, we compute the complete distribution of each building function.

Therefore, our objective is to design DNNs based on functions that allow for full distribution computation within a practical timeframe, independent of the overall architecture, all while maintaining accurate performance on large datasets.

1.1 Our Contributions And Claims

The LTT filter. To address this challenge, our paper introduces a novel filter function called the Learning Truth Table (LTT) filter. The LTT filter serves as the fundamental building block function of TTnet, similar to how a CNN filter is utilized in a DCNN. The LTT filter is defined based on three key rules and presents six attractive properties, see Section 4.1.

The TTnet architecture. LTT layers are assembled into a TTnet in the same way that CNN filters are assembled into DCNNs. Specifically, LTT filters are stacked together in LTT layers, and these LTT layers are stacked together in the overall TTnet. The final classification layer is linear.

Claim on scalability. In contrast to previous differentiable logic DNN solutions, TTnet demonstrates remarkable scalability, achieving performance comparable to other DNNs based on Boolean functions on the ImageNet classification task. For a fair comparison, we specifically evaluated TTnet against XnorNet [Rastegari et al., 2016] and the Binary Neural Networks (BNNs) original paper [Hubara et al., 2016], both of which are also based on Boolean functions. The results showcase that TTnet, which is a differentiable convolutional logic gate DCNN as well as a Boolean function, can effectively scale to large-scale datasets like ImageNet, achieving competitive performance (claim 1).

Claims on compactness. TTnet stands as the pioneering differentiable DCNN that can be transformed into a Boolean logic circuit by design (claim 2), which was already identified as an open problem [Petersen et al., 2022]. Empirical evaluation on small datasets like tabular datasets (Adult and Breast Cancer) and MNIST reveals that TTnet is equivalent to state-of-the-art differentiable logic gate DNN (Diff Logic Net [Petersen et al., 2022]) in terms of compactness and accuracy (claim 2A). Furthermore, at the cost of higher complexity, TTnet exhibits superior accuracy and training time scalability, achieving a notable accuracy of 70.75% on CIFAR-10 with less than an hour of training, marking an +8% improvement and ×90 faster training compared to Diff Logic Net [Petersen et al., 2022] (claim 2B).

Claims on formal verification. As a demonstration of its excellent scalability/compactness profile, we show that TTnet is very well suited to support fast property verification using generic SAT solvers (claim 3). This allows for the formal verification of the network's robustness in dozens of milliseconds on MNIST and CIFAR-10, which is about 104 times faster than α - β-Crown [Xu et al., 2020; Wang et al., 2021], the state-of-the-art DNN verification solver and a recent winner of the Verification Neural Network (VNN) competition [Brix et al., 2023] (claim 3A). We also provide a comparison with BNNs verification [Jia and Rinard, 2020; Narodytska et al., 2019]: our method is more robust in low-noise cases and faster to verify in all scenarios, for MNIST/CIFAR-10 (claim 3B).

Outline. Section 2 presents a literature review on Boolean logic gates DNN and DNN formal verification. Section 3 provides a comprehensive overview of the background in the field of Boolean logic and formal verification. Section 4 describes the design principles and architecture of the TTnet model. In Section 5, we provide a thorough evaluation of the performance of our model on various datasets, carefully demonstrating the above claims. Finally, we discuss the limitations and opportunities in Section 6, and conclude in Section 7.

2 RelatedWorks

Binary and Sparse Neural Networks. BNNs are DNN architectures where the activations and weights within a neural network use binary states, typically representing {-1, +1}. This innovative technique allows for the approximation of computationally expensive matrix multiplications through faster XNOR and bitcount (popcount) operations. BNNs are characterized primarily by their weights. Sparse Neural Networks (SNNs) represent another approach to neural network design. In SNNs, only a subset of connections is present, in contrast to fully-connected layers. In the SNNs literature, the primary focus often revolves around distilling a sparse neural network from a dense one, with careful consideration given to the choice of connections. However, recent research has suggested the high efficacy of using randomized and fixed sparse connections from the outset. In our experiments, we include BNNs and SNNs as baseline models, due to their exceptional inference speed performance.

DNNs into compact logic gate circuit representation. [Chatterjee, 2018] proposed a DNN based on truth tables, but it did not scale beyond MNIST. Other works aimed to convert DNNs into compact Boolean logic circuit designs, which are essential for deploying DNNs on resource-constrained devices [Wang et al., 2019]. However, the challenge in learning logic gate networks is that they are typically non-differentiable, making them difficult to train with gradient descent [Rumelhart et al., 1986]. To date, there is no family of differentiable DCNNs logic gates, as stated by [Petersen et al., 2022]and our LTT filter function is proposed as a possible bridge to that gap between symbolic AI and trainable DCNNs.

Exact, complete, and sound formal verification. Formal verification is a critical aspect in ensuring the DNN's soundness and completeness properties, particularly for safetycritical applications [Driscoll, 2020]. Conventional verifiers work with real-valued networks, but they face scalability challenges, e.g. hundreds of seconds to verify an MNIST image property [Müller et al., 2022], and provide no guarantees of correctness due to floating point errors [Jia and Rinard, 2021]. Therefore, developing an efficient DNNs verification process is an important topic, as evidenced by the α - β-Crown paper [Xu et al., 2020; Wang et al., 2021] and winner of the VNN competition [Brix et al., 2023]. In the present work, instead of designing a new general verification method for DNNs, we propose the first architecture that can be efficiently and correctly verified with any SAT solver [Roussel and Manquinho, 2009]. This research direction is attracting interest, as exemplified by [Jia and Rinard, 2020], who strives to show that BNNs [Hubara et al., 2016] are faster to verify if a specific well-crafted SAT solver is designed. Further discussion regarding incomplete methods is given in Appendix.

Local features for accurate DNN. Recent works by [Brendel and Bethge, 2018] and [Agarwal et al., 2021] experimentally showed that highly nonlinear functions (Resnet for the former, expanding autoencoder for the latter) can enable a DNN to learn high-quality local features (7 × 7 floating input pixels on image dataset for the former, 1 × 1 floating input on tabular dataset for the latter). In this work, we build upon the idea of using highly nonlinear functions to learn local features.

However, instead of processing local-dimensional floatingpoint inputs, TTnet reduces the local features to binary inputs (n ≤ 16). These two approaches legitimize our use of TTnet on tabular and image datasets and highlight the importance of Rule 3 in Section 4.1.

3 Background

Boolean logic. A truth table is a mathematical representation of the output of a Boolean function for all possible input combinations. It is usable in practice when the corresponding Boolean function distribution is fully computable. Note that the Boolean function distribution of a DNN/BNN is not fully computable, as the input size of the function is too large. A truth table can be expressed in CNF 1 , being the standard form to represent a Boolean function, especially in formal verification. A Boolean logic circuit is a physical or mathematical representation of a Boolean function, made up of interconnected logic gates [Arora and Barak, 2009; Klir et al., 1997], typically AND/OR gates.

Formal verification. Our framework is built upon [Narodytska et al., 2019], a theoretical exact sound and complete framework to verify any property. Given a precondition prec on inputs x, the property prop, on outputs o, and the SAT relations provided by a DNN between inputs and outputs denoted as DNN(x, o), we assess the validity of the statement prec(x) ∧DNN(x, o) =⇒ prop(o). To show the existence of a counter-example to this robustness property, we search for a satisfying assignment of prec(x) ∧ DNN(x, o) ∧ prop(o) (Eq1) with a proven SAT solver. An "unsat" result from the SAT solver proves no noise exists for satisfying (Eq1) and therefore no noise can attack; on the opposite, a "sat" answer proves that there is one noise that satisfies (Eq1) to attack the DNN. In that case, the noise is given by the SAT solver and then tested for validation. In this paper, one distinguishes the traditional natural accuracy from the verified accuracy, the latter measuring the fraction of predictions that remain correct for all adversarial attacks within the perturbation constraints.

4 Truth Table Neural Networks

First, we define LTT filters, give their properties, and illustrate their use with an example in Section 4.1. We then explain how these LTT filters are integrated into TTnet in Section 4.2. We also provide a companion video in Supplementary Material.

4.1 Overall LTT Filter Design

General Design Criteria And Rules Of LTT Filters.

We aim to develop a novel filter function, called the Learning Truth Table (LTT) filter, that is comparable to traditional CNN filters in terms of computational efficiency 2 but differs in complexity. Specifically, we design an LTT filter such that one of its main characteristics is to be a grouped CNN filter: it will be sparser in connectivity than a classical CNN filter. The LTT filter essential criteria are:

1 CNF is a conjunction of disjunctions of literals, for example Ω = (c1 ∧ · · · ∧ cm), with each clause cj = (lj1 ∨ · · · ∨ ljr) and where (lj1, . . . , ljr) are Boolean literals.

2 We define the computational efficiency in binary operations, denoted as OPs, as the total number of binary gates (NAND/NOR/AND/OR/XOR/XNOR) required to represent the entire DNN in Boolean logic gate format; and the floating-point operations counterpart denoted as FLOPs

(A) The LTT filter distribution must be entirely computable in practical time, independently of the overall DNN architecture. (B) Once LTT filters are assembled into a layer and layers into a DNN, the latter should be scalable, especially on large datasets such as ImageNet.

To achieve that, we define three LTT filter design rules:

• Rule 1: Force the input bit size n of the LTT filter to be n ≤ 16, independently of the architecture.

Rule 2: Use binary inputs/outputs, but with real-valued weights and intermediate values.

Rule 3: Ensure that the LTT filter uses nonlinear functions in between the Heaviside activations.

As a result, each filter in our architecture becomes a truth table with a maximum input bit size of 16, leading to a compact DNN represented as a Boolean logic gate circuit that is easy to train and verify. We explore these benefits in Section 5.

Regular 2D-Convolution Filters.

We first define below a traditional 2D-Convolution filter.

Definition 1. Let an input X ∈ RCin×H×W where Cin, H, W represent the number of channels, height, and width of a channel respectively. If a regular convolution filter is applied on X with kernel size k × k, group G, stride s = 1 padding p = 0, the output is denoted as O ∈ RCout×H×W where every output unit oij ∈ RCout is:

with ∪ the concatenation operation and unit oγij ∈ RCout/G representing the output in group γ at position i, j. Namely:

where i ∈ {1, . . . ,H}, j ∈ {1, . . . ,W}, γ ∈ {1, . . . ,G}, with the input xγ(i+u,j+v) ∈ RCin/G and the convolution filter weights ωγu,v ∈ R(Cin/G)×(Cout/G) .

Property 2. Given that the set of inputs (xγi,j , . . . , xγi+k-1,j+k-1 ) is encoded on q bits, the complete distribution of one 2D-CNN filter of function Ψωγ can be computed in 2q×k×k×(Cin/G) operations. Furthermore, the weights ωγ are real and learnable using gradient descent.

Definition of LTT filters. We aim to significantly reduce the complexity of the 2D-CNN filter, by designing a function whose input bit size q × k × k × (Cin/G) is smaller than 16. We now define LTT filters as below.

Definition 3. Let an input X ∈ {0, 1}Cin×H×W where Cin, H, W represent the number of channels, height, and width of a channel respectively. Let the group and the kernel size parameters be such that G = Cin/n and k2 ≤ 16/n, n ∈ {1, 4, 16}). We define two convolutions filter weights ωγ 1 ∈ Rk1×k1×(Cin/G)×(a×Cout/G) and ωγ 2 ∈ Rk2×k2×(a×Cout/G)×(Cout/G) with both stride 1, no padding

(b) LTT overview in one dimension. The intermedi-

ate values and the weights (ω1, ω2) are real and the

input/output values are binary. binact: Heaviside

step function defined as:

binact(x) = (1 + sgn(x))/2 with x ∈ R.

Figure 1: A Learning Truth Table (LTT) filter example in one dimension.

and such that k1 + k2 - 1 = k and a is the amplification ratio. We also define Θ to be a nonlinear function. The LTT output is denoted as O ∈ RCout×H×W where every output unit oij ∈ RCout is defined as in Equation (1). Unit oγij ∈ RCout/G, the output in group γ at position i, j is given by

with Ψωγ defined as in Equation (2) and αγ i,j ∈ Ra×Cout/G as

where i ∈ {1, . . . ,H}, j ∈ {1, . . . ,W}, γ ∈ {1, . . . ,G} and with the input xγ(i,j) ∈ RCin/G.

By definition, the described LTT filters validate the three rules given previously. In Figure 1a, we provide an example of an LTT computation in one dimension for k1 = 3, k2 = 2, k = k1 + k2 - 1 = 4, a = 4,Cin = 1,Cout = 1 and Θ = ReLU. The architecture is depicted in Figure 1b.

LTT Filters Properties.

We point six main LTT properties. Properties P1 and P2 of the proposed TTnet architecture offers practical benefits, including fast and scalable filter training. Meanwhile, properties P3, P4, P6 lead to the development of compact LTT filters and efficient verification techniques. Figure 2 provides an example of the two forms of P5.

Example: From LTT Weights To Truth Table To CNF.

Consider a trained 1D-LTT Φω1,ω2 with input size n = 4, a stride of size 1, and no padding. The architecture of Φω1,ω2 , given in Figure 1b, is composed of two CNN filter layers: the first one has parameters ω1 with (input channel, output channel, kernel size, stride) = (1, 4, 3, 1), while the second ω2 = (4, 1, 2, 1). The values of the weights (ω1, ω2) are given in Figure 2. The inputs and outputs of Φω1,ω2 are binary, and we denote the inputs as [x0, x1, x2, x3]. To compute the entire distribution of Φω1,ω2 , we generate all 24 = 16 possible input/output pairs, as shown in Figure 1a, and obtain the truth table in Figure 2. This truth table fully characterizes the behavior of Φω1,ω2 . We then transform the truth table into an optimal CNF using the Quine-McCluskey algorithm [Blake, 1938; Udovenko, 2023]. This optimal CNF fully characterizes the behaviour of Φω1,ω2 as well and is exactly equivalent.

• P1: The LTT filter weights (ω1, ω2) are trainable with gradient descent and the Straight-Through Estimator (STE) to handle the input/output binarisation.
• P2: The LTT filter preserves real-valued weights (ω1, ω2) and intermediate values α.
• P3: The entire distribution of the LTT filter can be calculated in 2n ≤ 216 = 65, 536 operations (less than 1 ms on a standard PC). Truth table input bit size n is independent of the architecture.
• P4: The Quine-McCluskey algorithm [Blake, 1938] can be used to compute the optimal CNF (in terms of Boolean logic gates) from the LTT truth table if n ≤ 12. For 12 < n ≤ 16 a compact CNF can be computed [Udovenko, 2023].
• P5: The LTT filter has two forms: neural network weights (ω1, ω2), or a small Boolean circuit (as a truth table or as Boolean logic gates).
• P6: Under truth table or CNF form, an LTT evaluation does not need to compute any activation function.

4.2 Overall TTnet Design

We integrated LTT filters into the neural network, just as CNN filters are integrated into a deep convolutional neural network: each LTT layer is composed of multiple LTT filters and there are multiple LTT layers in total (see Figure 2). Additionally, there is a pre-processing layer and a final layer, which provide flexibility in adapting to different applications: scalability, formal verification, and logic circuit design.

5 Results

Experimental environment. The project code can be found in Supplementary Material and was coded in Python with PyTorch library [Paszke et al., 2019] for training, Numpy [Van Der Walt et al., 2011] for testing as we infer with truth tables. We used 4 Nvidia GeForce RTX 3090 GPUs and 8 cores Intel(R) Core(TM) i7-8650U CPU clocked at 1.90 GHz, 16 GB RAM. We note TTnetn-k a TTnet with truth tables of input bit size n, without pre-processing layer and a final linear layer with weights quantized on k bits; and TTnetn-|k, with a pre-processing layer of one CNN layer with floating weights.

5.1 Claim 1: Scalability

TTnet16-|8 shows an accuracy of 41.6% on ImageNet with truth tables of size n = 16. These results are comparable to those achieved by the original BNN paper [Hubara et al., 2016] and XnorNet [Rastegari et al., 2016], see Table 1. Our experimental results confirm that TTnet achieves high accuracy on a large dataset, which proves its non-trivial nature. We emphasize that other differentiable logic gate networks did not scale to ImageNet so far: the work done by [Petersen et al., 2022] does not scale to larger datasets than CIFAR-10. However, we believe there remains room for improvement on TTnet in terms of accuracy as BNNs now can achieve ≈ 70% - 75% [Liu et al., 2018] on ImageNet. Detailed architecture/training information are given in Appendix.

Table 2 studies the influence of the input bit size n of the truth table on the scalability for CIFAR-10.

5.2 Claims 2: Compactness

We provide experimental evidence to support our claim of providing easy-to-train, accurate, and compact logic gate DCNNs. The results are presented in Table 3 for tabular datasets (Adult and Breast Cancer) and Table 4 for image datasets (MNIST and CIFAR-10) along with comparisons with state-of-the-art differentiable logic gate DNN [Petersen et al., 2022], BNNs [Umuroglu et al., 2017; Hirtzlin et al., 2019] and SNNs [Molchanov et al., 2017; Mocanu et al., 2018; Han et al., 2016; Zeng and Urtasun, 2018; Zhou et al., 2021]. More information on training conditions, architectures, and additional comparisons can be found in Appendix.

A FLOP (FLoating point OPerations) is typically composed of multiple binary operations (OPs). Float32 adders/multipliers require around 1,000 logic gates or lookup tables and have a significant delay. They are commonly implemented in CPU and GPU hardware due to their importance. However, they are much more expensive than simple calculations or bitwise logical operations on int64 data types. Processors can perform 3 to 10 int64 bitwise operations per cycle, while floating-point operations usually take a full clock cycle. Converting a non-sparse model assumes a conservative estimate of 1000 OPs per 1 FLOP. Neural networks' speeds are theoretical, with sparse execution often being 10 to 100 times slower. In practice, 1,000 binary OPs for 1 clear FLOP (float32) is a conservative estimate for SNNs. It's also a cautious estimate for sparse float32 models. Theoretical estimates assume no density cost and no hardware acceleration for floating-point operations [Petersen et al., 2022].

Performances discussion - small datasets. We present a comparison between two methods, TTnet6-4 and Diff Logic Net, with respect to accuracy and compactness on small datasets. Compactness is defined in terms of the number of Boolean logic gates (NAND/NOR/AND/OR/XOR/XNOR) used by the models, noted as OPs. Our results in Table 3 demonstrate that TTnet6-4 outperforms Diff Logic Net in terms of accuracy for both tabular datasets, while using much fewer gates. On the MNIST dataset, as indicated in Table 4 (top table), both models achieve comparable accuracies (10% maximum relative error rate), but TTnet6-4 utilizes fewer operations. In summary, our findings show that TTnet and Diff Logic Net have similar performance on small datasets, with TTnet offering the advantage of compactness in terms of number of logical gates.

Performances discussion - large dataset. We compare again TTnet6-4 and Diff Logic Net, but on the CIFAR-10 dataset, specifically focusing on scalability in terms of accuracy, training time, and model compactness. As shown in Table 4 (bottom table), for the small model, Diff Logic Net exhibits higher compactness with comparable accuracy than TTnet. On the other hand, when considering larger models, TTnet achieves an accuracy of 70.75% while Diff Logic Net shows a maximum of 62.14%. The superior scalability of TTnet in terms of accuracy is achieved at the cost of a more complex Boolean logic circuit.

To investigate the impact of relaxing the compactness constraint, we demonstrate that TTnet12-|4 can achieve an accuracy of 84.63% with 1.2G OPs. As the dataset gets larger and more complex, the complexity of the Boolean circuit needs to increase as well to maintain high accuracy. This is achievable with TTnet due to its scaling training properties.

Indeed, TTnet is notably easier to train than Diff Logic Net: TTnet6-4 achieves an accuracy of 70% in under 1 hour of training and TTnet12-|4 reaches 84.63% after 20 hours (on an NVIDIA GeForce RTX 3090 GPU), while the Diff Logic Net requires 90 hours of training (on a single NVIDIA A6000 GPU) to reach a 62.14% accuracy. We note these two GPUs are equivalent in terms of image training time, see Supplementary Material. The accuracy achieved by TTnet on CIFAR-10, along with its effective training, underscores its potential as a differentiable CNN logic gate architecture.

5.3 Claim 3: Complete, Sound Formal Verification

Greater Boolean logic compactness in circuit design can aid formal verification by reducing the complexity of the verification process. Therefore, we applied TTnet to formal verification, where two strategies are common: either using a specific solver to verify ReLU based-DNN like β-Crown [Wang et al., 2021], or using a specific architecture that allows a generic verification method. We compared both methods based on natural accuracy, verified accuracy for l∞-norm bounded input perturbations (formal definition in Appendix.For a fair comparison, we note that our pre-processing layer and training configuration are the same as [Jia and Rinard, 2020]. More results and discussions can be found in Appendixee.

Strategy 1: Comparison with general DNN solvers. In Table 5, we present a comparison of our proposed verification strategy, which utilizes the TTnet architecture and classical verification tools, against the state-of-the-art α - β-Crown method, the winner of the VNN competition 2021. The comparison is based on the 7 benchmarks from the VNN competition, and the results are presented as an average. Our approach demonstrates a significant improvement in verification time, with an average speed-up of 1250x for CIFAR-10 and 1600x for MNIST, at the same noise level. Additionally, a higher verified accuracy (+4% and +7%) was observed on the ci-far_10_resnet benchmark in Appendix.Also, our approach did not encounter any timeouts, whereas α - β Crown had an average of more than 10% of timeouts.

It should be noted that our strategy cannot be directly compared to the VNN competition as the competition focuses on novel DNN verification algorithms/pipelines, whereas we propose a new DNN family (TTnet) that can be easily verified using classical verification tools. However, the results presented demonstrate the competitiveness of our approach. One can use our strategy to verify the robustness property on CIFAR-10, 1K images, standard DNN with α - β-Crown which takes 2 days, whereas it takes 14 seconds if one chooses to verify TTnet.

• ∗ results given on the first 1K images of the test set. Moreover, the authors only authorize a maximum of 20 pixels to switch.

Table 6: Application of TTnet to complete adversarial robustness verification for low and high noise bounded by l∞. We tabulate results of verified accuracy, natural accuracy, and mean verification time on MNIST and CIFAR-10 datasets in comparison to state-ofthe-art SAT methods (JR20 stands for [Jia and Rinard, 2020] and N+19 for [Narodytska et al., 2019]). The best verified accuracy and verification time are displayed in bold.

Strategy 2: comparison with BNNs. We compared our work with the state-of-the-art of exact verification for BNNs [Jia and Rinard, 2020; Narodytska et al., 2019]. As shown in Table 6, our verified accuracy is competitive to the one of BNNs in all cases. In low noise case, we slightly outperform BNNs [Jia and Rinard, 2020] in terms of verified accuracy and verification time. For high noise, we offer a trade-off: a slightly better verification time for a slightly lower verified accuracy. In addition, we experienced a better resolution time than BNNs while using a general SAT solver, namely MiniCard [Liffiton and Maglalang, 2012]. We highlight that in [Jia and Rinard, 2020] the SAT solver is custom-made and specific to their problem, while in our case we can use a general one. We tested 9 SAT solvers [Ignatiev et al., 2018] on MNIST high noise: the best one is MiniCard (0.0008s), the worst is MapleCM (0.0033s); while MiniSat takes 0.242s for BNNs in [Jia and Rinard, 2020].

6 Limitations And FutureWorks

Overall limitations. Themain limitation of TTnet is closely related to the maximum input bit size n, so that the truth table can be fully enumerated practically. Additionally, users cannot pre-set the final number of gates or complexity before starting the training process. Also, as mentioned in Section 2, it has not yet been shown that the aggregation of local features learned by non-linear functions can provide good performances for another dataset than images and tabular.

Limitations on scaling. While TTnet has shown promising results, its performance falls behind state-of-the-art computer vision models on larger datasets. Improving the natural accuracy of the model without increasing n is an area for future investigation [Liu et al., 2018; Bello et al., 2021].

Limitations on compactness. TTnet achieves better compactness than previous methods on tabular and MNIST datasets, but its compactness on CIFAR-10 and accuracy on MNIST could be improved. Further research is needed to address this limitation and explore the use of CNNs with Boolean logic circuits for larger datasets such as ImageNet.

Limitations on formal verification. While TTnet has demonstrated promising results in terms of verification, it may be less effective in the presence of high noise. Further research is needed to increase the model's verified accuracy, especially in noisy environments. This includes exploring the use of dedicated robustness training techniques.

Future works. The TTnet architecture presents several opportunities for future research. These include exploring its application on time series or graph-based datasets, developing better LTT architectures and training methods to achieve higher accuracy on ImageNet, and creating heuristics for converting truth tables to optimized CNF for larger n, which would in turn help the scaling. TTnet could also be a good candidate for the VNN competition.

7 Conclusion

This work is a step towards more scalable, compact, and verifiable DNNs while linking symbolic AI and learning AI. There is room for improving TTnet, and we hope that it will inspire further explorations into the use of truth tables as a tool for applying DNNs to critical applications. We provide more discussions on TTnet in Appendix.