Efficient Counterexample-Guided Fairness Verification and Repair of Neural Networks Using Satisfiability Modulo Convex Programming

1 Introduction

Deep neural networks (DNNs) are increasingly utilized to make critical decisions across various domains, including finance, healthcare, and law enforcement. These decisions significantly impact individuals' lives, making it imperative that the outcomes be fair and unbiased. However, models trained on historical data are often prone to biases based on protected attributes such as race, gender, and age. These biases can lead to unfair and discriminatory decisions, raising ethical and legal concerns. Addressing these concerns is essential not only for ensuring ethical artificial intelligence (AI) practices but also for complying with regulatory standards and maintaining public trust. Fairness properties in machine learning can be broadly classified into two categories: group fairness and individual fairness. Group fairness evaluates the behavior of the model for different demographic groups to ensure that no group is systematically disadvantaged [Albarghouthi et al., 2017; Bastani et al., 2019]. Metrics such as demographic parity, equal opportunity, and disparate impact fall into this category. However, enforcing group fairness can still lead to unfair treatment of individuals within the groups. In contrast, individual fairness ensures that individuals with similar unprotected attributes, such as qualifications or experience, receive similar outcomes, regardless of their protected attributes, e.g., age, race [Zhang et al., 2020; Zheng et al., 2022; Fayyazi et al., 2025]. This concept is closely aligned with the principle of treating similar cases consistently and is essential for situations where decisions are made on an individual basis. This paper aims to ensure individual fairness of DNNs through a fairness verification and repair process.

Several methods have been proposed to verify the fairness of machine learning models. Techniques based on satisfiability modulo theories (SMT) [Benussi et al., 2022] and mixed integer linear programming (MILP) [Biswas and Rajan, 2023; Mohammadi et al., 2023] have been effective in verifying individual fairness properties. SMT-based techniques use logical constraints to ensure that the model behaves consistently across certain categories of inputs, while MILP-based approaches formulate the fairness verification problem as a MILP problem, where the presence of integer variables significantly increases computational complexity. As a result, these techniques may not scale well to large networks due to the combinatorial explosion of possible configurations and the high computational complexity involved.

However, researchers have employed various strategies to repair unfair models, including pre-processing, postprocessing, and in-processing methods [Barocas et al., 2023]. Pre-processing methods involve modifying the training data to remove biases before model training, while postprocessing techniques adjust the model's predictions to ensure fairness after training. However, both strategies operate externally to the model's internal mechanics, often failing to correct biases learned in the latent representations, particularly in DNNs that learn complex, latent features. Inprocessing methods address this limitation by directly modifying the model's parameters during training or through posthoc adjustments to incorporate fairness constraints. While effective, these methods must balance fairness improvements with computational efficiency and model accuracy.

In this context, we introduce a novel framework, named FaVeR (Fairness Verification and Repair), that efficiently addresses both the verification and repair of individual fairness properties in DNNs, as shown in Figure 1. Our approach is twofold. First, we encode the fairness verification prob- Pre-trained NN, Protected Attributes, Fairness Property lem into a satisfiability modulo convex programming (SMC) problem, which efficiently integrates logical reasoning with numerical optimization in an iterative way. As a second step, if the network is unfair, FaVeR focuses on a targeted repair process guided by the counterexamples generated by the SMC procedure. High-sensitivity neurons are identified using a sensitivity score, which is calculated from a difference in activation values. A backward weight adaptation process then begins from the last DNN layers, iteratively modifying the weights of the high-sensitivity neurons until fairness is achieved or a maximum number of iterations is reached.

The main contributions of our work are summarized as follows: (i) We introduce FaVeR, a framework that efficiently verifies and repairs DNNs for individual fairness using an SMC-based encoding and a backward neuron adaptation method for high-sensitivity neurons. (ii) We characterize the fairness guarantees of our approach, iteratively incorporating new counterexamples and adjusting high-sensitivity neurons. (iii) We illustrate the applicability of FaVeR to a wide range of DNN architectures and datasets, showing that it is a versatile tool for fairness repair in various applications.

2 Preliminaries

We introduce the foundational concepts and formulate the problem addressed by FaVeR.

2.1 Neural Network

We define a neural network (NN) f : X → Y as a composition of linear functions and activation functions, where X ⊆ RM is a bounded input domain and Y is the output domain.

Definition 1 (Feedforward Function of a NN). Let ϕ denote the activation function, l ∈ {1, ...,L}, and let W(l,l-1) ∈ Rnl×nl-1 and b(l) ∈ Rnl denote the weight matrix and bias vector for layer l. Then, the pre-activation and activation of the i-th neuron in layer l are, respectively:

where the last layer is assumed to be linear, leading to the following expression for l ∈ {1, . . . , L - 1},

where ϕ is applied element-wise, x(0) = xin = x, and x(L) = a(L) = ˆ f(x) denotes the logit output. In a classification problem, the output is given by f(x) = argmaxi ˆ fi(x). In a regression problem, we have f(x) = ˆ f (x).

2.2 Individual Fairness

Intuitively, individual fairness requires that all "similar" inputs get "similar" outputs from the model. Formally, assume x = (x1, x2, . . . , xM)T is an instance from a dataset with M attribute values, where the set of attributes is denoted as A = {A1, . . . ,AM} and aT denotes the transpose of a ∈ RM . The set of protected attributes (PA), such as age or race, is denoted by P , where P ⊂ A.

Definition 2 (Individual Fairness). The model f is individually fair if there exists no pair (x, x′ ) of data points in the input domain X such that: (1) ∀α,Aα ∈ A \ P: xα = x′α; (2) ∃β,Aβ ∈ P: xβ ̸= x′β ; and (3) f(x) ̸= f(x′ ).

This definition assumes a classification setting where the model output is discrete (e.g., a set of class labels) and the inputs associated with protected attributes are also discrete. In this context, differences are detected via value (label) mismatch. For regression or continuous outputs, condition (3) can be relaxed to a thresholded difference, e.g., |f(x)-f(x′ )| > δ. Definition 2 [Dwork et al., 2012] requires that two individuals with identical values for the unprotected attributes, but differing in the protected attributes, produce the same output. If this is not the case for a pair (x, x′ ), then we say that individual fairness is violated and (x, x′ ) is a counterexample for individual fairness. For example, suppose that we use NN to predict whether an individual's income exceeds $50K, with race designated as a protected attribute. According to individual fairness, if two individuals with identical attributes, such as occupation and work experience, but differing in race, are assigned different income predictions, the model is unfair. Definition 2 is often impractical in the real world due to its strict requirements on unprotected attributes. It can then be relaxed to the following notion of ϵ-fairness.

Definition 3 (ϵ-Fairness). The model f is individually ϵ-fair if there is no pair (x, x′ ) of data points in the input domain X such that: (1) ∀α,Aα ∈ A \ P: |xα - x′α| ≤ ϵα; (2) ∃β,Aβ ∈ P: xβ ̸= x′β ; and (3) f(x) ̸= f(x′ ).

This relaxed definition [Biswas and Rajan, 2023] extends standard individual fairness by allowing small deviations in unprotected attributes, making it suitable for real-world applications where exact equality is unrealistic. For example, if two individuals who differ only slightly in an unprotected attribute but have different values in a protected attribute are assigned different predicted classes, the model is still considered unfair under ϵ-fairness.

2.3 SatisfiabilityModulo Convex Programming

The fairness verification problem can be translated into a satisfiability problem for a class of first-order formulas over Boolean variables and convex constraints, which can be solved using the SMC approach. SMC was shown to be effective in handling combinatorial problems over discrete and continuous variables [Shoukry et al., 2017; Shoukry et al., 2018] by adopting a lazy coordination of a Boolean satisfiability (SAT) solver and a convex solver, inspired by the lazy SMT paradigm [Barrett and Tinelli, 2018]. In SMC, the SAT solver efficiently reasons about combinations of Boolean constraints to suggest possible assignments, while the convex solver checks their consistency and returns an infeasibility certificate when conflicts arise.

2.4 NN Fairness Verification and Repair

We formalize two core tasks: verifying whether a pre-trained NN satisfies a fairness property, and repairing the network if a violation is detected.

Problem 1 (NN Verification). Given a pre-trained NN model f and a set of protected attributes P , determine whether there exists a counterexample pair (x, x′ ) ∈ X 2 such that:

• |xα -x′α| ≤ ϵα for all Aα ∈ A \ P,
• xβ ̸= x′β for at least one Aβ ∈ P,
• f(x) ̸= f(x′ ).

Problem 2 (Verification-Guided Repair). Given a pretrained NN model f and a counterexample pair (x, x′ ), find f ′ such that f ′ (x) = f ′ (x′ ), where f ′ is a NN obtained via fairness-oriented repair of f.

By iteratively solving Problem 1 and Problem 2, FaVeR aims to construct a modified neural network that satisfies the ϵfairness property. We choose ϵα = 0 for individual fairness.

3 FaVeR: Fairness Verification and Repair

We detail our methodology, covering the SMC encoding of the fairness property and the verification problem as well as the repair procedure.

3.1 SMC-Based Verification

We encode the verification problem into a satisfiability problem for an SMC formula, and solve it by coordinating decision procedures based on SAT solving and convex programming. Based on Definition 1, for each neuron i in layer l = 1, . . . ,L - 1, we encode the ReLU activation ϕ(a(l) i ) = max(0, a(l) i ) using a Boolean variable m(l) i , which indicates the activation region:

This encoding is applied to all neurons across layers. The complete feedforward behavior is captured by:

To verify fairness, we encode the constraints from Definitions 2 and 3 using Boolean variables. We introduce m(0) i for each protected attribute Aβ and m(L) for the output layer. We define:

where φp, φu, and φo enforce attribute constraints and output difference conditions for a fairness counterexample. To detect a fairness violation, we solve for an assignment to input pairs (x, x′ ) such that at least one of the protected attributes differs, the unprotected ones remain similar (within ϵ(l) i ), and the final output f(x) differs from f(x′ ). For individual fairness, we set all ϵ(l) α to zero. We combine the constraints as

and check the satisfiability of Φ in conjunction with the NN constraints in (1) and (2) using an SMC solver. The solver decomposes the problem into SAT and convex constraint feasibility subproblems over Boolean and real-valued variables, respectively. It then incrementally refines its search space by evaluating the feasibility of each Boolean assignment using convex programming to efficiently detect fairness counterexamples [Shoukry et al., 2017; Naik and Nuzzo, 2020].

3.2 Counterexample-Guided Repair

When the SMC solver discovers a counterexample, FaVeR carries out a targeted repair process that refines the weights of the high-sensitivity neurons -neurons exhibiting significant difference in activation between the counterexample inputs x and x′ . Our procedure aims to iteratively adjust these weights starting from the last layer and moving backward until the network becomes fair.

High-Sensitivity Neuron Search

FaVeR identifies high-sensitivity neurons by comparing their activation values under inputs x and x′ . If the activation difference exceeds a threshold γ, then we obtain a candidate neuron for weight refinement.

Definition 4 (Sensitivity Score). Let N = {ni }Ni=1 be the set of all neurons in the network, and let σi(x) denote the activation of neuron ni given input x. For a counterexample pair (x, x′ ), the sensitivity score Si of the i-th neuron is

A neuron ni is considered a high-sensitivity neuron if

This threshold highlights neurons with large activation deviation Si relative to the overall range of sensitivity scores.

Backward Neuron Adaptation

Let N (l) denote the set of neurons in layer l, n(l) i the i-th neuron within the layer, and S(l) i the corresponding sensitivity score. We apply the following post-hoc adaptation rule to each high-sensitivity neuron n(l) i , iterating over the layers from L down to 1:

where W (l,l-1) i,: denotes the row of weights associated with all the neurons in layer l-1 connecting to the i-th neuron in layer l, η is the step size, and λ controls the fairness-accuracy trade-off. These parameters are selected empirically on a held-out validation set to balance fairness improvement and accuracy retention, in the same spirit as cross-validation in training. We stop repairing once the accuracy drop exceeds a tolerance, so we usually apply the update only on a subset of K layers.

In the following, we show that the same amount of weight perturbation can produce a larger shift in the first-order logits of a neural network when performed to neurons that are closer to the output layer. Therefore, applying the adaptations in reverse layer order πr = (L, L-1, . . . , 1) tends to maximize the impact on the norm of the first-order logit perturbation for any prefix length K ≤ L, thus requiring fewer weight adjustments to achieve the desired unfairness reduction.

Theorem 1 (Logit Shift Maximization). Let (x, x′ ) be a counterexample and ˆ f : X → RnL the network logit function. For each layer l ∈ {1, . . . ,L} and neuron i ∈ {1, . . . , nl}, we define its influence matrix slice

capturing how perturbations to the incoming weights of neuron i affect the output logits [Goodfellow et al., 2016; Montavon et al., 2018]. For a weight-slice update ∆W (l,l-1) i,: ∈ Rnl-1 , the corresponding first-order logit perturbation is

If neuron i in layer l and neuron j in layer k < l receive updates of equal norm, i.e., ∥∆W (l,l-1) i,: ∥2 = ∥∆W (k,k-1) j,: ∥2 = c, then we obtain

Proof. By the gradient attenuation property of neural networks [Hochreiter, 1998; Bengio et al., 1994], we obtain

By the properties of spectral norms, we also have

and similarly,

Since l > k, we also have ∥µ(l) i ∥2 ≥ ∥µ(k) j ∥2. Therefore, we

Algorithm 1 details FaVeR. The algorithm begins with a pre-trained network f and produces a repaired network f ′ . Each iteration calls the SMC solver to find a counterexample (x, x′ ) (line 8). If none exists, fairness is certified and f ′ is returned (line 10). Otherwise, we compute the sensitivity score Si for each neuron ni , and select the high-sensitivity set of neurons S (lines 13-15). For each ni ∈ S, from layer L to 1, we check whether it has already been adapted (line 18). If not, its weight row W (l,l-1) i,: and bias b(l) i are updated using (5) (lines 20-22). If the resulting accuracy degradation stays within α, the update is accepted and ni is added to the adapted set A; otherwise, the change is reverted (lines 23-26). This process ensures fairness violations are resolved with minimal impact on the predictive performance and avoids redundant updates to previously repaired neurons.

3.3 Formal Guarantees of FaVeR

We discuss the formal guarantees offered by FaVeR. In each repair iteration, FaVeR updates the neurons with a significantly large influence on the NN output. The following theorem states that, for small weight perturbations, such updates strictly reduce model unfairness.

Theorem 2 (Local Unfairness Reduction). Let ˆ ft : X → RnL be the network's logit function after t repair steps, and let (xt, x′t ) be a counterexample for ˆ ft. We define the current logit difference and its unfairness as follows:

Let St be the set of high-sensitivity neurons at iteration t. Suppose we pick one neuron ni ∈ St in layer l and apply the update in (5). Let ˆ ft+1 and dt+1 be the logit function and difference after the update. Then, for small perturbations ∥∆W (l,l-1) i,: ∥2, we obtain Ut+1 < Ut, i.e., unfairness strictly decreases.

Algorithm 1: Fairness Verification and Repair

• 1: Definitions:
• 2: N (l) : set of neurons in layer l, l = 1, . . . ,L; N = ⋃Ll=1 N (l) ;
• 3: C: set of counterexamples; A: set of adapted neurons
• 4: Input: NN model f, protected attributes P, fairness property Φ, parameters η, λ, max iterations T, accuracy tolerance α
• 5: Output: Repaired classifier f ′ 6: f ′ ← f, C ← ∅, A← ∅ 7: for t = 1 to T do 8: (x, x′ ) ← SMC Solver(f ′ ,Φ, P) 9: if x = None then 10: return f ′ 11: C ← C ∪ {(x, x′ )} 12: for (x, x′ ) ∈ C do 13: Si ← |σi(x) -σi(x′ )|, ∀ni ∈ N 14: γ ← 12 (maxi Si + mini Si) 15: S ← {ni ∈ N | Si ≥ γ} 16: for l = L downto 1 do 17: for ni ∈ S ∩N (l) do 18: if ni ∈ A then 19: continue 20: Wold ← W (l,l-1) i,: , bold ← b(l) i 21: W (l,l-1) i,: ←W (l,l-1) i,: +∆W (l,l-1) i,: 22: b(l) i ← b(l) i +∆b(l) i 23: if |Lacc(f ′ ) -Lacc(f)| < αLacc(f) then 24: A ← A ∪ {n(l) i } 25: else 26: W (l,l-1) i,: ←Wold, b(l) i ← bold 27: return f ′

Proof. Under the assumption of small weight perturbation, by a first-order Taylor expansion of ˆ ft around the current weights, the change in logit difference becomes

We now evaluate the change in the norm:

For small updates, the derivative of the unfairness norm along the (dt+1 - dt ) direction gives

By substituting the Taylor approximation above, we obtain

where νl,i,j > 0 holds since a high-sensitivity neuron satisfies d⊤t gl,i,j > 0. Finally, plugging in the weight update formula from (5) yields

since η, λ, Si, νl,i,j , |Wi,j | are all positive, which leads to the (local) inequality Ut+1 < Ut.

Theorem 3 (Progress and Termination). Let ˆ ft be the logit network at iteration t and let N be the set of neurons. Then, Algorithm 1 terminates after at most |N| accepted updates. At any iteration t, we have Lacc ( ˆ ft ) ≤ (1 + α)Lacc ( ˆ f0 ). Moreover, if any (local) update is applied upon termination at some iteration t∗ , we have Ut∗ < U0.

4 Experimental Results

We discuss the empirical effectiveness of FaVeR.

4.1 Experimental Setup

FaVeR is built using Python, with models trained via the Keras APIs [Urban et al., 2020]. In alignment with previous research [Biswas and Rajan, 2023], we utilized Z3 [De Moura and Bjørner, 2008] and Gurobi [Gurobi Optimization, LLC, 2023] to solve SAT and convex problems, respectively. All the experiments were carried out on a 3.4-GHz AMD EPYC 7763 64-core processor with 32 GB of memory.

Benchmarks. We evaluated FaVeR on three datasets, namely, Bank Marketing (BM), Adult Census (AC), and German Credit (GC), which were also used to evaluate Fairify [Biswas and Rajan, 2023], as well as on the Compas (CP) dataset from FairQuant [Kim et al., 2024], as detailed in the column "Datasets" of Table 1. We relaxed individual fairness with ϵ = 0.01. We used λ = 0.01 for the regularization parameter and α = 0.02 for the accuracy tolerance to balance fairness and accuracy. These values were selected as they consistently achieved high repair rates while maintaining accuracy across the tested models.

Fairness Metrics. We evaluated fairness using two metrics adapted from prior work [Dwork et al., 2012; Krishna et al., 2022; Zhou et al., 2003]:

• Pairwise Disagreement Fraction (PD). PD measures the fraction of randomly sampled similar input pairs (xi, xj) whose predicted labels differ. A lower PD indicates fewer disagreements among similar samples, hence higher fairness.
• Local Consistency (LC). For each sample xi, LC measures the fraction of its k-nearest neighbors, computed in the input space of unprotected attributes, that share the same predicted label, and then averages this over all samples. Higher LC indicates more consistent local predictions.

We report both metrics before and after fairness repair, showing how effectively disagreements among similar inputs are reduced (PD) and local agreement is promoted (LC).

4.2 Individual Fairness Verification

Comparison with Fairify. The "Verification" columns in Table 1 present a comparison between our SMC-based verification method and Fairify [Biswas and Rajan, 2023] in terms of the verification results and runtime, showing the efficiency of SMC-based verification. Our method required, on average, approximately 20× less runtime than Fairify, while also delivering accurate verification results. In this context, SAT indicates that a counterexample exists, meaning that the model is unfair, and UNSAT denotes that the model is fair. UNK indicates cases where the solver could not conclusively determine fairness violations.

Scalability. For the CP dataset, the model sizes scale from 24 to 900. While Fairify fails to provide results for CP-3 and CP-4, FaVeR successfully solves these problems within a reasonable time frame, demonstrating its capability to handle more complex models.

4.3 Repair for Individual Fairness

The "Repair" column in Table 1 presents the fairness metrics before ("Init.") and after ("Final") repair, along with the total runtime of FaVeR applied to various models. FaVeR successfully repaired all models (the SMC solver output was UNSAT after the repair procedure) with acceptable execution times, while maintaining a low accuracy decrease.

Effectiveness of the Neuron SelectionMethod. Figure 2a shows runtime comparisons on the Bank models, contrasting random neuron selection (orange bars) with our sensitivitybased neuron selection approach (blue bars) to repair. By targeting only the neurons that are most responsible for unfair outputs, our method typically reduces the time needed to reach a fair network, illustrating its practical gains.

Comparison with REGLO. Table 2 compares FaVeRwith the state-of-the-art method REGLO [Fu et al., 2024]. In our experiments, FaVeR consistently achieves a 100% repair rate with higher accuracy: 80.09% vs. 62.97% on AC, and 87.06% vs. 27.87% on BM. Both methods achieve 69.33% on GC. Figure 2b tracks the changes in accuracy of the repaired AC-2 model over repair iterations, showing that FaVeR can achieve a significantly smaller reduction in accuracy while attaining fairness in four repair iterations. It also achieves a shorter run-time in most models.

Fairness-Accuracy Trade-offs. FaVeR keeps accuracy loss low (average ≤2.27%, as shown in Table 1), but the exact loss can vary with model size and data. Networks with fewer neurons (e.g., AC-7) tend to lose more accuracy (2.29%) because small weight changes have a larger impact. Datasets where one class appears much more than others (e.g., GC-1) are harder to repair, since the model tends to favor the majority class; bigger changes are needed to correct unfair behaviors, which lead to greater accuracy loss. In models where features are highly interconnected (e.g., BM-4), even small changes can unintentionally affect multiple outputs. Using larger fairness parameters (λ, γ) incentivizes improving fairness, which can also reduce accuracy.

5 RelatedWork

This section reviews key literature on fairness verification and repair, which is related to FaVeR.

5.1 Individual Fairness vs. Group Fairness

Fairness properties in machine learning are often categorized as individual fairness and group fairness. Individual fairness requires that similar individuals, i.e., individuals differing only in protected attributes, receive similar outcomes [Dwork et al., 2012; Bechavod and Ligett, 2017]. Group fairness, on the other hand, ensures equitable outcomes across protected groups using metrics like demographic parity and equalized odds [Hardt et al., 2016; Hardt and Barocas, 2017]. While group fairness addresses population-level bias, it does not ensure fair treatment for every pair of similar individuals. Our work focuses on individual fairness verification and repair, ensuring consistent predictions for individuals with identical non-protected attributes.

5.2 Individual Fairness Verification

Our SMC-based method differs from existing techniques for verifying individual fairness properties of NNs, by virtue of its iterative approach efficiently coordinating SAT solving and convex programming to attack the complexity of the verification problem. SMT-based methods [Benussi et al., 2022] verify individual fairness by formulating it as a satisfiability problem and leveraging SMT solvers. However, their scalability is limited for large networks. Similarly, MILP-based approaches [Biswas and Rajan, 2023;

Mohammadi et al., 2023] provide effective solutions but suffer from high computational costs, making them impractical for large-scale NNs.

5.3 Neural Network Repair

Methods for NN repair can generally be categorized into preprocessing, in-processing, and post-processing approaches. Our approach falls into the post-processing category, since we adjust the weights of specific, high-sensitivity neurons to enhance fairness. Pre-processing methods [Barocas et al., 2023] mitigate bias by altering the training data distribution, for instance, through reweighting or feature transformation. In-processing methods [Dasu et al., 2024; Li et al., 2024; Gao et al., 2022; Fu et al., 2024] address bias by directly modifying the model while learning. For example, the adversarial training framework RUNNER [Li et al., 2024] integrates fairness constraints during training using adversarial examples, although this increases computational overhead. Other post-processing techniques [Nguyen et al., 2023; Li et al., 2023] adjust weights in pre-trained models to improve fairness empirically, but they often rely on heuristic updates and lack a principled verification mechanism. Finally, REGLO [Fu et al., 2024] proposes a provable repair method for ReLU networks by solving a convex program to compute minimal weight changes to satisfy fairness constraints. While effective, REGLO applies a global linearization of the network around specific inputs, which may overlook important nonlinearities of the model. Moreover, its objective function does not encourage preserving accuracy, e.g., via explicit regularization terms. This may lead to degraded performance, e.g., in our experiments, especially in deeper models where fairness conflicts with test accuracy and generalization.

6 Conclusion

We introduced FaVeR, a framework for the verification and repair of deep neural networks with respect to individual fairness properties. FaVeR leverages satisfiability modulo convex programming-based verification to guide the dynamic weight adaptation of high-sensitivity neurons, encouraging the satisfaction of the fairness specification with minimal impact on accuracy. Our theoretical analysis shows that the proposed adjustments effectively reduce the influence of highsensitivity neurons on the overall fairness metric. Empirical results highlight the efficiency and effectiveness of FaVeR, achieving a 100% repair success rate in all the datasets tested, while maintaining high accuracy and low runtime.

Acknowledgments

This work was supported in part by NSF under awards 2514683 and 2514748.