Method of verifying pretrained neural net mapping for use in safety-critical software

• US 6,473,746 B1
• Filed: 12/16/1999
• Issued: 10/29/2002
• Est. Priority Date: 12/16/1999
• Status: Expired due to Term

• Current Assignee: a New York corporation, Simmonds Precision Products, Inc. (Raytheon Technologies Corporation d/b/a RTX)
• Original Assignee: Simmonds Precision Products, Inc. (Raytheon Technologies Corporation d/b/a RTX)
• Inventors: Zakrzewski, Radoslaw Romuald
• Primary Examiner(s): Davis, George B.
• Application Number:
  US09/465,881
• Time in Patent Office: 1,048 Days
• Field of Search: 706/15, 706/31
• US Class Current: 706/15
• CPC Class Codes: G06F 11/3608 using formal methods, e.g. model checking, abstract interpretation theorem proving G06N5/013

Abstract

A method of verifying pretrained, static, feedforward neural network mapping software using Lipschitz constants for determining bounds on output values and estimation errors is disclosed. By way of example, two cases of interest from the point of view of safety-critical software, like aircraft fuel gauging systems, are discussed. The first case is the simpler case of when neural net mapping software is trained to replace look-up table mapping software. A detailed verification procedure is provided to establish functional equivalence of the neural net and look-up table mapping functions on the entire range of inputs accepted by the look-up table mapping function. The second case is when a neural net is trained to estimate the quantity of interest form the process (such as fuel mass, for example) from redundant and noisy sensor signals. Given upper and lower bounds on sensor noises and on modeling inaccuracies, it is demonstrated how to verify the performance of such a neural network estimator (a “black box”) when compared to a true value of the estimated quantity.

Claims

1. A method of verifying the behavior of pretrained, static, feedforward neural network mapping software having a neural net mapping function ƒ

(x) that is intended to replace look up table mapping software having a look up table mapping function φ

(x), said method comprising executing the following steps on the neural network mapping software and look up table mapping software in a digital computer;

establishing a multi-axis rectangular domain including upper and lower limits of each axis to bound all input vectors x of both said look up table mapping function φ

(X) and said neural net mapping function ƒ

(x);

determining a set of test points within the rectangular domain based on said upper and lower limits of each axis;

determining Lipschitz constant K_ƒ

for said neural net mapping function ƒ

(x);

determining upper and lower value bounds of said neural net mapping function ƒ

(x) for said domain based on a function of said set of test points and said Lipschitz constant K_ƒ

; and

verifying the behavior of the neural network mapping software based on the determination of said upper and lower value bounds.

2. The method of claim 1 including the step of dividing the multi-axis domain into a plurality of cells based on the set of test points.

3. The method of claim 2 wherein the step of determining the upper and lower value bounds includes the steps of:

determining upper and lower value bounds for each cell of the plurality based on a function of the test points of the corresponding cell and the Lipschitz constant K_ƒ

;

selecting an upper value bound from the upper value bounds of the cells as the upper value bound of the neural net mapping function; and

selecting a lower value bound from the lower value bounds of the cells as the lower value bound of the neural net mapping function.

4. The method of claim 3 wherein the maximum of the upper value bounds of the cells is selected as the upper value bound of the neural net mapping function;

and the minimum of the lower value bounds is selected as the lower value bound of the neural net mapping function.

5. The method of claim 2 wherein the step of determining a set of test points includes the step of discretizing each axis i of the multi-axis domain into N_i test point coordinates and N_i−

1 equal intervals of length Δ

_i; and

wherein the step of dividing the domain into a plurality of cells includes forming the cells with the test point coordinates of the axes as its vertices, whereby each cell has 2ⁿ test point vertices, where n is the number of axes in the domain.

6. The method of claim 5 wherein the step of determining upper and lower value bounds of the neural net mapping function ƒ

(x) includes the steps of;

(a) determining values y_j of a neural net mapping ƒ

of each of the 2ⁿ vertices j of a cell of the plurality;

(b) determining a mean y of said values y_j of the cell;

(c) determining a mean distance d of any x within the cell from its vertices;

(d) determining a maximum D_max of the mean distances determined for the cell; and

(e) determining an upper value bound of the cell by the expression;

y+K_ƒ

D_max;

(f) determining a lower value bound of the cell by the expression;

y−

K_ƒ

D_max;

(g) repeating steps (a) through (f) to determine upper and lower value bounds for each cell of the plurality;

(h) selecting the maximum of the upper value bounds of the cells as the upper value bound of the neural net mapping function for the domain; and

(i) selecting the minimum of the lower value bounds of the cells as the lower value bound of the neural net mapping function for the domain.

7. The method of claim 1 including the steps of:

determining Lipschitz constant K_ƒ

′

for the gradient ƒ

(x)′

; and

determining upper and lower error bounds for the neural net and look up table functions based on a function of the set of test points and said Lipschitz constant K_ƒ

′

, whereby if the upper and lower value bounds and said upper and lower error bounds can be determined, then the neural network mapping software is verified.

8. The method of claim 7 including the step of dividing the multi-axis domain into a plurality of cells based on the set of test points.

9. The method of claim 8 wherein the step of determining upper and lower error bounds for said neural net and look up table functions includes the steps of:

determining upper and lower error bounds for each cell of the plurality based on a function of the test points of the corresponding cell, the Lipschitz constant K_ƒ

′

, and a desired constant K_φ

′

;

selecting an upper error bound from the upper error bounds of the cells as the upper error bound of the neural net and look up table mapping functions; and

selecting a lower error bound from the lower error bounds of the cells as the lower error bound of the neural net and look up table mapping functions.

10. The method of claim 9 wherein the maximum of the upper error bounds of the cells is selected as the upper error bound of the neural net and look up table mapping functions;

and the minimum of the lower error bounds is selected as the lower error bound of the neural net and look up table mapping functions.

11. The method of claim 8 wherein the step of determining a set of test points includes the step of discretizing each axis i of the multi-axis domain into N_i test point coordinates and N_i−

1 equal intervals of length Δ

_i; and

wherein the step of dividing the domain into a plurality of cells includes forming the cells with the test point coordinates of the axes as its vertices, whereby each cell has 2ⁿ test point vertices, where n is the number of axes in the domain; and

wherein the step of determining upper and lower error bounds for said neural net and look up table functions includes the steps of;

(a) determining values y_j of a neural net mapping ƒ

of each of the 2ⁿ vertices j of a cell of the plurality;

(b) determining values v_j of a look up table mapping φ

of each of the 2ⁿ vertices j of the cell of the plurality;

(c) determining an error mapping value e_j between each of said y_j and v_j values;

(d) determining a gradient vector y_j′

of the neural net mapping y_j;

(e) determining a maximum mean distance D_max and a maximum mean square distance D_max² from mean distances d_j between an input vector x within the cell and the vertices j of the corresponding cell;

(f) determining a mean error value e of the error values e_j of the cell;

(g) determining a gradient e_j′

of said error mapping e_j of the cell;

(h) determining a desired constant K_φ

′

valid within the cell;

(i) determining maximal and minimal values of directional derivatives at the vertices j of the cell as a function of e_j′

; and

determining bounds G_max and G_min of said maximal and minimal values;

(k) determining upper and lower error bounds for the cell as a function of e, G_max, G_min, K_ƒ

′

, K_φ

′

, D_max, and D_max²;

(l) repeating steps (a) through (k) for each cell of said plurality; and

(m) selecting an upper error bound from the upper error bounds of the cells as the upper error bound of the neural net and look up table mapping functions and selecting a lower error bound from the lower error bounds of the cells as the lower error bound of the neural net and look up table mapping functions.

12. The method of claim 11 wherein the maximum of the upper error bounds of the cells is selected as the upper error bound of the neural net and look up table mapping functions;

and the minimum of the lower error bounds is selected as the lower error bound of the neural net and look up table mapping functions.

13. The method of claim 1 wherein the look up table mapping software being replaced includes entries for mapping inputs of fuel plane coefficients x of a fuel tank to fuel quantity of the fuel tank φ

(x); and

wherein the neural network mapping software replacement yields an estimate of said fuel quantity ƒ

(x).

14. The method of claim 13 including the step of operating the neural network mapping software in a digital processor for estimating fuel quantity of at least one fuel tank.

15. A method of verifying the behavior of pretrained, static, feedforward neural network mapping software having a neural network mapping function ƒ

(ψ

(x)+ζ

), where ψ

(x) is a predetermined mapping of n dimensional state vectors x of a process into m dimensional measurement vectors z=ψ

(x), ζ

is representative of a noise component of the process, and ƒ

(ψ

(x)+ζ

) is an estimate of the desired output parameter y(est) of the process, said method comprising the steps of;

providing model mapping software including a predetermined mapping function φ

(x) for mapping said n dimensional state vectors x directly into a true value y(true) of said desired output parameter;

executing the following steps on the neural network mapping software and model mapping software in a digital computer;

establishing a multi-axis rectangular domain including upper and lower limits of each axis to bound all state vectors x of both said predetermined mapping functions φ

(x) and ψ

(x);

determining a set of test points within the rectangular domain based on said upper and lower limits of each axis;

determining Lipschitz constant K_ƒ

for neural net mapping function ƒ

(ψ

(x));

determining an upper bound ζ

^up and a lower bound ζ

^lo of the noise component ζ

;

determining upper and lower value bounds of said neural net mapping function ƒ

(ψ

(x)+ζ

) for said domain based on a function of said set of test points, said Lipschitz constant K_ƒ

and said upper bound ζ

^up and lower bound ζ

^lo and

verifying the behavior of the neural network mapping software based on the determination of said upper and lower value bounds.

16. The method of claim 15 wherein the predetermined mapping function φ

(x) is provided as a look up table mapping function.

17. The method of claim 15 including the step of dividing the multi-axis domain into a plurality of cells based on the set of test points.

18. The method of claim 17 wherein the step of determining the upper and lower value bounds includes the steps of:

determining upper and lower value bounds for each cell of the plurality based on a function of the test points of the corresponding cell and the Lipschitz constant K_ƒ

;

selecting an upper value bound from the upper value bounds of the cells as the upper value bound of the neural net mapping function; and

selecting a lower value bound from the lower value bounds of the cells as the lower value bound of the neural net mapping function.

19. The method of claim 18 wherein the maximum of the upper value bounds of the cells is selected as the upper value bound of the neural net mapping function;

and the minimum of the lower value bounds is selected as the lower value bound of the neural net mapping function.

20. The method of claim 17 wherein the step of determining a set of test points includes the step of discretizing each axis i of the multi-axis domain into N_i test point coordinates and N_i−

1 equal intervals of length Δ

_i; and

wherein the step of dividing the domain into a plurality of cells includes forming the cells with the test point coordinates of the axes as its vertices, whereby each cell has 2ⁿ test point vertices, where n is the number of axes in the domain.

21. The method of claim 20 wherein the step of determining upper and lower value bounds of the neural net mapping function ƒ

(ψ

(x)+ζ

) includes the steps of;

(a) determining values y_j of a predetermined mapping ƒ

(ψ

(x_j)) of each x_j of the 2ⁿ vertices j of a cell of the plurality;

(b) determining a Lipschitz constant K_ψ

for the cell based on said values y_j of the cell;

(c) determining a mean y of said values y_j of the cell;

(d) determining a maximum mean distance D_max for the cell from distances of any x within the cell from its vertices;

(e) determining a maximum value ζ

_max of the noise component ζ

from its upper and lower bounds;

(f) determining an upper value bound of the cell by the expression;

22. The method of claim 15 including the steps of:

determining Lipschitz constant K_ƒ

′

for the gradient ƒ

(ψ

(x))′

;

determining upper and lower error bounds for said neural net function ƒ

(ψ

(x)+ζ

) and predetermined mapping function φ

(x) based on a function of said set of test points, said Lipschitz constant K_ƒ

′

, and said upper bound ζ

^up and a lower bound ζ

^lo, whereby if the upper and lower value bounds and said upper and lower error bounds can be determined, then the neural network mapping software is verified.

23. The method of claim 22 including the step of dividing the multi-axis domain into a plurality of cells based on the set of test points.

24. The method of claim 23 including decomposing the error between neural net mapping function ƒ

(ψ

(x)+ζ

) and the predetermined mapping function φ

(x) into a noise free error component F(x)−

φ

(x) and a term representative of noise magnitude.

25. The method of claim 23 wherein the step of determining the upper and lower error bounds includes the steps of:

determining upper and lower error bounds for each cell of the plurality based on a function of the test points of the corresponding cell, the Lipschitz constants K_ƒ

and K_ƒ

′ and

Lipschitz constants K_ψ

and K_ψ

′

;

selecting an upper error bound from the upper error bounds of the cells as the upper error bound of the neural net mapping function and predetermined mapping φ

(x); and

selecting a lower error bound from the lower error bounds of the cells as the lower error bound of the neural net mapping function and predetermined mapping φ

(x).

26. The method of claim 25 wherein the maximum of the upper error bounds of the cells is selected as the upper error bound of the neural net mapping function and predetermined mapping φ

(x); and

the minimum of the lower error bounds is selected as the lower error bound of the neural net mapping function and predetermined mapping φ

(x).

27. The method of claim 23 wherein the step of determining a set of test points includes the step of discretizing each axis i of the multi-axis domain into N_i test point coordinates and N_i−

1 equal intervals of length Δ

_i; and

wherein the step of dividing the domain into a plurality of cells includes forming the cells with the test point coordinates of the axes as its vertices, whereby each cell has 2ⁿ test point vertices, where n is the number of axes in the domain; and

wherein the step of determining upper and lower error bounds for the neural net mapping function and predetermined mapping φ

(x) includes the steps of;

(a) determining values y_j of a neural net function mapping ƒ

(ψ

(x_j)) of each x_j of the 2ⁿ vertices j of a cell of the plurality;

(b) determining values v_j of a predetermined mapping φ

(x_j) of each x_j of the 2ⁿ vertices j of the cell of the plurality;

(c) determining an error mapping value e_j between each of said y_j and v_j values;

(d) determining a gradient vector y_j′

of the neural net mapping y_j;

(e) determining a maximum mean distance D_max and a maximum mean square distance D_max² from mean distances d_j between an input vector x within the cell and the vertices j of the corresponding cell;

(f) determining a mean error value e of the error values e_j of the cell;

(g) determining a gradient e_j′

of said error mapping e_j of the cell;

(h) determining Lipschitz constants K_φ

′

, K_ψ

, and K_ψ

′

valid within the cell;

(i) determining maximal and minimal values of directional derivatives at the vertices j of the cell as a function of e_j′

; and

determining bounds G_max and G_min of said maximal and minimal values;

(k) determining upper and lower error bounds for the cell as a function of e, G_max, G_min, K_ƒ

, K_ƒ

′

, K_φ

′

, D_max, D_max², K_ψ

, and K_ψ

′

;

(l) repeating steps (a) through (k) for each cell of said plurality;

(m) selecting an upper error bound from the upper error bounds of the cells and selecting a lower error bound from the lower error bounds of the cells;

(n) determining a value ζ

_max of the noise component ζ

from its upper and lower bounds; and

(o) determining the lower error bound of the neural net mapping function and predetermined mapping φ

(x) by subtracting a product K_ƒ

ζ

_max from the selected lower error bound and determining the upper error bound of the neural net mapping function and predetermined mapping φ

(x) by adding the product K_ƒ

ζ

_max to the selected upper error bound.

28. The method of claim 27 wherein the maximum of the upper error bounds of the cells is selected as the upper error bound of the neural net mapping function and predetermined mapping φ

(x); and

the minimum of the lower error bounds is selected as the lower error bound of the neural net mapping function and predetermined mapping φ

(x).

29. The method of claim 15 wherein the predetermined mapping function ψ

(x) is provided as a look up table mapping function coded in software.

30. The method of claim 15 wherein the predetermined mapping function ψ

(x) is provided as a computer simulation model of the process coded in software.

31. The method of claim 15 wherein the state vector x is provided as states of a fuel tank;

wherein the measurement vector z is provided as an estimation of measurements of the states of the fuel tank;

wherein ζ

is provided as a noise component in the measurement of the state of the fuel tank; and

including the step of operating the neural network mapping software in a digital processor for estimating fuel quantity of at least one fuel tank.