We introduce a neuro-symbolic verification framework that challenges the conventional trade-of between accuracy and explainability by maintaining model precision while enabling formal verification or explanation for the majority of decisions. Rather than attempting to verify an entire neural network - often computationally intractable - we train it to decompose its decision boundary into smaller, verifiable submodels, allowing for partial coverage with Reduced Ordered Binary Decision Diagrams representations. This ensures rigorous verification for the majority of cases, while acknowledging and identifying cases that remain unverifiable. Our method allows us to formally analyze over 94% of decisions in standard benchmarks without sacrificing accuracy. Additionally, our system is designed to identify cases where a decision cannot be formally verified, ensuring that uncertain predictions are flagged for human intervention or additional scrutiny. This guarantees that AI-driven decisions remain not only precise and explainable but also trustworthy. Our approach provides a scalable and practical solution for deploying safe, accountable, and formally verifiable AI, ofering a new verification pathway where accuracy and interpretability are simultaneously achievable rather than being at odds.
The widespread adoption of Artificial Intelligence (AI) and Machine Learning (ML) in critical applications (such as healthcare, finance, and autonomous systems) has created a growing demand for trustworthy and verifiable AI. However, modern machine learning models, particularly deep neural networks and complex ensemble methods, often function as black boxes, making their decisions dificult to interpret or formally verify. This lack of explainability and verifiability is a major concern in high-stakes environments, where erroneous or unverifiable predictions can lead to severe consequences.
Existing explainability and verification methods typically rely on post-hoc interpretability techniques
[
To do so, we introduce a hierarchical verification structure, where approximation networks, trained
alongside the main model, are able to provide formal guarantees for most decisions while allowing
complex, unverifiable cases to be flagged for additional control. We use a neuro-symbolic [
The remainder of this paper is structured as follows. Section 2 examines the limitations of existing formal verification methods for neural networks. Section 3 introduces our approximation-based verification framework, detailing how smaller submodels constrain the overall decision space. Section 4 presents experimental results demonstrating that our approach preserves accuracy while allowing a significant proportion of decisions to be formally verified. Finally, we conclude by discussing the implications of our findings and potential future research directions.
Our approach applies formal verification (FM) to neural networks (NNs) by expressing them as Boolean
circuits [
Once expressed as an ROBDD, a (binarized) neural network allows for precise formal verification
queries that are otherwise infeasible in conventional deep learning models, for instance bias
elimination (ensuring that protected attributes such as gender or ethnicity do not afect predictions), safety
verification in autonomous systems (guaranteeing that the AI model does not enter unsafe states under
any possible input configuration) and even adversarial robustness. However, despite these advantages,
applying ROBDDs to large-scale neural networks remains highly challenging. Converting a neural
network into a ROBDD may have a time complexity of (! · 2 · 22 ) and may result in a BDD of size
(22 ) (for a special family of function) [
To address this scalability issue, we introduce approximation networks, which allow us to reduce the complexity of the ROBDD conversion while preserving the benefits of formal verification. Instead of verifying the full neural network, our approach selectively trains smaller subnetworks, designed to approximate specific decision boundaries while remaining tractable for ROBDD representation. These approximation networks act as verifiable surrogates, covering a large proportion of decisions that can be formally verified, while leaving only a limited set of complex cases unverifiable. By structuring the decision boundary in this way, we enable partial but scalable verification, ensuring that the majority prev_layer ← layers_obdd[0] p_vars ← prev_layer[0].vars for each layer of layers_obdd[1:] do res_layer ← [] for each obdd of layer do res_bdd ← obdd.compose(obdd.vars, prev_layer) res_bdd.vars ← p_vars append(res_layer, res_bdd) prev_layer ← res_layer return prev_layer 1 2 3
1 1 2 3 4 of AI decisions remain provably correct while explicitly flagging uncertain cases for further scrutiny. This approach provides a practical pathway for integrating formal verification into modern AI systems, balancing computational feasibility with the need for rigorous, logic-based guarantees in machine learning models.
While it is possible to train a network directly in its binarized form, this often leads to optimization challenges due to the non-diferentiability of the binarization function. Therefore, in practice, BNNs are usually trained using floating-point weights and activations, and then binarized afterward for compilation purposes. Binarized NN have binary inputs and outputs, but floating-point weights and biases. We use an activation layer between each fully connected layer that implements the threshold function 2.1. This ensures that every neuron input and output is binary, either 1 or 0 ( () = 1 if ≥ 0 otherwise 0). The binarization by itself is not particularly computationally expansive (if we accept to loose precision). The main challenge is to be able to "compile" a BNN into a ROBDD, in order to use formal verification on it.
During the training phase, the activation layers function as sigmoid activations, facilitating faster
training. The compilation method follows these steps: first, each layer is processed sequentially,
considering one neuron at a time, based on the algorithm of [
This algorithm can be illustrated using the example of a binarized neural network in Figure 1: we sequentially express the outputs (ℎ1, ℎ2, ℎ3, ℎ4) of the first layer with inputs ( 1, 2, 3), and the output (1) of the second layer with the outputs (ℎ1, ℎ2, ℎ3, ℎ4) of the first layer. At the end of the algorithm, a single BDD will be constructed, representing the output in terms of the inputs. 2 1 features
State-of-the-art Neural network
M a x F u n c t i o n
Unfortunately, Table 1 illustrates our measured growth in computational cost required to rewrite
a binarized neural network based on its size (also reported in [
We propose a novel structured verification approach that overcomes the limitations discussed earlier by integrating a logical layer that connects multiple neural networks, with controlled sizes. Our approach replaces a single large neural network with a Global Model that integrates multiple approximation networks (see Figure 2). Each approximation network is trained to capture a verifiable subset of decisions, while we expect the main neural network to remain responsible for handling more complex cases. The final prediction, denoted as , is computed as = max(1, 2, . . . , , ), where represents the output of an approximation network and is the output of the main neural network. This architecture ensures that if any approximator is confident in its decision, the final model prediction is immediately verifiable. If no approximator provides a decision, the main neural network takes over, handling more intricate cases that may not be directly verifiable.
The intuition behind our idea is to build on Decision Boundary Decomposition. We take advantage of the fact that many real-world decision boundaries are locally simple but globally complex: while the global decision boundary may be highly complex, many local subregions are governed by simple, well-separated decision rules. This phenomenon aligns with the Pareto principle, where (typically) 80% of the decision complexity arises from only 20% of cases. Our aim is to exploit this structure by assigning verifiable approximation networks to low-complexity regions, while more intricate cases are handled by the main neural network. This design follows a Pareto-like pattern, where the majority of decisions fall into simpler, verifiable subregions, significantly improving formal verification feasibility.
Note that, in the current work, we focus on explaining positive decisions (cases where the model responds "yes" or "1"), using the max function to capture verifiable subsets. While our framework is currently designed for positive predictions, generalizing it to both "yes" and "no" decisions (0/1 outputs) is a natural extension and remains an ongoing area of research.
Since the final decision inherits the properties of at least one approximator when it takes precedence, we can ensure global model properties by controlling the behavior of its subcomponents. If all approximators are designed/proved to be fully explainable or bias-free, any decision one approximator covers will also be explainable at the global level: let’s suppose that approximator satisfies a given formal property (e.g., fairness, monotonicity, adversarial robustness), then for any input where () = 1, we can guarantee that the Global Model also satisfies on that input, since
() = max(1(), 2(), . . . , (), ()) ≥ ()
For example, consider the case of fairness and explainability, where we construct multiple approximation networks that adhere to a specific constraint: “The decision must not be influenced by the individual’s gender.” Our decomposition of the decision-making process across multiple approximation networks (each one enforcing this fairness constraint) ensures that any decision made by one of these modules inherently satisfies the condition at the global level. If these approximation networks are trained to cover all positive cases, the fairness property extends to the entire model, guaranteeing that all decisions made by at least one approximator remain unbiased.
To efectively integrate approximation networks into the global model, diferent training strategies may be proposed. One approach is sequential training, where approximation networks are trained ifrst to handle simpler decisions before training the main neural network to focus on more complex cases. This method encourages approximation networks to learn the most verifiable decisions, improving explainability. Alternatively, simultaneous training allows all components to be trained together, ensuring consistency between models, though it may limit the efectiveness of approximation networks in capturing simple cases independently. Another option is independent training with post-integration, where each component is trained separately and later combined through the logical layer. This last method is only used in Section 4 as it is not relevant for the current experiment (each component is independently trained with classical methods that do not need to be studied here). Gradient Propagation through the Max Layer For each of these methods, we also consider two diferent gradient propagation strategies through the max layer: ALL and MAX. The ALL method distributes the gradient to all inputs, while the MAX method propagates the gradient only to the maximum value. These methods may impact the performance of the global model, particularly in terms of coverage and accuracy.
Loss Function To optimize the training process, we employed a range of ad hoc loss functions in a preliminary study. The loss function that yielded the best results is a weighted binary cross-entropy function (see eq. 1), where is a penalty applied to class 1. When the expected label is 0 but the predicted label is 1, the loss is times larger than in the opposite case. The idea is to penalized submodules that wrongly predict class 1 (because the decision will be irrevocable): it is better for submodules to have a false negative, that can be recovered by the large NN.
= − ( · (1 − ) · log(1 − ) + · log()) (1)
Using this loss function provided better results compared to standard binary cross-entropy, particularly in terms of recall for class 0 and precision for class 1. However, this approach led to a reduction in precision for class 0 and a decrease in recall for class 1. Increasing the penalty results in higher confidence in class 1 predictions but at the expense of reduced coverage (for example, setting = 25 often results in a model predicting only class 0). A suitable value must be chosen to balance precision and coverage (see below).
We based our experimental study on all the available benchmarks on [
The evaluation metrics used in our study include several key measures to assess the performance of the global model and its components. Model Coverage refers to the accuracy of the global model when predicting positive cases (class "1"). Approximator Coverage measures the accuracy considering only the predictions made by the approximator network. Relative Coverage represents the proportion of positive predictions made by the global model that are also predicted by the approximator, computed as the ratio of approximator coverage to model coverage ( AMpopdroelxccoovveerraaggee ). Neural Network Coverage reflects the accuracy of the large neural network, though a lower value does not necessarily indicate poor performance, as the network is designed to handle only complex cases. Additionally, Approximator Misclassifying Zeros quantifies the percentage of false positives for class 1, capturing errors where the approximator incorrectly predicts a positive outcome. Finally, Global Model Accuracy accounts for the overall accuracy of the model across both classes, providing a global measure of system performance.
The results of this preliminary study are presented in Table 2. We observe that the ALL method performs best. However, it is quite surprising to see that the Simultaneous method also provides strong results. The main diference is seen in the incorrect classification of zeros by the approximator. This metric is particularly important because if an approximator incorrectly classifies a 0 as a 1, the large neural network will not be able to correct this decision, regardless of its size.
The Table 3 shows the results of the same experiment, but with diferent penalties applied to class 1. We can see that the best results are obtained with a penalty of 2, which provides a good balance between precision and recall for both classes.
We selected datasets containing tabular data and providing binary classification problems and we
binarized their features that may be originally boolean, floating-point, or categorical. We included the
datasets Compas ([20]), Diabetes ([
One limitation of our current work is that, for simplicity, both the neural network and the approximators are trained with binarized datasets, which decrease the performances of the large NN (we are working on this point). Our final observation concerns how the diferent neural networks are trained. The Table 5 shows that sequential and separate trainings are the best methods for covering most of the cases with approximation networks. Between these two methods, sequential training appears to yield slightly fewer misclassifications and a better coverage than separate training. As for simultaneous training, it generally results in significantly more "0" misclassifications and lower coverage. Additionally, using the sequential or separate training methods allows for easy extension at a later date by adding new approximation networks. Another advantage is the ability to change the loss function for each part of the global model, unlike the simultaneous method, which does not easily support this flexibility.
The increasing deployment of neural networks in critical domains highlights the importance of formal verification. As these models are often used in safety-critical or ethically sensitive settings, providing guarantees about their behavior is essential. Formal methods, such as compilation into decision diagrams, ofer a promising path for analyzing and reasoning about the internal logic of neural models in a principled and rigorous manner. One of the main advantages of ROBDDs lies in their ability to eficiently count models, which can be leveraged to assess fairness criteria—such as balancing positive outcomes across protected groups—through exact counting.
Our approach, however, is not limited to neural networks. In principle, other interpretable approximators could be used, such as decision trees or small random forests. These models are inherently explainable and can sometimes yield more compact logical representations. Nonetheless, random forests are more dificult to integrate into end-to-end diferentiable pipelines and typically lack the flexibility needed for tasks such as knowledge distillation or joint optimization with other components.
By contrast, using a neural network as the approximation module ofers significantly more modeling freedom. Neural networks can be trained jointly with other subsystems, fine-tuned for specific downstream tasks, and serve as targets for distillation from larger, more accurate models. This enables a hybrid strategy in which a complex model is first trained for accuracy and then distilled into a smaller, verifiable architecture.
Thus, retaining a neural representation—even if it is eventually binarized for compilation and not trivially amenable to formal analysis—provides greater flexibility in the learning pipeline. It supports a wider range of optimization strategies while still enabling formal guarantees through the compilation step.
An additional benefit of our approach is that it enables the integration of symbolic prior knowledge
through knowledge compilation [
One final point of discussion concerns a limitation of our current work: we only target positive decisions. To overcome this, we are investigating the use of the ROBDD from the current approximator as a routing mechanism. Specifically, the 1/0 output would indicate whether to delegate the input to a specialized approximator—for handling multiple classes—or to the main neural network. In this setting, the router functions as a selector, determining whether a given instance is suficiently simple to be handled by an auxiliary component, or requires the full capacity of the original model. Our preliminary results suggest that this routing strategy could achieve similar levels of coverage while extending the approach beyond binary classification.
The goal of our proposed method is to enable formal verification of simple cases decided by neural networks, which can be processed by reasonably sized subnetworks. We demonstrate that it is possible to integrate a small neural network within a larger neural network model in such a way that if any of the small networks decide "Yes" for a given decision, the global model will also decide "Yes". We show that even on non-trivial examples, very small neural networks (NNs) can capture a high proportion of decisions for which formal verification or explanation can be performed eficiently.
While our results demonstrate that up to 94% of decisions can be formally verified, there remain important limitations. The subset of unverifiable decisions (ranging from 6% to 25% depending on the dataset) may correspond to more complex or edge-case scenarios, potentially requiring additional scrutiny. Furthermore, our approach relies on a binarization step that can lead to feature explosion, especially in datasets with continuous variables. Future work will explore hybrid approaches combining our method with adversarial training techniques to improve coverage in high-complexity cases.
A key advantage of our method is its ability to identify unverifiable decisions—cases where the approximation networks fail to provide a provable answer—allowing these instances to be flagged for further scrutiny. In other words, our approach ensures that the system "knows when it doesn’t know", a crucial property for safe and trustworthy AI deployment.
Looking forward, a natural extension of this work is to explore knowledge distillation as a means to apply our approach to existing neural networks (instead of training the approximator at the same time). By systematically transferring knowledge from the larger model to smaller, verifiable networks, we could refine the decision boundary decomposition even further, maximizing the proportion of formally verifiable decisions. Additionally, extending this framework to handle both "yes" and "no" decisions, and integrating it with adversarial robustness techniques, could further enhance its applicability in real-world AI deployment. We also want to study the exact nature of the cases that remain unverifiable. Are they edge cases, adversarial examples, or ambiguous samples?
By bridging the gap between machine learning and formal verification, this work paves the way for scalable, explainable, and provably reliable AI systems. This contributes to the broader goal of building trustworthy and accountable artificial intelligence.
This work has been partially funded by the "Chaire IA Digne de Confiance" (Chair on Trustworthy AI), operated by the Bordeaux University Foundation.
All the experiments and code were developped without generative AI. The translation of a number of sentences in this paper, the english grammar and language were improved by text generation AI. on Computer Applications in Medical Care, American Medical Informatics Association, 1988, pp. 261–265. URL: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC2245318/. [20] J. Angwin, J. Larson, S. Mattu, L. Kirchner, Machine bias: There’s software used across the country to predict future criminals. and it’s biased against blacks, ProPublica (2016). URL: https: //www.propublica.org/article/machine-bias-risk-assessments-in-criminal-sentencing. [21] British Board of Trade, Report on the loss of the titanic (s.s.), 1912. URL: https://www.kaggle.com/ c/titanic. [22] D. Dua, C. Graf, UCI Machine Learning Repository - Adult Dataset, Technical Report, University of California, Irvine, School of Information and Computer Sciences, 2019. URL: https://archive.ics. uci.edu/ml/datasets/adult. [23] Kaggle, Kaggle: Your machine learning and data science community, 2024. URL: https://www. kaggle.com.