{'fraction_non_alphanumeric': 0.028825278065399647, 'fraction_numerical': 0.01015397975884298, 'mean_word_length': 4.6088422630198576, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Verifying Inverse Model Neural Networks

Inverse problems exist in a wide variety of physical domains from aerospace engineering to medical imaging. The goal is to infer the underlying state from a set of observations. When the forward model that produced the observations is nonlinear and stochastic, solving the inverse problem is very challenging. Neural networks are an appealing solution for solving inverse problems as they can be trained from noisy data and once trained are computationally efficient to run. However, inverse model neural networks do not have guarantees of correctness built-in, which makes them unreliable for use in safety and accuracy-critical contexts. In this work we introduce a method for verifying the correctness of inverse model neural networks. Our approach is to overapproximate a nonlinear, stochastic forward model with piecewise linear constraints and encode both the overapproximate forward model and the neural network inverse model as a mixed-integer program. We demonstrate this verification procedure on a real-world airplane fuel gauge case study. The ability to verify and consequently trust inverse model neural networks allows their use in a wide variety of contexts, from aerospace to medicine.


Introduction
Neural networks have been used to solve a variety of nonlinear inverse problems such as state estimation (Melzi & Sabbioni, 2011), inverse computational mechanics (Tamaddon-Jahromi et al., 2020), and inverse-model controller design (Hussain et al., 2001). Neural networks are used because they can learn complex functions from data, whereas traditional inverse modeling approaches rely on expensive analytical inverses or brute force simulation of the forward model. However, neural network in-verse models lack accuracy guarantees, limiting their use in safety critical applications such as transportation. To enable the adoption of these models, we present a method for verifying the accuracy of an inverse model neural network. Our approach combines recent advancements in neural network and dynamic system verification to provide formal guarantees of the correctness of the model over its entire domain.
Inverse problems arise when trying to estimate an unobserved state from a set of observations, where only the forward model is known (i.e. the model that maps states to observations). This is in contrast to a filtering setting where a dynamics model as well as an observation model is often available. Analytical solutions to inverse problems may become intractable when the forward model is nonlinear, high-dimensional, or stochastic, so data-driven approaches are applied. The forward model is used to produce a dataset of state-observation pairs that are then used to train a neural network to output a state for a given observation.
Once a neural network inverse model is trained, we want guarantees that the inverse mapping between observations and states has low error, but this may be challenging due to the complexity of the forward model and neural network. Prior work (Zakrzewski, 2004) has approached this problem using sampling to get stochastic bounds on the error of an inverse model network. Formal approaches (Zakrzewski, 2002) have also been applied to 1layer networks where the forward model is replaced with a lookup table so that the Lipschitz constants of the simple network and forward model may be easily calculated and the accuracy evaluated at grid points in the domain. In addition to these simplifying assumptions, this approach scales exponentially with the number of dimensions in the domain, making it unsuitable for large scale problems.
We verify ReLU-based inverse model neural networks using mixed-integer programming, a technique that has seen significant recent usage for neural network verification (Tjeng et al., 2019;Lomuscio & Maganti, 2017). This approach allows formal verification over the entire input domain without a dependence on gridding. Instead of replacing the complex forward model that maps states to observations with a lookup table, we encode it into the mixed integer program, preserving the integrity of the model. This is enabled by overapproximating the nonlinear functions in the forward model using a technique borrowed from verification of neural network control systems (Sidrane et al., 2021). The nonlinear functions are overapproximated using piecewise linear constraints, which can be encoded into a mixed-integer program, alongside the inverse model neural network. We then maximize the error between the portion of the state that our inverse model reconstructs and the original state values. This gives us a verified upper bound on the estimation error of our inverse model.

Contributions
Our contribution is to provide a new, deterministic approach to verifying inverse model neural networks.

Related Work
Sampling can be used to assess the quality of a neural network; neural networks are typically evaluated on a test set after training (Goodfellow et al., 2016). Statistical approaches to verification (Corso et al., 2021) have been used for a wide variety of applications such as autonomous driving (Huang et al., 2018) and aviation (Zakrzewski, 2004). Zakrzewski (2004) investigates the number of samples required to estimate the failure probability with high confidence, considering Bayesian and non-Bayesian settings. They ascertain that the number of required samples, on the order of 10 10 , is tractable if the system is fast enough to evaluate. However, in the case of a component for a real autonomous vehicle, on the order of 10 9 to 10 10 hours of driving time is not feasible (Koopman & Wagner, 2016).
Additionally, Zakrzewski (2004)'s calculations rely on the assumption of being able to sample from the true distribution governing the input domain. If sampling is performed using a distribution that is slightly wrong, the claims of safety assurance fall apart. Consequently, other methods obtain guarantees using sampling coverage metrics over the input space, which again scale exponentially with the dimension of the input domain (Corso et al., 2021). Given the difficulties of sampling-based safety guarantees, we believe formal guarantees which hold over the entire input domain are more compelling.
There has recently been a surge in development of formal methods to verify neural networks (Liu et al., 2021). Of particular relevance are approaches which employ mixed-integer programming (Tjeng et al., 2019;Lomuscio & Maganti, 2017). While these approaches can make formal claims about neural networks, they are generally limited to verifying the network over a well-defined input domain. In our setting, however, the input domain of the neural network is defined by the forward model, which may be nonlinear and stochastic. Zakrzewski (2002) verifies inverse models consisting of 1layer sigmoid neural networks by replacing the forward model with a lookup table and gridding the input domain.
Our work builds upon this by verifying multi-layer ReLU neural networks, employing a mixed-integer programming approach that does not require gridding the input space, and verifying the inverse model neural network against the true nonlinear model instead of an approximate lookup table. Zakrzewski (2002) identifies the difficulty of representing the possible observation space given a domain in state space and a complex forward model. We represent this set implicitly by overapproximating and encoding the nonlinear measurement model. This is made possible by overapproximation techniques introduced by Sidrane et al. .

Problem Definition
The state of the system is a vector of variables x. Let y be a noisy measurement of the state such that where ν is a vector of random variables and f is the stochastic forward model. We are interested in estimating a subset of the state, z, from a noisy measurement y. The function f leads to the distribution p(y | x), from which we can write where x\ z denotes the variables in x but not in z. Our goal is to invert p(y | z) and estimate z given measurements y: without explicitly computing Equations (2) and (3). We interchangeably use distributional notation such as y ∼ p(y | x) and functional notation such as y = f (x, ν) depending on which is more clear for the context. For the purpose of this paper we define The functional inverse may not always exist but arg max z ′ p(z ′ | y) always exists.
To make the problem more concrete, we will use a 2D localization problem as a running example throughout this section to explain our methodology. In this problem, a robot attempts to localize itself within a 2D room. The state is the robot's position, x = (x r , y r ). The robot receives two noisy range measurements of its state: from sensor beacons located at the corners of the back wall, as shown in Figure 1. The sensor beacons are located at coordinates (x 1 , y 1 ) and (x 2 , y 2 ) and each measurement has additive noise ν i ∼ N (0, σ). The robot is free to move anywhere in the blue shaded region. We would like to invert the forward model in Equation (5) and recover the robot's position. In this example, z is the same as x:  We verify neural networks N N (y) trained to estimate z from a measurement y and produce an estimateẑ: For the localization example, a neural network is trained to produce estimatesẑ = [x r ,ŷ r ] given inputs y = [r 1 , r 2 ] and labels z = [x r , y r ]. Once trained, we would like assess the quality of our inverse model. We would like to bound the error between z and our estimate of it. Given a bounded region of states x ∈ X , which in turn bounds z as z ⊆ x, we want to find some u such that where · is some norm. Neural networks do not have built in guarantees of correctness, so we use neural network verification tools to obtain u. However, the nonlinear and stochastic nature of the forward model presents new challenges that many existing neural network verification tools are not equipped to handle.
state estimate Figure 2: Overview of the method.

Methods
Our methodology is illustrated in Figure 2. The forward model f (x, ν) maps states in X to a set of measurements as shown by the black irregularly shaped set in the center of Figure 2. Our approach is to overapproximate the nonlinear forward model using piecewise linear constraints to produce a modelf (x, ν). This model implicitly defines an overapproximation of the set of possible measurements and is shown by the blue set in the center of Figure 2. Noting that both the overapproximate forward model and the neural network can be represented by piecewise linear expressions, they can be combined into a single mixed-integer linear program. We add the maximum error between the reconstructionẑ and the original subset of the state z as an objective. By solving the resulting optimization problem, we can obtain a bound on the set of possible estimation errors. The following subsections provide more details.

Overapproximating the measurement model
The measurement model f which produces measurements y may contain polynomials (e.g. x 2 ), trigonometric functions (e.g. cos(x)), piecewise nonlinearities (e.g. max(x, y)), exponentials (e.g. e x ) and compositions thereof. As the end goal is to encode the entire verification problem into a mixed integer linear program, these functions are approximated with piecewise linear constraints. We overapproximate these nonlinear functions using a method called OVERT (Sidrane et al., 2021). An overapproximation is an approximation such that any property proven for the overapproximate model holds for the true model. For example, we would like to quantify the maximum error between our estimateẑ and the true z.
If we compute an upper boundû on this maximum error using the overapproximate model, we know thatû is greater than or equal to the maximum error e max that exists between z andẑ when using the true nonlinear model: OVERT involves re-writing a multi-dimensional nonlinear function into one-dimensional nonlinear functions, and then finding an optimally tight upper and lower bound for each one-dimensional nonlinear function. Given a domain for the input of each one-dimensional nonlinear function and knowledge of the inflection points, OVERT fits strings of secants or tangents to form tight bounds. It opti- x 2 lower bound, n = 5 upper bound, n = 4 mizes the sub-interval boundaries between secants/tangents to achieve minimum area between the function and its bounds.
In the example localization problem, the measurement model contains the functions g(x) = x 2 and g(x) = √ x. These functions are converted to piecewise linear bounds to produce the overapproximate forward modelf . An illustration of an overapproximation for the x 2 function over the domain [1, 15] is shown in Figure 3. The lower bound contains 5 linear segments and the upper bound contains 4. In this example, the error between the function and bound is within 2% of the range of the function.

Posing the verification problem as an MIP
Once the nonlinear measurement model f has been overapproximated, the entire system consists of piecewise linear relations, because the ReLU-based inverse model neural network N N (y) is already a piecewise linear function. Piecewise linear constraints can be encoded into mixedinteger programs using binary variables. Thus the entire system can be encoded into a mixed integer program. In order to compute the maximum error between z and the estimate returned by the inverse model neural network,ẑ, the following mixed integer optimization problem is solved: where X denotes the domain of the state variables x, of which z is a subset, N denotes the domain of the random variables ν, and y ⊲⊳f (x) denotes that the measurements y are related to the state x via the approximated nonlinear measurement modelf . The optimal solution to the mixedinteger program (x * , p * ) is produced using the commer-cial MIP solver Gurboi (Gurobi Optimization, LLC, 2022). The value of the optimal solution is an upper bound on the maximum error: p * =û ≥ e max . It is an upper bound due to the error introduced by overapproximation.

Encoding piecewise linear functions into the MIP
Prior work has demonstrated how ReLU activation functions and other piecewise linear functions may be encoded as mixed-integer constraints ( Expr2MIP.jl that implements the above encodings. It is modular and capable of encoding general piecewise linear functions composed of | · |, max, and ReLU into mixedinteger constraints.

Handling stochasticity
Because the forward model is probabilistic, the bounds on the maximum estimation error will also be probabilistic, which we account for using the notion of probability mass. When the forward model is overapproximated using the methods in Section 4.1, a domain on each variable in the model must be specified, as mentioned in Section 4.2. Therefore, we restrict the domain of the random variables ν to contain a desired amount of probability mass. The probability mass captured by this restricted domain will also correspond to the probability mass captured in the distribution of estimation errors.
For example, the localization problem has two random variables (ν 1 and ν 2 ), each independently distributed according to a normal distribution with standard deviation σ. If we constrain the domain of ν 1 to ν 1 ∈ [−3σ,3σ], we capture 99.73% of the probability mass associated with ν 1 . Similar logic applies to ν 2 . Because the variables are independent, these domains cover 0.9973 2 = 0.9946, or 99.46% of the probability mass of the joint distribution. In turn, the verification algorithm will find the maximum estimation error across 99.46% of the full distribution of network estimation errors. We note that the domains of the random variables can be selected based on the user's desired confidence. If we instead constrained the variables to have a domain of ±2σ, we would capture 91.107% of the probability mass in the joint distribution.

Example results
We apply the methodology described in Section 4 to the running example problem of 2D localization. The first problem maximizes the objective |x r −x r | wherex r is the estimate produced by the neural network and |·| is the absolute value. The second problem maximizes |y r −ŷ r |. The choice of norm for the objective is up to the user. For example, z −ẑ ∞ = max(|x r −x r |, |y r −ŷ r |) could have also been chosen. The problem of finding the maximum error in the x and y directions over the whole domain is solved with two calls to the optimizer, resulting in maximum x and y estimation errors over the whole domain of 3.95 ft and 3.96 ft, respectively. In order to better visualize the error, we discretize the domain according to our desired computational budget and solve two optimization problems for each (x, y) cell. The results can be seen in Figure 4.
We can tell from these bounds that errors in the estimate of x-position tend to be higher for small values of y, and errors in the estimate of the y-position tends to be higher for large values of y. Based on the sensor beacon locations, small changes in range result in larger changes in x for small values of y producing a more difficult estimation problem in that region. The opposite is true for the y-position.
Additionally, for the x-coordinate, we compare the upper bounds on error computed using our verification approach to approximate upper bounds obtained through sampling and through the simulation of the extreme points found from verification. The results are shown in Figure 5. As expected, the output of the formal verification upper bounds the true values from the model.

Fuel Gauge Case Study
We use an airplane fuel gauge as a case study to demonstrate the real-world applicability of our method. Fuel is often kept in wings of aircraft and getting an accurate measurement during flight is difficult. As fuel is flight critical, an accurate, responsive, and independent measurement is desired. Filtering using a time-history of measurements is undesirable because it allows errors in fuel estimates to propagate across time. For this reason, singleshot Bayesian inference, which can be used to estimate the distribution p(z | y) given the forward model p(y | z), is a desirable technique to solve the problem. Nevertheless, exact Bayesian inference is often intractable for systems with nonlinear measurement models. Therefore, these techniques often rely on complex sampling methods such as Markov Chain Monte Carlo (MCMC), which can require many samples to produce accurate estimates and only provide statistical guarantees of convergence (Brooks et al., 2011). All of these properties make the use of an inverse The approach proposed by Zakrzewski (2001) is to use a neural network that takes in pressure measurements from the fuel chamber as well as the three-axis acceleration of the aircraft. Using a forward model of the fuel tank similar to the model used in Zakrzewski (2001), we trained a ReLU-based inverse model neural network to produce the mass of fuel as a function of the pressure and acceleration measurements. We use a fully connected network with three hidden layers containing 64, 32, and 12 hidden units respectively. We compare the performance of the neural network to that of a samplingbased Bayesian inference technique and that of linear regression. The Bayesian inference was performed approximately using a version of MCMC called No-U-Turn sampling (NUTS) (Hoffman et al., 2014) implemented in Turing.jl (Ge et al., 2018). The NUTS algorithm was used to generate 1, 000 samples for each mass value with 1, 000 adaptation steps and a target accept rate of 0.9. A comparison of these techniques is summarized in Figure 6.
Overall, the neural network has the best performance. While the Bayesian inference estimates often converge close to the true value, the MCMC sampling procedure sometimes fails to converge to an accurate estimate. Furthermore, the Bayesian inference queries took 26 seconds on average on a single 4.20 GHz Intel Core i7 processor, while the neural network queries took 6 × 10 −6 seconds on average.
Airplane fuel gauge model The forward model for the airplane fuel gauge is described as follows. The state x consists of the current mass of fuel in the tank m, roll φ and pitch θ of the aircraft, and ambient air pressure P a . The measurement model computes readings at 9 pressure sensors in the fuel tank as well as the three-dimensional acceleration of the aircraft, which all have associated noise.
The inverse model attempts to recover the fuel mass m: We want to quantify the error between the neural network estimate of the fuel mass and its true value: where | · | denotes absolute value. The pressure reading at a given sensor is determined by the height of fuel above the sensor: where h f is the fuel height, h s is the sensor height, ρ is the fuel density, a is the acceleration magnitude, c is a scaling factor, P a is ambient air pressure, and ν p is Gaussian noise distributed as ν p ∼ N (0, σ p ). The fuel height at a given point in the tank and the three-dimensional position of a given pressure sensor are both functions of the roll φ and pitch θ of the aircraft. The fuel height is also a function of the volume v of fuel in the tank: where f lo is a mapping from (v, θ, φ) to fuel height when the wings are unloaded and analogously f hi is a mapping from (v, θ, φ) to fuel height when the wings are fully loaded. Similarly, p l = (x l , y l , z l ) is the position of the sensor when the aircraft is at nominal attitude (θ = 0, φ = 0) with wings unloaded, and p h = (x h , y h , z h ) is the position of the sensor at nominal attitude with wings loaded. The function g maps the pressure sensor coordinates p l and p h from nominal attitude to an arbitrary roll φ and pitch θ: g(θ, φ, x, y, z) = x sin(φ)−y sin(θ) cos(φ)+z cos(θ) cos(φ) The acceleration at a given attitude is computed: (20) where a is the magnitude of total acceleration and (ν ax , ν ay , ν az ) are independent Gaussian noise variables each distributed ν a ∼ N (0, σ a ). The magnitude of total acceleration is fixed at a = 10 m/s 2 .
Gridding and parallelization Despite abundant nonlinearity and the use of transcendental functions such as in Equation (17), the resulting forward model could be encoded using OVERT and solved as a single mixed integer program except for the fact that the analytical mappings from volume, pitch and roll to fuel height at any given sensor, h f uel lo = f lo (v, θ, φ) and h f uel hi = f hi (v, θ, φ), are not known. As a result two lookup tables mapping (v, θ, φ) → h f uel lo and (v, θ, φ) → h f uel hi are calculated from a CAD model of the fuel tank and these tables are treated as ground truth. Without the lookup table, the state space could be gridded as desired in order to obtain additional resolution about maximum error, as is done in the example in Section 4.5. In general, no gridding is required and a resolution could be chosen given a computational budget. However, the use of a lookup table determines the grid resolution in the case of this fuel gauge case study. Given a large number of pre-imposed grid cells (7488) that are completely independent of one another, our technique is highly parallelizable.
Overapproximation using OVERT requires a domain for each smooth function. Similarly, the mixed-integer encodings used both for the network and the overapproximate forward model compute bounds based on a given domain. However, separately overapproximating and encoding the forward model and network for every (v, θ, φ) cell would be wasteful as these are relatively expensive operations involving many calls to the optimizer. Consequently, the smooth functions of the model (e.g. Equation (17), Equation (20)) are overapproximated and encoded over the whole domain. Similarly, the network is encoded using bounds computed from the whole domain. The optimization problem is then duplicated. For each cell (v, θ, φ), the domain is then additionally constrained to find the maximum error unique to that specific cell.
One key modification was made to increase the speed of verification: the use of a sampled lower bound. When seeking the maximum value of |m −m|, all samples of the true model form a lower bound. A constraint is added to the optimization problem of the form where s max is the worst deviation between m andm found while sampling from the domain uniformly at random. Sampling is fast and helps narrow the search space for an optimum. Overall, we observed a speedup of up to 16%.

Fuel Gauge Results
We present the results of running our verification method for an inverse model neural network on the airplane fuel gauge case study. We are able to obtain verified upper bounds on error max x |m −m| for each (v, θ, φ) cell in the problem domain. We maximize over φ and θ values in order to find the maximum error at a given fuel level and show the results in Figure 7. Quantifying the error in fuel mass estimate is important because the remaining fuel mass determines the safe remaining range of the aircraft.
We compute the verified upper bound for three noise domains of the 12 random variables in the input: 1σ, 2σ, and 3σ. This gives upper bounds corresponding to 1.02%, 57.12%, and 96.81% of the probability mass of the error distribution, respectively. The verified upper bound considering 3σ noise levels and consequently 96.81% of the probability mass of the error distribution may be an acceptable upper bound depending on the application. However, the risk threshold is ultimately a user-chosen parameter, and, for example, a verified upper bound considering higher noise levels could also be computed. Increasing the noise level increases the conservatism of the verified upper bound and the time required to compute it. The time taken to compute verified upper bounds on the error for each level of noise on the inputs is shown in Table 1. Experiments where run on 148 physical cores (see Appendix B).
Returning to Figure 7, we compare the verified upper bounds on error to two baselines. The first baseline is uniform random sampling from the domain of x and the corresponding noise domain for noise variables ν. We estimate the maximum error using 63, 000 samples for each mass bin. We can see that the verified upper bound is much higher than the sampled upper bound. Sampling will always form a lower bound to the maximum error, so this result is as expected. However, the difference between the verified bound and sampling may be due to both overapproximation in the forward model and suboptimality of random sampling.
To determine which has more impact, we pass the optimum point x * for each cell through the original nonlinear  forward model, and the neural network fuel gauge. This is in effect an adversarial sample found through optimization and produces an error which is plotted under the label "true" in Figure 7. This line is tight to the upper bound on error values produced by the optimizer using the overapproximate forward model, and relatively farther from the sampled lower bound. This tells us that little conservatism is added due to the use of overapproximation. It also tells us that the sampled lower bound is not as tight to the true maximum error curve (which the 'true' curve still lower bounds) as in the example localization problem. This problem has many more state variables and 12 dimensions of noise, which make it difficult for unguided random sampling to find the maximum error.
Our method allows precise quantification of the error of the inverse model neural network throughout different areas of the state space. Figure 8 shows the maximum amount of error for different regions of state space as roll and pitch of the aircraft vary. The maximum over the entire range of fuel mass values is shown. Such a precise quantification of error could be used to decide a safe lower bound on remaining fuel mass, and therefore safe range limits for an aircraft at its current roll and pitch attitude.
Finally, the performance of the inverse fuel gauge model can also be quantified by assessing the fraction of the domain (by volume) over which the inverse model produces estimates below a specified error tolerance. The results are shown in Figure 9. Such an analysis could be used to determine whether a given inverse model meets performance standards.

Conclusion
We introduced a method for quantifying the error of inverse model neural networks against nonlinear, stochastic forward models. Given a noise threshold on each of the random variables in the model, our method produces verified upper bounds on the estimation error. In addition, the points of the domain selected by the optimizer represent adversarial samples of the true model that may not be found with unguided sampling. We demonstrate that our method can scale to real-world problems such as an airplane fuel gauge system. In general, neural networks do not have built-in guarantees of correctness, which can prevent their application to many real world problems that could benefit from their flexibility and performance. Precisely quantifying estimation error of inverse model neural networks could allow their use in many safety-critical applications.

B. Fuel Gauge Experimental Details
Fuel gauge verification experiments were run across 5 servers with a collective 148 physical CPU cores and 296 logical CPU cores. Fourteen Julia threads were used, but each call to the optimizer calls the BLAS library which was allowed to spawn a number of threads up to the number of physical CPU cores on each server. The processors of the five machines used were: C. Additional Fuel Gauge Results Figure 10 shows the fuel mass estimation error plotted with respect to different system variables. For the left plot a maximum was taken over mass values, for the middle plot a maximum was taken over pitch values and for the right plot a maximum was taken over roll values.