Analysing Machine Learning Models With Imandra¶
In this notebook we show how Imandra can be used to analyse and reason about models that have been learnt from data, an important and exciting topic bridging the gap between formal methods and machine learning (ML). Brief notes and some links are included, but for a fuller explanation (with code snippets included for reference) see our corresponding Medium post. You can also find all of our code for both learning and analysing our models on GitHub.
To illustrate this approach we'll be looking at (relatively simple) examples from two of the most common tasks within supervised learning (and ML more generally): classification and regression. In particular, we'll show how two of the most common kinds of model used to perform these tasks, random forests and neural networks, can be analysed using Imandra. For each task we'll use a real-world benchmark dataset from the UCI Machine Learning Repository and create our models using Python with some standard ML libraries.
We'll mostly be working with reals in this notebook so we'll start by installing a pretty printer so that we're not overrun with digits.
In [1]:
let pp_approx fmt r = CCFormat.fprintf fmt "%s" (Real.to_string_approx r) [@@program]
#install_printer pp_approx
Out[1]:
val pp_approx : Format.formatter -> real -> unit = <fun>
Classification¶
In a classification task we want to learn to predict the label of a datapoint based on previous data. In the classic Wisconsin Breast Cancer (Diagnostic) dataset) the task is to predict whether the cancer is benign or malignant based on the features of cell nuclei. In the dataset we have the following variables:
1. ID number
2. Diagnosis (malignant or benign)
3-32. Real values for the mean, standard error, and the 'worst' value for each cell nucleus'
a) Radius
b) Texture
c) Perimeter
d) Area
e) Smoothness
f) Compactness
g) Concavity
h) Concave points
i) Symmetry
j) Fractal dimensionAs is standard practice we pre-process the data before learning. First we standardise each variable to have zero mean and unit variance, then remove all but one from sets of highly correlated variables, along with those that have low mutual information with respect to the target variable. The data is split into training (80%) and test (20%) sets and we use Scikit-Learn to learn a random forest of 3 decision trees of maximum depth 3. As this is a relatively straightforward problem even this simple model achieves a fairly high accuracy. Using a short Python script each tree is then converted to Imandra Modelling Language (IML) and can be reasoned about using Imandra.
In [2]:
let tree_0 (f_0 : real) (f_1 : real) (f_2 : real) (f_3 : real) (f_4 : real) (f_5 : real) (f_6 : real) = let open Real in
if f_2 <=. (-0.10815) then
if f_0 <=. (0.26348) then
if f_6 <=. (-0.06176) then
(236.0, 1.0)
else
(17.0, 5.0)
else
if f_3 <=. (-0.54236) then
(8.0, 2.0)
else
(3.0, 7.0)
else
if f_6 <=. (0.09812) then
if f_6 <=. (-0.17063) then
(24.0, 0.0)
else
(4.0, 2.0)
else
if f_2 <=. (2.65413) then
(6.0, 128.0)
else
(7.0, 5.0);;
let tree_1 (f_0 : real) (f_1 : real) (f_2 : real) (f_3 : real) (f_4 : real) (f_5 : real) (f_6 : real) = let open Real in
if f_5 <=. (-0.05799) then
if f_0 <=. (0.68524) then
if f_1 <=. (-0.83180) then
(110.0, 3.0)
else
(137.0, 0.0)
else
if f_3 <=. (0.45504) then
(1.0, 8.0)
else
(0.0, 7.0)
else
if f_0 <=. (-0.18668) then
if f_6 <=. (0.45214) then
(39.0, 0.0)
else
(2.0, 11.0)
else
if f_6 <=. (-0.00009) then
(8.0, 4.0)
else
(5.0, 120.0);;
let tree_2 (f_0 : real) (f_1 : real) (f_2 : real) (f_3 : real) (f_4 : real) (f_5 : real) (f_6 : real) = let open Real in
if f_2 <=. (0.10459) then
if f_5 <=. (-0.38015) then
if f_5 <=. (-0.60659) then
(139.0, 1.0)
else
(44.0, 3.0)
else
if f_6 <=. (-0.07927) then
(38.0, 2.0)
else
(25.0, 17.0)
else
if f_6 <=. (0.46888) then
if f_3 <=. (0.41642) then
(28.0, 3.0)
else
(1.0, 4.0)
else
if f_2 <=. (1.74327) then
(3.0, 122.0)
else
(4.0, 21.0);;
let rf (f_0, f_1, f_2, f_3, f_4, f_5, f_6) = let open Real in
let (a_0, b_0) = tree_0 f_0 f_1 f_2 f_3 f_4 f_5 f_6 in
let (a_1, b_1) = tree_1 f_0 f_1 f_2 f_3 f_4 f_5 f_6 in
let (a_2, b_2) = tree_2 f_0 f_1 f_2 f_3 f_4 f_5 f_6 in
let a = a_0 + a_1 + a_2 in
let b = b_0 + b_1 + b_2 in
(a, b);;
Out[2]:
val tree_0 : real -> real -> real -> real -> real -> real -> real -> real * real = <fun> val tree_1 : real -> real -> real -> real -> real -> real -> real -> real * real = <fun> val tree_2 : real -> real -> real -> real -> real -> real -> real -> real * real = <fun> val rf : real * real * real * real * real * real * real -> real * real = <fun>
We can create a custom input type in Imandra for our model, so that we can keep track of the different features of our data.
In [3]:
type rf_input = {
radius_mean : real;
compactness_mean : real;
concavity_mean : real;
radius_se : real;
compactness_worst : real;
concavity_worst : real;
concave_points_worst : real;
}
Out[3]:
type rf_input = {
radius_mean : real;
compactness_mean : real;
concavity_mean : real;
radius_se : real;
compactness_worst : real;
concavity_worst : real;
concave_points_worst : real;
}
However, remember that we also processed our data before learning. To make things easier we'll add in a function applying this transformation to each input variable. Here we simply use some multiplicative and additive scaling values extracted during our data pre-processing stage. After that we can define a full model which combines these pre-processing steps and the random forest.
In [4]:
let process_rf_input input = let open Real in
let f_0 = (input.radius_mean - 14.12729) / 3.52405 in
let f_1 = (input.compactness_mean - 0.10434) / 0.05281 in
let f_2 = (input.concavity_mean - 0.08880) / 0.07972 in
let f_3 = (input.radius_se - 0.40517) / 0.27731 in
let f_4 = (input.compactness_worst - 0.25427) / 0.15734 in
let f_5 = (input.concavity_worst - 0.27219) / 0.20862 in
let f_6 = (input.concave_points_worst - 0.11461) / 0.06573 in
(f_0, f_1, f_2, f_3, f_4, f_5, f_6)
let process_rf_output c =
let (a, b) = c in
if a >. b then "benign" else "malignant"
let rf_model input = input |> process_rf_input |> rf |> process_rf_output
Out[4]:
val process_rf_input : rf_input -> real * real * real * real * real * real * real = <fun> val process_rf_output : real * real -> string = <fun> val rf_model : rf_input -> string = <fun>
As our model is fully executable we can both query it as well as find counterexamples, prove properties, apply logical side-conditions, decompose its regions, and more. As a quick sanity check to make sure everything is working, let's run a datum from our dataset through the model. In particular, we'll input (17.99, 0.2776, 0.3001, 1.095, 0.6656, 0.7119, 0.2654) which is classified as malignant in the data.
In [5]:
let x = {
radius_mean = 17.99;
compactness_mean = 0.2776;
concavity_mean = 0.3001;
radius_se = 1.095;
compactness_worst = 0.6656;
concavity_worst = 0.7119;
concave_points_worst = 0.7119;
}
let y = rf_model x
Out[5]:
val x : rf_input =
{radius_mean = 17.99; compactness_mean = 0.2776; concavity_mean = 0.3001;
radius_se = 1.095; compactness_worst = 0.6656; concavity_worst = 0.7119;
concave_points_worst = 0.7119}
val y : string = "malignant"
Great, just what we'd expect. Now we'll use Imandra to generate an example datapoint for us given that diagnosis is benign.
In [6]:
instance (fun x -> rf_model x = "benign")
Out[6]:
- : rf_input -> bool = <fun> module CX : sig val x : rf_input end
Instance (after 0 steps, 0.020s):
let x : rf_input =
{radius_mean = (-216972096653/500000000);
compactness_mean = (-140469793679/500000000);
concavity_mean = (-4048959910859/500000000); radius_se = 5853;
compactness_worst = 9; concavity_worst = (-5709271784029/5000000000);
concave_points_worst = (-47569488241/78125000)}
Instance
Loading..
proof attempt
| ground_instances: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||
| definitions: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||
| inductions: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||
| search_time: | 0.020s | ||||||||||||||||||||||||||||||||||||||||||||||
| details: | Expand
|
Expand
start[0.020s] let (_x_0 : real) = ….2 in let (_x_1 : (Real.t * Real.t)) = if _x_0 <= (-2163/20000) then … else … in let (_x_2 : (Real.t * Real.t)) = if ….5 <= (-5799/100000) then … else … in let (_x_3 : (Real.t * Real.t)) = if _x_0 <= 10459/100000 then … else … in (if _x_1.0 +. _x_2.0 +. _x_3.0 > _x_1.1 +. _x_2.1 +. _x_3.1 then "benign" else "malignant") = "benign"simplify
into: let (_x_0 : real) = ( :var_0: ).concavity_mean in let (_x_1 : real) = ( :var_0: ).concave_points_worst in let (_x_2 : real) = ( :var_0: ).radius_se in let (_x_3 : real) = ( :var_0: ).radius_mean in let (_x_4 : (Real.t * Real.t)) = if _x_0 <= 40089141/500000000 then if _x_3 <= 7527903347/500000000 then if _x_1 <= 8636759/78125000 then … else … else if _x_2 <= 636920371/2500000000 then … else … else if _x_1 <= 302648569/2500000000 then if _x_1 <= 1033944901/10000000000 then … else … else if _x_0 <= 750968109/2500000000 then … else … in let (_x_5 : real) = ( :var_0: ).concavity_worst in let (_x_6 : (Real.t * Real.t)) = if _x_5 <= 1300460631/5000000000 then if _x_3 <= 8271055011/500000000 then if ( :var_0: ).compactness_mean <= 30206321/500000000 then … else … else if _x_2 <= 166049107/312500000 then … else … else if _x_3 <= 6734710173/500000000 then if _x_1 <= 721645811/5000000000 then … else … else if _x_1 <= 1146040843/10000000000 then … else … in let (_x_7 : (Real.t * Real.t)) = if _x_0 <= 242844787/2500000000 then if _x_5 <= 192883107/1000000000 then if _x_5 <= 728215971/5000000000 then … else … else if _x_1 <= 1093995829/10000000000 then … else … else if _x_1 <= 181786853/1250000000 then if _x_2 <= 2603237151/5000000000 then … else … else if _x_0 <= 569433711/2500000000 then … else … in (if _x_4.0 +. _x_6.0 +. _x_7.0 <= _x_4.1 +. _x_6.1 +. _x_7.1 then "malignant" else "benign") = "benign"expansions: []
rewrite_steps: forward_chaining: - Sat (Some let x : rf_input = {radius_mean = (Q.of_string "-216972096653/500000000"); compactness_mean = (Q.of_string "-140469793679/500000000"); concavity_mean = (Q.of_string "-4048959910859/500000000"); radius_se = (Q.of_nativeint (5853n)); compactness_worst = (Q.of_nativeint (9n)); concavity_worst = (Q.of_string "-5709271784029/5000000000"); concave_points_worst = (Q.of_string "-47569488241/78125000")} )
Loading..
In [7]:
CX.x
Out[7]:
- : rf_input =
{radius_mean = -433.944193306; compactness_mean = -280.939587358;
concavity_mean = -8097.91982172; radius_se = 5853.; compactness_worst = 9.;
concavity_worst = -1141.85435681; concave_points_worst = -608.889449485}
This looks a bit funny however; notice how the unspecified input variables are unbounded in a way that doesn't make sense with respect to the data. In general we might only care about the performance of our model when some reasonable bounds are placed on the input (for example, the mean radius can't be negative, and if the values for this variable in our dataset range between 6.98 and 28.11 we wouldn't really expect any value greater than, say, 35). Using the description of each variable in the dataset we can form a condition describing valid and reasonable inputs to our model. In machine learning more generally, we are typically only interested in the performance and quality of a model over some particular distribution of data, which we often have particular prior beliefs about.
In [8]:
let is_valid_rf input =
5.0 <=. input.radius_mean && input.radius_mean <=. 35.0 &&
0.0 <=. input.compactness_mean && input.compactness_mean <=. 0.4 &&
0.0 <=. input.concavity_mean && input.concavity_mean <=. 0.5 &&
0.0 <=. input.radius_se && input.radius_se <=. 3.5 &&
0.0 <=. input.compactness_worst && input.compactness_worst <=. 1.2 &&
0.0 <=. input.concavity_worst && input.concavity_worst <=. 1.5 &&
0.0 <=. input.concave_points_worst && input.concave_points_worst <=. 0.35
instance (fun x -> rf_model x = "benign" && is_valid_rf x)
Out[8]:
val is_valid_rf : rf_input -> bool = <fun> - : rf_input -> bool = <fun> module CX : sig val x : rf_input end
Instance (after 0 steps, 0.031s):
let x : rf_input =
{radius_mean = 15370932811137/2500000000000;
compactness_mean = 13562638129/5000000000000;
concavity_mean = 11265048621/5000000000000; radius_se = 40971/20000;
compactness_worst = 321/5000;
concavity_worst = 443483526339/50000000000000;
concave_points_worst = 34970237191/390625000000}
Instance
Loading..
proof attempt
| ground_instances: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||
| definitions: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||
| inductions: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||
| search_time: | 0.031s | ||||||||||||||||||||||||||||||||||||||||||||||
| details: | Expand
|
Expand
start[0.031s] let (_x_0 : real) = ….2 in let (_x_1 : (Real.t * Real.t)) = if _x_0 <= (-2163/20000) then … else … in let (_x_2 : (Real.t * Real.t)) = if ….5 <= (-5799/100000) then … else … in let (_x_3 : (Real.t * Real.t)) = if _x_0 <= 10459/100000 then … else … in let (_x_4 : real) = ( :var_0: ).radius_mean in let (_x_5 : real) = ( :var_0: ).compactness_mean in let (_x_6 : real) = ( :var_0: ).concavity_mean in let (_x_7 : real) = ( :var_0: ).radius_se in let (_x_8 : real) = ( :var_0: ).compactness_worst in let (_x_9 : real) = ( :var_0: ).concavity_worst in let (_x_10 : real) = ( :var_0: ).concave_points_worst in ((if _x_1.0 +. _x_2.0 +. _x_3.0 > _x_1.1 +. _x_2.1 +. _x_3.1 then "benign" else "malignant") = "benign") && ((5 <= _x_4) && ((_x_4 <= 35) && ((0 <= _x_5) && ((_x_5 <= 2/5) && ((0 <= _x_6) && ((_x_6 <= 1/2) && ((0 <= _x_7) && ((_x_7 <= 7/2) && ((0 <= _x_8) && ((_x_8 <= 6/5) && ((0 <= _x_9) && ((_x_9 <= 3/2) && ((0 <= _x_10) && (_x_10 <= 7/20))))))))))))))simplify
into: let (_x_0 : real) = ( :var_0: ).concavity_mean in let (_x_1 : real) = ( :var_0: ).concave_points_worst in let (_x_2 : real) = ( :var_0: ).radius_se in let (_x_3 : real) = ( :var_0: ).radius_mean in let (_x_4 : (Real.t * Real.t)) = if _x_0 <= 40089141/500000000 then if _x_3 <= 7527903347/500000000 then if _x_1 <= 8636759/78125000 then … else … else if _x_2 <= 636920371/2500000000 then … else … else if _x_1 <= 302648569/2500000000 then if _x_1 <= 1033944901/10000000000 then … else … else if _x_0 <= 750968109/2500000000 then … else … in let (_x_5 : real) = ( :var_0: ).compactness_mean in let (_x_6 : real) = ( :var_0: ).concavity_worst in let (_x_7 : (Real.t * Real.t)) = if _x_6 <= 1300460631/5000000000 then if _x_3 <= 8271055011/500000000 then if _x_5 <= 30206321/500000000 then … else … else if _x_2 <= 166049107/312500000 then … else … else if _x_3 <= 6734710173/500000000 then if _x_1 <= 721645811/5000000000 then … else … else if _x_1 <= 1146040843/10000000000 then … else … in let (_x_8 : (Real.t * Real.t)) = if _x_0 <= 242844787/2500000000 then if _x_6 <= 192883107/1000000000 then if _x_6 <= 728215971/5000000000 then … else … else if _x_1 <= 1093995829/10000000000 then … else … else if _x_1 <= 181786853/1250000000 then if _x_2 <= 2603237151/5000000000 then … else … else if _x_0 <= 569433711/2500000000 then … else … in let (_x_9 : real) = ( :var_0: ).compactness_worst in ((if _x_4.0 +. _x_7.0 +. _x_8.0 <= _x_4.1 +. _x_7.1 +. _x_8.1 then "malignant" else "benign") = "benign") && (5 <= _x_3) && (_x_3 <= 35) && (0 <= _x_5) && (_x_5 <= 2/5) && (0 <= _x_0) && (_x_0 <= 1/2) && (0 <= _x_2) && (_x_2 <= 7/2) && (0 <= _x_9) && (_x_9 <= 6/5) && (0 <= _x_6) && (_x_6 <= 3/2) && (0 <= _x_1) && (_x_1 <= 7/20)expansions: []
rewrite_steps: forward_chaining: - Sat (Some let x : rf_input = {radius_mean = (Q.of_string "15370932811137/2500000000000"); compactness_mean = (Q.of_string "13562638129/5000000000000"); concavity_mean = (Q.of_string "11265048621/5000000000000"); radius_se = (Q.of_string "40971/20000"); compactness_worst = (Q.of_string "321/5000"); concavity_worst = (Q.of_string "443483526339/50000000000000"); concave_points_worst = (Q.of_string "34970237191/390625000000")} )
Loading..
In [9]:
CX.x
Out[9]:
- : rf_input =
{radius_mean = 6.14837312445; compactness_mean = 0.0027125276258;
concavity_mean = 0.0022530097242; radius_se = 2.04855;
compactness_worst = 0.0642; concavity_worst = 0.00886967052678;
concave_points_worst = 0.089523807209}
This looks much better. Now let's move on to reasoning about our model in more interesting ways. One thing we can do is check the validity of certain constraints we might want our model to satisfy. For example, if the surface of a cell nucleus has many, large concave sections then is a particularly negative sign indicating that the cancer is likely to be malignant. We can use Imandra to easily verify that our model always classifies a sample of highly concave cells as malignant.
In [10]:
verify (fun x -> is_valid_rf x
&& x.concavity_mean >=. 0.4
&& x.concavity_worst >=. 1.0
&& x.concave_points_worst >=. 0.25
==> rf_model x = "malignant")
Out[10]:
- : rf_input -> bool = <fun>
Proved
proof
| ground_instances: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||
| definitions: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||
| inductions: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||
| search_time: | 0.022s | ||||||||||||||||||||||||||||||||||||||||||||||||
| details: | Expand
|
Expand
start[0.022s] let (_x_0 : real) = ( :var_0: ).radius_mean in let (_x_1 : real) = ( :var_0: ).compactness_mean in let (_x_2 : real) = ( :var_0: ).concavity_mean in let (_x_3 : real) = ( :var_0: ).radius_se in let (_x_4 : real) = ( :var_0: ).compactness_worst in let (_x_5 : real) = ( :var_0: ).concavity_worst in let (_x_6 : real) = ( :var_0: ).concave_points_worst in let (_x_7 : real) = ….2 in let (_x_8 : (Real.t * Real.t)) = if _x_7 <= (-2163/20000) then … else … in let (_x_9 : (Real.t * Real.t)) = if ….5 <= (-5799/100000) then … else … in let (_x_10 : (Real.t * Real.t)) = if _x_7 <= 10459/100000 then … else … in (5 <= _x_0) && ((_x_0 <= 35) && ((0 <= _x_1) && ((_x_1 <= 2/5) && ((0 <= _x_2) && ((_x_2 <= 1/2) && ((0 <= _x_3) && ((_x_3 <= 7/2) && ((0 <= _x_4) && ((_x_4 <= 6/5) && ((0 <= _x_5) && ((_x_5 <= 3/2) && ((0 <= _x_6) && (_x_6 <= 7/20))))))))))))) && ((_x_2 >= 2/5) && ((_x_5 >= 1) && (_x_6 >= 1/4))) ==> (if _x_8.0 +. _x_9.0 +. _x_10.0 > _x_8.1 +. _x_9.1 +. _x_10.1 then "benign" else "malignant") = "malignant"simplify
into: let (_x_0 : real) = ( :var_0: ).radius_mean in let (_x_1 : real) = ( :var_0: ).compactness_mean in let (_x_2 : real) = ( :var_0: ).concavity_mean in let (_x_3 : real) = ( :var_0: ).radius_se in let (_x_4 : real) = ( :var_0: ).compactness_worst in let (_x_5 : real) = ( :var_0: ).concavity_worst in let (_x_6 : real) = ( :var_0: ).concave_points_worst in let (_x_7 : (Real.t * Real.t)) = if _x_2 <= 40089141/500000000 then if _x_0 <= 7527903347/500000000 then if _x_6 <= 8636759/78125000 then … else … else if _x_3 <= 636920371/2500000000 then … else … else if _x_6 <= 302648569/2500000000 then if _x_6 <= 1033944901/10000000000 then … else … else if _x_2 <= 750968109/2500000000 then … else … in let (_x_8 : (Real.t * Real.t)) = if _x_5 <= 1300460631/5000000000 then if _x_0 <= 8271055011/500000000 then if _x_1 <= 30206321/500000000 then … else … else if _x_3 <= 166049107/312500000 then … else … else if _x_0 <= 6734710173/500000000 then if _x_6 <= 721645811/5000000000 then … else … else if _x_6 <= 1146040843/10000000000 then … else … in let (_x_9 : (Real.t * Real.t)) = if _x_2 <= 242844787/2500000000 then if _x_5 <= 192883107/1000000000 then if _x_5 <= 728215971/5000000000 then … else … else if _x_6 <= 1093995829/10000000000 then … else … else if _x_6 <= 181786853/1250000000 then if _x_3 <= 2603237151/5000000000 then … else … else if _x_2 <= 569433711/2500000000 then … else … in not ((5 <= _x_0) && (_x_0 <= 35) && (0 <= _x_1) && (_x_1 <= 2/5) && (0 <= _x_2) && (_x_2 <= 1/2) && (0 <= _x_3) && (_x_3 <= 7/2) && (0 <= _x_4) && (_x_4 <= 6/5) && (0 <= _x_5) && (_x_5 <= 3/2) && (0 <= _x_6) && (_x_6 <= 7/20) && (_x_2 >= 2/5) && (_x_5 >= 1) && (_x_6 >= 1/4)) || ((if _x_7.0 +. _x_8.0 +. _x_9.0 <= _x_7.1 +. _x_8.1 +. _x_9.1 then "malignant" else "benign") = "malignant")expansions: []
rewrite_steps: forward_chaining: - Unsat
Loading..
Loading..
The nested if ... then ... else statements in how the trees are defined mean that they are a prime candidate for Imandra's region decomposition functionality. As well as the total model we can of course also decompose the individual trees making up the ensemble.
In [11]:
Modular_decomp.top ~assuming:"is_valid_rf" "rf_model"
Out[11]:
- : Modular_decomp_intf.decomp_ref = <abstr>
Regions details
No group selected.
- Concrete regions are numbered
- Unnumbered regions are groups whose children share a particular constraint
- Click on a region to view its details
- Double click on a region to zoom in on it
- Shift+double click to zoom out
- Hit escape to reset back to the top
Direct sub-regions: -
Contained regions: -
Constraints
<constraint>
Invariant
<invariant>
decomp of (rf_model input
| Reg_id | Constraints | Invariant |
|---|---|---|
| 173 |
| "benign" |
| 172 |
| "benign" |
| 171 |
| "benign" |
| 170 |
| "benign" |
| 169 |
| "benign" |
| 168 |
| "benign" |
| 167 |
| "benign" |
| 166 |
| "benign" |
| 165 |
| "benign" |
| 164 |
| "benign" |
| 163 |
| "benign" |
| 162 |
| "benign" |
| 161 |
| "benign" |
| 160 |
| "benign" |
| 159 |
| "benign" |
| 158 |
| "benign" |
| 157 |
| "benign" |
| 156 |
| "benign" |
| 155 |
| "benign" |
| 154 |
| "benign" |
| 153 |
| "benign" |
| 152 |
| "benign" |
| 151 |
| "benign" |
| 150 |
| "benign" |
| 149 |
| "benign" |
| 148 |
| "benign" |
| 147 |
| "benign" |
| 146 |
| "benign" |
| 145 |
| "benign" |
| 144 |
| "benign" |
| 143 |
| "benign" |
| 142 |
| "benign" |
| 141 |
| "benign" |
| 140 |
| "benign" |
| 139 |
| "benign" |
| 138 |
| "benign" |
| 137 |
| "benign" |
| 136 |
| "benign" |
| 135 |
| "benign" |
| 134 |
| "benign" |
| 133 |
| "benign" |
| 132 |
| "benign" |
| 131 |
| "benign" |
| 130 |
| "benign" |
| 129 |
| "benign" |
| 128 |
| "benign" |
| 127 |
| "benign" |
| 126 |
| "benign" |
| 125 |
| "benign" |
| 124 |
| "benign" |
| 123 |
| "benign" |
| 122 |
| "benign" |
| 121 |
| "benign" |
| 120 |
| "benign" |
| 119 |
| "benign" |
| 118 |
| "benign" |
| 117 |
| "benign" |
| 116 |
| "benign" |
| 115 |
| "benign" |
| 114 |
| "benign" |
| 113 |
| "benign" |
| 112 |
| "benign" |
| 111 |
| "benign" |
| 110 |
| "benign" |
| 109 |
| "benign" |
| 108 |
| "benign" |
| 107 |
| "benign" |
| 106 |
| "benign" |
| 105 |
| "benign" |
| 104 |
| "benign" |
| 103 |
| "benign" |
| 102 |
| "benign" |
| 101 |
| "benign" |
| 100 |
| "benign" |
| 99 |
| "benign" |
| 98 |
| "benign" |
| 97 |
| "benign" |
| 96 |
| "benign" |
| 95 |
| "benign" |
| 94 |
| "benign" |
| 93 |
| "benign" |
| 92 |
| "benign" |
| 91 |
| "benign" |
| 90 |
| "benign" |
| 89 |
| "benign" |
| 88 |
| "benign" |
| 87 |
| "benign" |
| 86 |
| "benign" |
| 85 |
| "benign" |
| 84 |
| "benign" |
| 83 |
| "benign" |
| 82 |
| "benign" |
| 81 |
| "benign" |
| 80 |
| "benign" |
| 79 |
| "benign" |
| 78 |
| "benign" |
| 77 |
| "benign" |
| 76 |
| "benign" |
| 75 |
| "benign" |
| 74 |
| "benign" |
| 73 |
| "benign" |
| 72 |
| "benign" |
| 71 |
| "benign" |
| 70 |
| "benign" |
| 69 |
| "benign" |
| 68 |
| "benign" |
| 67 |
| "benign" |
| 66 |
| "benign" |
| 65 |
| "benign" |
| 64 |
| "benign" |
| 63 |
| "benign" |
| 62 |
| "benign" |
| 61 |
| "benign" |
| 60 |
| "benign" |
| 59 |
| "benign" |
| 58 |
| "benign" |
| 57 |
| "benign" |
| 56 |
| "benign" |
| 55 |
| "benign" |
| 54 |
| "benign" |
| 53 |
| "benign" |
| 52 |
| "benign" |
| 51 |
| "benign" |
| 50 |
| "benign" |
| 49 |
| "benign" |
| 48 |
| "malignant" |
| 47 |
| "malignant" |
| 46 |
| "malignant" |
| 45 |
| "malignant" |
| 44 |
| "malignant" |
| 43 |
| "malignant" |
| 42 |
| "malignant" |
| 41 |
| "malignant" |
| 40 |
| "malignant" |
| 39 |
| "malignant" |
| 38 |
| "malignant" |
| 37 |
| "malignant" |
| 36 |
| "malignant" |
| 35 |
| "malignant" |
| 34 |
| "malignant" |
| 33 |
| "malignant" |
| 32 |
| "malignant" |
| 31 |
| "malignant" |
| 30 |
| "malignant" |
| 29 |
| "malignant" |
| 28 |
| "malignant" |
| 27 |
| "malignant" |
| 26 |
| "malignant" |
| 25 |
| "malignant" |
| 24 |
| "malignant" |
| 23 |
| "malignant" |
| 22 |
| "malignant" |
| 21 |
| "malignant" |
| 20 |
| "malignant" |
| 19 |
| "malignant" |
| 18 |
| "malignant" |
| 17 |
| "malignant" |
| 16 |
| "malignant" |
| 15 |
| "malignant" |
| 14 |
| "malignant" |
| 13 |
| "malignant" |
| 12 |
| "malignant" |
| 11 |
| "malignant" |
| 10 |
| "malignant" |
| 9 |
| "malignant" |
| 8 |
| "malignant" |
| 7 |
| "malignant" |
| 6 |
| "malignant" |
| 5 |
| "malignant" |
| 4 |
| "malignant" |
| 3 |
| "malignant" |
| 2 |
| "malignant" |
| 1 |
| "malignant" |
| 0 |
| "malignant" |
In [12]:
Modular_decomp.top "tree_0"
Out[12]:
- : Modular_decomp_intf.decomp_ref = <abstr>
Regions details
No group selected.
- Concrete regions are numbered
- Unnumbered regions are groups whose children share a particular constraint
- Click on a region to view its details
- Double click on a region to zoom in on it
- Shift+double click to zoom out
- Hit escape to reset back to the top
Direct sub-regions: -
Contained regions: -
Constraints
<constraint>
Invariant
<invariant>
decomp of (tree_0 f_0, f_1, f_2, f_3, f_4, f_5, f_6
| Reg_id | Constraints | Invariant |
|---|---|---|
| 7 |
| (7, 5) |
| 6 |
| (6, 128) |
| 5 |
| (4, 2) |
| 4 |
| (24, 0) |
| 3 |
| (3, 7) |
| 2 |
| (8, 2) |
| 1 |
| (17, 5) |
| 0 |
| (236, 1) |
We can also use side conditions on the region decomposition of our model by using the ~assuming: flag. One application here is in simulating partial observability. Perhaps we know most of the measurements for a particular set of cells and we'd like to see how the classification of the input depends on the remaining features. Let's imagine that we only have the concavity measurements for a particular patient's cell sample and we'd like to see how the output of our model depends on the values of the other features.
In [13]:
let partial_observation x =
is_valid_rf x &&
x.concavity_mean = 0.04295 &&
x.concavity_worst = 0.26000 &&
x.concave_points_worst = 0.11460;;
Modular_decomp.top ~prune:true ~assuming:"partial_observation" "rf_model" [@@program];;
Out[13]:
val partial_observation : rf_input -> bool = <fun> - : Modular_decomp_intf.decomp_ref = <abstr>
Regions details
No group selected.
- Concrete regions are numbered
- Unnumbered regions are groups whose children share a particular constraint
- Click on a region to view its details
- Double click on a region to zoom in on it
- Shift+double click to zoom out
- Hit escape to reset back to the top
Direct sub-regions: -
Contained regions: -
Constraints
<constraint>
Invariant
<invariant>
decomp of (rf_model input
| Reg_id | Constraints | Invariant |
|---|---|---|
| 173 |
| "benign" |
| 172 |
| "benign" |
| 171 |
| "benign" |
| 170 |
| "benign" |
| 169 |
| "benign" |
| 168 |
| "benign" |
| 167 |
| "benign" |
| 166 |
| "benign" |
| 165 |
| "benign" |
| 164 |
| "benign" |
| 163 |
| "benign" |
| 162 |
| "benign" |
| 161 |
| "benign" |
| 160 |
| "benign" |
| 159 |
| "benign" |
| 158 |
| "benign" |
| 157 |
| "benign" |
| 156 |
| "benign" |
| 155 |
| "benign" |
| 154 |
| "benign" |
| 153 |
| "benign" |
| 152 |
| "benign" |
| 151 |
| "benign" |
| 150 |
| "benign" |
| 149 |
| "benign" |
| 148 |
| "benign" |
| 147 |
| "benign" |
| 146 |
| "benign" |
| 145 |
| "benign" |
| 144 |
| "benign" |
| 143 |
| "benign" |
| 142 |
| "benign" |
| 141 |
| "benign" |
| 140 |
| "benign" |
| 139 |
| "benign" |
| 138 |
| "benign" |
| 137 |
| "benign" |
| 136 |
| "benign" |
| 135 |
| "benign" |
| 134 |
| "benign" |
| 133 |
| "benign" |
| 132 |
| "benign" |
| 131 |
| "benign" |
| 130 |
| "benign" |
| 129 |
| "benign" |
| 128 |
| "benign" |
| 127 |
| "benign" |
| 126 |
| "benign" |
| 125 |
| "benign" |
| 124 |
| "benign" |
| 123 |
| "benign" |
| 122 |
| "benign" |
| 121 |
| "benign" |
| 120 |
| "benign" |
| 119 |
| "benign" |
| 118 |
| "benign" |
| 117 |
| "benign" |
| 116 |
| "benign" |
| 115 |
| "benign" |
| 114 |
| "benign" |
| 113 |
| "benign" |
| 112 |
| "benign" |
| 111 |
| "benign" |
| 110 |
| "benign" |
| 109 |
| "benign" |
| 108 |
| "benign" |
| 107 |
| "benign" |
| 106 |
| "benign" |
| 105 |
| "benign" |
| 104 |
| "benign" |
| 103 |
| "benign" |
| 102 |
| "benign" |
| 101 |
| "benign" |
| 100 |
| "benign" |
| 99 |
| "benign" |
| 98 |
| "benign" |
| 97 |
| "benign" |
| 96 |
| "benign" |
| 95 |
| "benign" |
| 94 |
| "benign" |
| 93 |
| "benign" |
| 92 |
| "benign" |
| 91 |
| "benign" |
| 90 |
| "benign" |
| 89 |
| "benign" |
| 88 |
| "benign" |
| 87 |
| "benign" |
| 86 |
| "benign" |
| 85 |
| "benign" |
| 84 |
| "benign" |
| 83 |
| "benign" |
| 82 |
| "benign" |
| 81 |
| "benign" |
| 80 |
| "benign" |
| 79 |
| "benign" |
| 78 |
| "benign" |
| 77 |
| "benign" |
| 76 |
| "benign" |
| 75 |
| "benign" |
| 74 |
| "benign" |
| 73 |
| "benign" |
| 72 |
| "benign" |
| 71 |
| "benign" |
| 70 |
| "benign" |
| 69 |
| "benign" |
| 68 |
| "benign" |
| 67 |
| "benign" |
| 66 |
| "benign" |
| 65 |
| "benign" |
| 64 |
| "benign" |
| 63 |
| "benign" |
| 62 |
| "benign" |
| 61 |
| "benign" |
| 60 |
| "benign" |
| 59 |
| "benign" |
| 58 |
| "benign" |
| 57 |
| "benign" |
| 56 |
| "benign" |
| 55 |
| "benign" |
| 54 |
| "benign" |
| 53 |
| "benign" |
| 52 |
| "benign" |
| 51 |
| "benign" |
| 50 |
| "benign" |
| 49 |
| "benign" |
| 48 |
| "malignant" |
| 47 |
| "malignant" |
| 46 |
| "malignant" |
| 45 |
| "malignant" |
| 44 |
| "malignant" |
| 43 |
| "malignant" |
| 42 |
| "malignant" |
| 41 |
| "malignant" |
| 40 |
| "malignant" |
| 39 |
| "malignant" |
| 38 |
| "malignant" |
| 37 |
| "malignant" |
| 36 |
| "malignant" |
| 35 |
| "malignant" |
| 34 |
| "malignant" |
| 33 |
| "malignant" |
| 32 |
| "malignant" |
| 31 |
| "malignant" |
| 30 |
| "malignant" |
| 29 |
| "malignant" |
| 28 |
| "malignant" |
| 27 |
| "malignant" |
| 26 |
| "malignant" |
| 25 |
| "malignant" |
| 24 |
| "malignant" |
| 23 |
| "malignant" |
| 22 |
| "malignant" |
| 21 |
| "malignant" |
| 20 |
| "malignant" |
| 19 |
| "malignant" |
| 18 |
| "malignant" |
| 17 |
| "malignant" |
| 16 |
| "malignant" |
| 15 |
| "malignant" |
| 14 |
| "malignant" |
| 13 |
| "malignant" |
| 12 |
| "malignant" |
| 11 |
| "malignant" |
| 10 |
| "malignant" |
| 9 |
| "malignant" |
| 8 |
| "malignant" |
| 7 |
| "malignant" |
| 6 |
| "malignant" |
| 5 |
| "malignant" |
| 4 |
| "malignant" |
| 3 |
| "malignant" |
| 2 |
| "malignant" |
| 1 |
| "malignant" |
| 0 |
| "malignant" |
Regression¶
In a regression task we want to learn to predict the value(s) of some variable(s) based on previous data. In the commonly used Forest Fires dataset the aim is to predict the area burned by forest fires, in the northeast region of Portugal, by using meteorological and other data. This is a fairly difficult task and while the neural network below doesn't achieve state-of-the-art performance, it's enough to demonstrate how we can analyse relatively simple models in Imandra. In the dataset we have the following variables:
1. X-axis spatial coordinate (within the Montesinho park map)
2. Y-axis spatial coordinate (within the Montesinho park map)
3. Month
4. Day
5. FFMC index (from the FWI system)
6. DMC index (from the FWI system)
7. DC index (from the FWI system)
8. ISI index (from the FWI system)
9. Temperature
10. Relative percentage humidity
11. Wind speed
12. Rainfall
13. Area of forest burnedWe again pre-process the data before learning by first transforming the month and day variables into a numerical value and applying a sine transformation (so that similar times are close in value), as well as removing outliers and applying an approximate logarithmic transformation to the area variable (as recommended in the dataset description). Each variable is scaled to lie between 0 and 1, and those with high correlations and/or low mutual information respect to the target variable are removed. We then split the data into training (80%) and test (20%) sets and use Keras to learn a simple feed-forward neural network with one (6 neuron) hidden layer, ReLU activation functions, and stochastic gradient descent to optimise the mean squared error. After saving our model as a .h5 file we use a short Python script to extract the network into an IML file and reason about it using Imandra.
In [14]:
let relu x = Real.(if x > 0.0 then x else 0.0);;
let linear x = Real.(x)
let layer_0 (x_0, x_1, x_2, x_3, x_4, x_5) = let open Real in
let y_0 = relu @@ (0.20124)*x_0 + (-0.15722)*x_1 + (-0.19063)*x_2 + (-0.54562)*x_3 + (0.03425)*x_4 + (0.50104)*x_5 + -0.02768 in
let y_1 = relu @@ (0.29103)*x_0 + (0.03180)*x_1 + (-0.16336)*x_2 + (0.17919)*x_3 + (0.32971)*x_4 + (-0.43206)*x_5 + -0.02620 in
let y_2 = relu @@ (0.66419)*x_0 + (0.25399)*x_1 + (0.00449)*x_2 + (0.03841)*x_3 + (-0.51482)*x_4 + (0.58299)*x_5 + 0.11858 in
let y_3 = relu @@ (0.47598)*x_0 + (-0.36142)*x_1 + (0.38981)*x_2 + (0.27632)*x_3 + (-0.61231)*x_4 + (-0.03662)*x_5 + -0.02890 in
let y_4 = relu @@ (0.10277)*x_0 + (-0.28841)*x_1 + (0.04637)*x_2 + (0.28808)*x_3 + (0.05957)*x_4 + (-0.22041)*x_5 + 0.18270 in
let y_5 = relu @@ (0.55604)*x_0 + (-0.04015)*x_1 + (0.10557)*x_2 + (0.60757)*x_3 + (-0.32314)*x_4 + (0.47933)*x_5 + -0.24876 in
(y_0, y_1, y_2, y_3, y_4, y_5)
let layer_1 (x_0, x_1, x_2, x_3, x_4, x_5) = let open Real in
let y_0 = linear @@ (0.28248)*x_0 + (-0.25208)*x_1 + (-0.50075)*x_2 + (-0.07092)*x_3 + (-0.43189)*x_4 + (0.60065)*x_5 + 0.47136 in
(y_0)
let nn (x_0, x_1, x_2, x_3, x_4, x_5) = let open Real in
(x_0, x_1, x_2, x_3, x_4, x_5) |> layer_0 |> layer_1
Out[14]:
val relu : real -> real = <fun> val linear : 'a -> 'a = <fun> val layer_0 : real * real * real * real * real * real -> real * real * real * real * real * real = <fun> val layer_1 : real * real * real * real * real * real -> real = <fun> val nn : real * real * real * real * real * real -> real = <fun>
Given the description of the dataset above we can again create some custom input types in Imandra for our model.
In [15]:
type month = Jan | Feb | Mar | Apr | May | Jun| Jul | Aug | Sep | Oct | Nov | Dec
type day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
type nn_input = {
month : month;
day : day;
dmc : real;
temp : real;
rh : real;
rain : real
}
Out[15]:
type month =
Jan
| Feb
| Mar
| Apr
| May
| Jun
| Jul
| Aug
| Sep
| Oct
| Nov
| Dec
type day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
type nn_input = {
month : month;
day : day;
dmc : real;
temp : real;
rh : real;
rain : real;
}
As before, because we pre-processed our data, we'll add in a function applying this transform to each input variable. Equally, we'll need to convert back to hectares for our output variable, again using some minimum and maximum values extracted during our data pre-processing stage. After that we define a full model which combines these pre/post-processing steps and the network above.
In [16]:
let month_2_num = let open Real in function
| Jan -> 0.134
| Feb -> 0.500
| Mar -> 1.000
| Apr -> 1.500
| May -> 1.866
| Jun -> 2.000
| Jul -> 1.866
| Aug -> 1.500
| Sep -> 1.000
| Oct -> 0.500
| Nov -> 0.133
| Dec -> 0.000
let day_2_num = let open Real in function
| Mon -> 0.377
| Tue -> 1.223
| Wed -> 1.901
| Thu -> 1.901
| Fri -> 1.223
| Sat -> 0.377
| Sun -> 0.000
let process_nn_input input = let open Real in
let real_month = month_2_num input.month in
let real_day = day_2_num input.day in
let x_0 = (real_month - 0.0) / (2.0 - 0.0) in
let x_1 = (real_day - 0.0) / (1.901 - 0.0) in
let x_2 = (input.dmc - 1.1) / (291.3 - 1.1) in
let x_3 = (input.temp - 2.2) / (33.3 - 2.2) in
let x_4 = (input.rh - 15.0) / (100.0 - 15.0) in
let x_5 = (input.rain - 0.0) / (6.40 - 0.0) in
(x_0, x_1, x_2, x_3, x_4, x_5)
let process_nn_output y_0 = let open Real in
let y = 4.44323 * y_0 in
if y <= 1.0 then (y - 0.00000) * 1.71828 else
if y <= 2.0 then (y - 0.63212) * 4.67077 else
if y <= 3.0 then (y - 1.49679) * 12.69648 else
if y <= 4.0 then (y - 2.44700) * 34.51261 else
(y - 3.42868) * 93.81501
let nn_model input = input |> process_nn_input |> nn |> process_nn_output
Out[16]:
val month_2_num : month -> real = <fun> val day_2_num : day -> real = <fun> val process_nn_input : nn_input -> real * real * real * real * real * real = <fun> val process_nn_output : real -> real = <fun> val nn_model : nn_input -> real = <fun>
Let's start as in the previous section by running a datum from our dataset through the model. In particular, we'll input x = (Aug, Sat, 231.1, 26.9, 31.0, 0.0) which has an area of y = 4.96 hectares in the data.
In [17]:
let x = {
month = Aug;
day = Sat;
dmc = 231.1;
temp = 26.9;
rh = 31.0;
rain = 0.0
}
let y = nn_model x
Out[17]:
val x : nn_input =
{month = Aug; day = Sat; dmc = 231.1; temp = 26.9; rh = 31.; rain = 0.}
val y : real = 2.1368837387
Our answer is both roughly similar to the recorded datapoint value and also to the value we get from our original Keras model, 2.13683266556. The small disparity here is due to our rounding the weight values in our network to 5 decimal places when we extracted them to IML, though it wasn't necessary to do so. Now we'll use Imandra to generate an example for us with some particular side conditions.
In [18]:
instance (fun x -> nn_model x >. 20.0 && x.temp = 20.0 && x.month = May)
Out[18]:
- : nn_input -> bool = <fun> module CX : sig val x : nn_input end
Instance (after 0 steps, 0.043s):
let x : nn_input =
{month = May; day = Mon;
dmc =
24055123284982228097226992611528380093193919762056180084008433021/22092492331123120841192276133772540657727264346914321684175000;
temp = 20;
rh =
30345807841768722760850615268729933643730512262727593903588137/110462461655615604205961380668862703288636321734571608420875;
rain =
29095799829274662509656643890210163797429819271649922778038604/2761561541390390105149034516721567582215908043364290210521875}
Instance
Loading..
proof attempt
| ground_instances: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| definitions: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| inductions: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| search_time: | 0.043s | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| details: | Expand
|
Expand
start[0.043s] let (_x_0 : real) = 5031/25000 * … +. (-7861/50000) * … +. (-19063/100000) * … +. (-27281/50000) * … +. 137/4000 * … +. 6263/12500 * … +. (-173/6250) in let (_x_1 : real) = 29103/100000 * … +. 159/5000 * … +. (-1021/6250) * … +. 17919/100000 * … +. 32971/100000 * … +. (-21603/50000) * … +. (-131/5000) in let (_x_2 : real) = 66419/100000 * … +. 25399/100000 * … +. 449/100000 * … +. 3841/100000 * … +. (-25741/50000) * … +. 58299/100000 * … +. 5929/50000 in let (_x_3 : real) = 23799/50000 * … +. (-18071/50000) * … +. 38981/100000 * … +. 1727/6250 * … +. (-61231/100000) * … +. (-1831/50000) * … +. (-289/10000) in let (_x_4 : real) = 10277/100000 * … +. (-28841/100000) * … +. 4637/100000 * … +. 3601/12500 * … +. 5957/100000 * … +. (-22041/100000) * … +. 1827/10000 in let (_x_5 : real) = 13901/25000 * … +. (-803/20000) * … +. 10557/100000 * … +. 60757/100000 * … +. (-16157/50000) * … +. 47933/100000 * … +. (-6219/25000) in let (_x_6 : real) = 444323/100000 * (3531/12500 * (if _x_0 > 0 then _x_0 else 0) +. (-3151/12500) * (if _x_1 > 0 then _x_1 else 0) +. (-2003/4000) * (if _x_2 > 0 then _x_2 else 0) +. (-1773/25000) * (if _x_3 > 0 then _x_3 else 0) +. (-43189/100000) * (if _x_4 > 0 then _x_4 else 0) +. 12013/20000 * (if _x_5 > 0 then _x_5 else 0) +. 1473/3125) in ((if _x_6 <= 1 then (_x_6 - 0) * 42957/25000 else if _x_6 <= 2 then (_x_6 - 15803/25000) * 467077/100000 else if _x_6 <= 3 then (_x_6 - 149679/100000) * 79353/6250 else if _x_6 <= 4 then … else …) > 20) && ((( :var_0: ).temp = 20) && (( :var_0: ).month = May))simplify
into: let (_x_0 : month) = ( :var_0: ).month in let (_x_1 : bool) = _x_0 = Mar in let (_x_2 : bool) = _x_0 = Feb in let (_x_3 : bool) = _x_0 = Jan in let (_x_4 : real) = if _x_3 then 67/500 else if _x_2 then 1/2 else if _x_1 then 1 else if _x_0 = Apr then 3/2 else … in let (_x_5 : real) = 5031/50000 * _x_4 in let (_x_6 : day) = ( :var_0: ).day in let (_x_7 : bool) = (_x_6 = Wed) || (_x_6 = Thu) in let (_x_8 : bool) = _x_6 = Tue in let (_x_9 : bool) = _x_6 = Mon in let (_x_10 : real) = if _x_9 then 377/1000 else if _x_8 then 1223/1000 else if _x_7 then 1901/1000 else if _x_6 = Fri then 1223/1000 else … in let (_x_11 : real) = (-7861/95050) * _x_10 in let (_x_12 : real) = ( :var_0: ).dmc in let (_x_13 : real) = (-19063/29020000) * _x_12 in let (_x_14 : real) = ( :var_0: ).temp in let (_x_15 : real) = (-27281/1555000) * _x_14 in let (_x_16 : real) = ( :var_0: ).rh in let (_x_17 : real) = 137/340000 * _x_16 in let (_x_18 : real) = ( :var_0: ).rain in let (_x_19 : real) = 6263/80000 * _x_18 in let (_x_20 : real) = if _x_3 then 67/500 else if _x_2 then 1/2 else if _x_1 then 1 else … in let (_x_21 : real) = if _x_9 then 377/1000 else if _x_8 then 1223/1000 else if _x_7 then 1901/1000 else … in let (_x_22 : real) = (-1021/1813750) * _x_12 in let (_x_23 : real) = 17919/3110000 * _x_14 in let (_x_24 : real) = 32971/8500000 * _x_16 in let (_x_25 : real) = (-21603/320000) * _x_18 in let (_x_26 : real) = if 29103/200000 * _x_4 +. 159/9505 * _x_10 +. _x_22 +. _x_23 +. _x_24 +. _x_25 <= 73983893263/767143700000 then 0 else (-73983893263/767143700000) +. 29103/200000 * _x_20 +. 159/9505 * _x_21 +. _x_22 +. _x_23 +. _x_24 +. _x_25 in let (_x_27 : real) = 66419/200000 * _x_4 in let (_x_28 : real) = 25399/190100 * _x_10 in let (_x_29 : real) = 449/29020000 * _x_12 in let (_x_30 : real) = 3841/3110000 * _x_14 in let (_x_31 : real) = (-25741/4250000) * _x_16 in let (_x_32 : real) = 58299/640000 * _x_18 in let (_x_33 : real) = if _x_27 +. _x_28 +. _x_29 +. _x_30 +. _x_31 +. _x_32 <= (-317131778543/1534287400000) then 0 else 317131778543/1534287400000 +. _x_27 +. _x_28 +. _x_29 +. _x_30 +. _x_31 +. _x_32 in let (_x_34 : real) = 23799/100000 * _x_4 in let (_x_35 : real) = (-18071/95050) * _x_10 in let (_x_36 : real) = 38981/29020000 * _x_12 in let (_x_37 : real) = 1727/194375 * _x_14 in let (_x_38 : real) = (-61231/8500000) * _x_16 in let (_x_39 : real) = (-1831/320000) * _x_18 in let (_x_40 : real) = if _x_34 +. _x_35 +. _x_36 +. _x_37 +. _x_38 +. _x_39 <= (-89188713933/1534287400000) then 0 else 89188713933/1534287400000 +. _x_34 +. _x_35 +. _x_36 +. _x_37 +. _x_38 +. _x_39 in let (_x_41 : real) = 10277/200000 * _x_4 in let (_x_42 : real) = (-28841/190100) * _x_10 in let (_x_43 : real) = 4637/29020000 * _x_12 in let (_x_44 : real) = 3601/388750 * _x_14 in let (_x_45 : real) = 5957/8500000 * _x_16 in let (_x_46 : real) = (-22041/640000) * _x_18 in let (_x_47 : real) = if _x_41 +. _x_42 +. _x_43 +. _x_44 +. _x_45 +. _x_46 <= (-372238333/2454859840) then 0 else 372238333/2454859840 +. _x_41 +. _x_42 +. _x_43 +. _x_44 +. _x_45 +. _x_46 in let (_x_48 : real) = 13901/50000 * _x_4 in let (_x_49 : real) = (-803/38020) * _x_10 in let (_x_50 : real) = 10557/29020000 * _x_12 in let (_x_51 : real) = 60757/3110000 * _x_14 in let (_x_52 : real) = (-16157/4250000) * _x_16 in let (_x_53 : real) = 47933/640000 * _x_18 in let (_x_54 : real) = if _x_48 +. _x_49 +. _x_50 +. _x_51 +. _x_52 +. _x_53 <= 72146699557/306857480000 then 0 else (-72146699557/306857480000) +. _x_48 +. _x_49 +. _x_50 +. _x_51 +. _x_52 +. _x_53 in let (_x_55 : real) = 1568904513/1250000000 * (if _x_5 +. _x_11 +. _x_13 +. _x_15 +. _x_17 +. _x_19 <= (-1716983137/306857480000) then 0 else (1716983137/306857480000 +. _x_5 +. _x_11 +. _x_13 +. _x_15 +. _x_17 +. _x_19)) +. (-1400061773/1250000000) * _x_26 +. (-889978969/400000000) * _x_33 +. (-787784679/2500000000) * _x_40 +. (-19189866047/10000000000) * _x_47 +. 5337652199/2000000000 * _x_54 in let (_x_56 : real) = 5031/50000 * _x_20 in let (_x_57 : real) = (-7861/95050) * _x_21 in let (_x_58 : real) = if _x_56 +. _x_57 +. _x_13 +. _x_15 +. _x_17 +. _x_19 <= (-1716983137/306857480000) then 0 else 1716983137/306857480000 +. _x_56 +. _x_57 +. _x_13 +. _x_15 +. _x_17 +. _x_19 in not ((if _x_55 <= (-341987779/312500000) then 28114831522503/7812500000000 +. 67395431164941/31250000000000 * _x_58 +. (-60142453582761/31250000000000) * _x_26 +. (-38230826571333/10000000000000) * _x_33 +. (-33840866455803/62500000000000) * _x_40 +. (-824339075780979/250000000000000) * _x_47 +. 229289525512443/50000000000000 * _x_54 else if _x_55 <= (-29487779/312500000) then 213430965464483/31250000000000 +. 732799213218501/125000000000000 * _x_58 +. (-653936652747521/125000000000000) * _x_26 +. (-415688706903613/40000000000000) * _x_33 +. (-367956104513283/250000000000000) * _x_40 +. (-8963145063634619/1000000000000000) * _x_47 +. 2493094576152323/200000000000000 * _x_54 else if _x_55 <= 283012221/312500000 then 1852306369389/244140625000 +. 124497279820089/7812500000000 * _x_58 +. (-111099101872869/7812500000000) * _x_26 +. (-70622501127057/2500000000000) * _x_33 +. (-62513077632687/15625000000000) * _x_40 +. (-1522773440427591/62500000000000) * _x_47 +. 423558714947247/12500000000000 * _x_54 else if _x_55 <= 595512221/312500000 then … else …) <= 20) && (_x_14 = 20) && (_x_0 = May)expansions: []
rewrite_steps: forward_chaining: - Sat (Some let x : nn_input = {month = May; day = Mon; dmc = (Q.of_string "24055123284982228097226992611528380093193919762056180084008433021/22092492331123120841192276133772540657727264346914321684175000"); temp = (Q.of_nativeint (20n)); rh = (Q.of_string "30345807841768722760850615268729933643730512262727593903588137/110462461655615604205961380668862703288636321734571608420875"); rain = (Q.of_string "29095799829274662509656643890210163797429819271649922778038604/2761561541390390105149034516721567582215908043364290210521875")} )
Loading..
In [19]:
CX.x
Out[19]:
- : nn_input =
{month = May; day = Mon; dmc = 1088.83700962; temp = 20.; rh = 274.716020148;
rain = 10.5359954479}
Notice how the unspecified input variables are unbounded, just as in our original classification instances. Using the description of each variable in the data (plus some reasonable assumptions about Portugal's climate) we can form the following condition describing valid inputs to the network.
In [20]:
let is_valid_nn input =
0.0 <=. input.dmc && input.dmc <=. 500.0 &&
0.0 <=. input.temp && input.temp <=. 40.0 &&
0.0 <=. input.rh && input.rh <=. 100.0 &&
0.0 <=. input.rain && input.rain <=. 15.0
instance (fun x -> nn_model x >. 20.0 && x.temp = 20.0 && x.month = May && is_valid_nn x)
Out[20]:
val is_valid_nn : nn_input -> bool = <fun> - : nn_input -> bool = <fun> module CX : sig val x : nn_input end
Instance (after 0 steps, 0.090s):
let x : nn_input =
{month = May; day = Sun;
dmc =
10320016944192717928085378625498323/104479107528761825932953783127500;
temp = 20; rh = 100;
rain = 59292603493829172244694194140464/5223955376438091296647689156375}
Instance
Loading..
proof attempt
| ground_instances: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| definitions: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| inductions: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| search_time: | 0.090s | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| details: | Expand
|
Expand
start[0.090s] let (_x_0 : real) = 5031/25000 * … +. (-7861/50000) * … +. (-19063/100000) * … +. (-27281/50000) * … +. 137/4000 * … +. 6263/12500 * … +. (-173/6250) in let (_x_1 : real) = 29103/100000 * … +. 159/5000 * … +. (-1021/6250) * … +. 17919/100000 * … +. 32971/100000 * … +. (-21603/50000) * … +. (-131/5000) in let (_x_2 : real) = 66419/100000 * … +. 25399/100000 * … +. 449/100000 * … +. 3841/100000 * … +. (-25741/50000) * … +. 58299/100000 * … +. 5929/50000 in let (_x_3 : real) = 23799/50000 * … +. (-18071/50000) * … +. 38981/100000 * … +. 1727/6250 * … +. (-61231/100000) * … +. (-1831/50000) * … +. (-289/10000) in let (_x_4 : real) = 10277/100000 * … +. (-28841/100000) * … +. 4637/100000 * … +. 3601/12500 * … +. 5957/100000 * … +. (-22041/100000) * … +. 1827/10000 in let (_x_5 : real) = 13901/25000 * … +. (-803/20000) * … +. 10557/100000 * … +. 60757/100000 * … +. (-16157/50000) * … +. 47933/100000 * … +. (-6219/25000) in let (_x_6 : real) = 444323/100000 * (3531/12500 * (if _x_0 > 0 then _x_0 else 0) +. (-3151/12500) * (if _x_1 > 0 then _x_1 else 0) +. (-2003/4000) * (if _x_2 > 0 then _x_2 else 0) +. (-1773/25000) * (if _x_3 > 0 then _x_3 else 0) +. (-43189/100000) * (if _x_4 > 0 then _x_4 else 0) +. 12013/20000 * (if _x_5 > 0 then _x_5 else 0) +. 1473/3125) in let (_x_7 : real) = ( :var_0: ).temp in let (_x_8 : real) = ( :var_0: ).dmc in let (_x_9 : real) = ( :var_0: ).rh in let (_x_10 : real) = ( :var_0: ).rain in ((if _x_6 <= 1 then (_x_6 - 0) * 42957/25000 else if _x_6 <= 2 then (_x_6 - 15803/25000) * 467077/100000 else if _x_6 <= 3 then (_x_6 - 149679/100000) * 79353/6250 else if _x_6 <= 4 then … else …) > 20) && ((_x_7 = 20) && ((( :var_0: ).month = May) && ((0 <= _x_8) && ((_x_8 <= 500) && ((0 <= _x_7) && ((_x_7 <= 40) && ((0 <= _x_9) && ((_x_9 <= 100) && ((0 <= _x_10) && (_x_10 <= 15))))))))))simplify
into: let (_x_0 : month) = ( :var_0: ).month in let (_x_1 : real) = if _x_0 = Jan then 67/500 else if _x_0 = Feb then 1/2 else if _x_0 = Mar then 1 else if _x_0 = Apr then 3/2 else … in let (_x_2 : real) = 5031/50000 * _x_1 in let (_x_3 : day) = ( :var_0: ).day in let (_x_4 : real) = if _x_3 = Mon then 377/1000 else if _x_3 = Tue then 1223/1000 else if (_x_3 = Wed) || (_x_3 = Thu) then 1901/1000 else if _x_3 = Fri then 1223/1000 else … in let (_x_5 : real) = (-7861/95050) * _x_4 in let (_x_6 : real) = ( :var_0: ).dmc in let (_x_7 : real) = (-19063/29020000) * _x_6 in let (_x_8 : real) = ( :var_0: ).temp in let (_x_9 : real) = (-27281/1555000) * _x_8 in let (_x_10 : real) = ( :var_0: ).rh in let (_x_11 : real) = 137/340000 * _x_10 in let (_x_12 : real) = ( :var_0: ).rain in let (_x_13 : real) = 6263/80000 * _x_12 in let (_x_14 : real) = if _x_2 +. _x_5 +. _x_7 +. _x_9 +. _x_11 +. _x_13 <= (-1716983137/306857480000) then 0 else 1716983137/306857480000 +. _x_2 +. _x_5 +. _x_7 +. _x_9 +. _x_11 +. _x_13 in let (_x_15 : real) = 29103/200000 * _x_1 in let (_x_16 : real) = 159/9505 * _x_4 in let (_x_17 : real) = (-1021/1813750) * _x_6 in let (_x_18 : real) = 17919/3110000 * _x_8 in let (_x_19 : real) = 32971/8500000 * _x_10 in let (_x_20 : real) = (-21603/320000) * _x_12 in let (_x_21 : real) = if _x_15 +. _x_16 +. _x_17 +. _x_18 +. _x_19 +. _x_20 <= 73983893263/767143700000 then 0 else (-73983893263/767143700000) +. _x_15 +. _x_16 +. _x_17 +. _x_18 +. _x_19 +. _x_20 in let (_x_22 : real) = 66419/200000 * _x_1 in let (_x_23 : real) = 25399/190100 * _x_4 in let (_x_24 : real) = 449/29020000 * _x_6 in let (_x_25 : real) = 3841/3110000 * _x_8 in let (_x_26 : real) = (-25741/4250000) * _x_10 in let (_x_27 : real) = 58299/640000 * _x_12 in let (_x_28 : real) = if _x_22 +. _x_23 +. _x_24 +. _x_25 +. _x_26 +. _x_27 <= (-317131778543/1534287400000) then 0 else 317131778543/1534287400000 +. _x_22 +. _x_23 +. _x_24 +. _x_25 +. _x_26 +. _x_27 in let (_x_29 : real) = 23799/100000 * _x_1 in let (_x_30 : real) = (-18071/95050) * _x_4 in let (_x_31 : real) = 38981/29020000 * _x_6 in let (_x_32 : real) = 1727/194375 * _x_8 in let (_x_33 : real) = (-61231/8500000) * _x_10 in let (_x_34 : real) = (-1831/320000) * _x_12 in let (_x_35 : real) = if _x_29 +. _x_30 +. _x_31 +. _x_32 +. _x_33 +. _x_34 <= (-89188713933/1534287400000) then 0 else 89188713933/1534287400000 +. _x_29 +. _x_30 +. _x_31 +. _x_32 +. _x_33 +. _x_34 in let (_x_36 : real) = 10277/200000 * _x_1 in let (_x_37 : real) = (-28841/190100) * _x_4 in let (_x_38 : real) = 4637/29020000 * _x_6 in let (_x_39 : real) = 3601/388750 * _x_8 in let (_x_40 : real) = 5957/8500000 * _x_10 in let (_x_41 : real) = (-22041/640000) * _x_12 in let (_x_42 : real) = if _x_36 +. _x_37 +. _x_38 +. _x_39 +. _x_40 +. _x_41 <= (-372238333/2454859840) then 0 else 372238333/2454859840 +. _x_36 +. _x_37 +. _x_38 +. _x_39 +. _x_40 +. _x_41 in let (_x_43 : real) = 13901/50000 * _x_1 in let (_x_44 : real) = (-803/38020) * _x_4 in let (_x_45 : real) = 10557/29020000 * _x_6 in let (_x_46 : real) = 60757/3110000 * _x_8 in let (_x_47 : real) = (-16157/4250000) * _x_10 in let (_x_48 : real) = 47933/640000 * _x_12 in let (_x_49 : real) = if _x_43 +. _x_44 +. _x_45 +. _x_46 +. _x_47 +. _x_48 <= 72146699557/306857480000 then 0 else (-72146699557/306857480000) +. _x_43 +. _x_44 +. _x_45 +. _x_46 +. _x_47 +. _x_48 in let (_x_50 : real) = 1568904513/1250000000 * _x_14 +. (-1400061773/1250000000) * _x_21 +. (-889978969/400000000) * _x_28 +. (-787784679/2500000000) * _x_35 +. (-19189866047/10000000000) * _x_42 +. 5337652199/2000000000 * _x_49 in not ((if _x_50 <= (-341987779/312500000) then 28114831522503/7812500000000 +. 67395431164941/31250000000000 * _x_14 +. (-60142453582761/31250000000000) * _x_21 +. (-38230826571333/10000000000000) * _x_28 +. (-33840866455803/62500000000000) * _x_35 +. (-824339075780979/250000000000000) * _x_42 +. 229289525512443/50000000000000 * _x_49 else if _x_50 <= (-29487779/312500000) then 213430965464483/31250000000000 +. 732799213218501/125000000000000 * _x_14 +. (-653936652747521/125000000000000) * _x_21 +. (-415688706903613/40000000000000) * _x_28 +. (-367956104513283/250000000000000) * _x_35 +. (-8963145063634619/1000000000000000) * _x_42 +. 2493094576152323/200000000000000 * _x_49 else if _x_50 <= 283012221/312500000 then 1852306369389/244140625000 +. 124497279820089/7812500000000 * _x_14 +. (-111099101872869/7812500000000) * _x_21 +. (-70622501127057/2500000000000) * _x_28 +. (-62513077632687/15625000000000) * _x_35 +. (-1522773440427591/62500000000000) * _x_42 +. 423558714947247/12500000000000 * _x_49 else if _x_50 <= 595512221/312500000 then … else …) <= 20) && (_x_8 = 20) && (_x_0 = May) && (0 <= _x_6) && (_x_6 <= 500) && (0 <= _x_8) && (_x_8 <= 40) && (0 <= _x_10) && (_x_10 <= 100) && (0 <= _x_12) && (_x_12 <= 15)expansions: []
rewrite_steps: forward_chaining: - Sat (Some let x : nn_input = {month = May; day = Sun; dmc = (Q.of_string "10320016944192717928085378625498323/104479107528761825932953783127500"); temp = (Q.of_nativeint (20n)); rh = (Q.of_nativeint (100n)); rain = (Q.of_string "59292603493829172244694194140464/5223955376438091296647689156375")} )
Loading..
In [21]:
CX.x;;
nn_model CX.x
Out[21]:
- : nn_input =
{month = May; day = Sun; dmc = 98.7758910685; temp = 20.; rh = 100.;
rain = 11.3501359068}
- : real = 20.0272890315
These constraints mean it is slightly harder for Imandra to find a particular instance satisfying our original demand, but nonetheless it's possible. Now let's try something a bit more interesting. First of all let's check for one desirable property of the model, namely that it never outputs a negative area as a prediction.
In [22]:
verify (fun x -> is_valid_nn x ==> nn_model x >=. 0.0)
Out[22]:
- : nn_input -> bool = <fun>
Proved
proof
| ground_instances: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| definitions: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| inductions: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| search_time: | 0.532s | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| details: | Expand
|
Expand
start[0.532s] let (_x_0 : real) = ( :var_0: ).dmc in let (_x_1 : real) = ( :var_0: ).temp in let (_x_2 : real) = ( :var_0: ).rh in let (_x_3 : real) = ( :var_0: ).rain in let (_x_4 : real) = 5031/25000 * … +. (-7861/50000) * … +. (-19063/100000) * … +. (-27281/50000) * … +. 137/4000 * … +. 6263/12500 * … +. (-173/6250) in let (_x_5 : real) = 29103/100000 * … +. 159/5000 * … +. (-1021/6250) * … +. 17919/100000 * … +. 32971/100000 * … +. (-21603/50000) * … +. (-131/5000) in let (_x_6 : real) = 66419/100000 * … +. 25399/100000 * … +. 449/100000 * … +. 3841/100000 * … +. (-25741/50000) * … +. 58299/100000 * … +. 5929/50000 in let (_x_7 : real) = 23799/50000 * … +. (-18071/50000) * … +. 38981/100000 * … +. 1727/6250 * … +. (-61231/100000) * … +. (-1831/50000) * … +. (-289/10000) in let (_x_8 : real) = 10277/100000 * … +. (-28841/100000) * … +. 4637/100000 * … +. 3601/12500 * … +. 5957/100000 * … +. (-22041/100000) * … +. 1827/10000 in let (_x_9 : real) = 13901/25000 * … +. (-803/20000) * … +. 10557/100000 * … +. 60757/100000 * … +. (-16157/50000) * … +. 47933/100000 * … +. (-6219/25000) in let (_x_10 : real) = 444323/100000 * (3531/12500 * (if _x_4 > 0 then _x_4 else 0) +. (-3151/12500) * (if _x_5 > 0 then _x_5 else 0) +. (-2003/4000) * (if _x_6 > 0 then _x_6 else 0) +. (-1773/25000) * (if _x_7 > 0 then _x_7 else 0) +. (-43189/100000) * (if _x_8 > 0 then _x_8 else 0) +. 12013/20000 * (if _x_9 > 0 then _x_9 else 0) +. 1473/3125) in (0 <= _x_0) && ((_x_0 <= 500) && ((0 <= _x_1) && ((_x_1 <= 40) && ((0 <= _x_2) && ((_x_2 <= 100) && ((0 <= _x_3) && (_x_3 <= 15))))))) ==> (if _x_10 <= 1 then (_x_10 - 0) * 42957/25000 else if _x_10 <= 2 then (_x_10 - 15803/25000) * 467077/100000 else if _x_10 <= 3 then (_x_10 - 149679/100000) * 79353/6250 else if _x_10 <= 4 then … else …) >= 0simplify
into: let (_x_0 : real) = ( :var_0: ).dmc in let (_x_1 : real) = ( :var_0: ).temp in let (_x_2 : real) = ( :var_0: ).rh in let (_x_3 : real) = ( :var_0: ).rain in let (_x_4 : month) = ( :var_0: ).month in let (_x_5 : real) = if _x_4 = Jan then 67/500 else if _x_4 = Feb then 1/2 else if _x_4 = Mar then 1 else if _x_4 = Apr then 3/2 else … in let (_x_6 : real) = 5031/50000 * _x_5 in let (_x_7 : day) = ( :var_0: ).day in let (_x_8 : real) = if _x_7 = Mon then 377/1000 else if _x_7 = Tue then 1223/1000 else if (_x_7 = Wed) || (_x_7 = Thu) then 1901/1000 else if _x_7 = Fri then 1223/1000 else … in let (_x_9 : real) = (-7861/95050) * _x_8 in let (_x_10 : real) = (-19063/29020000) * _x_0 in let (_x_11 : real) = (-27281/1555000) * _x_1 in let (_x_12 : real) = 137/340000 * _x_2 in let (_x_13 : real) = 6263/80000 * _x_3 in let (_x_14 : real) = if _x_6 +. _x_9 +. _x_10 +. _x_11 +. _x_12 +. _x_13 <= (-1716983137/306857480000) then 0 else 1716983137/306857480000 +. _x_6 +. _x_9 +. _x_10 +. _x_11 +. _x_12 +. _x_13 in let (_x_15 : real) = 29103/200000 * _x_5 in let (_x_16 : real) = 159/9505 * _x_8 in let (_x_17 : real) = (-1021/1813750) * _x_0 in let (_x_18 : real) = 17919/3110000 * _x_1 in let (_x_19 : real) = 32971/8500000 * _x_2 in let (_x_20 : real) = (-21603/320000) * _x_3 in let (_x_21 : real) = if _x_15 +. _x_16 +. _x_17 +. _x_18 +. _x_19 +. _x_20 <= 73983893263/767143700000 then 0 else (-73983893263/767143700000) +. _x_15 +. _x_16 +. _x_17 +. _x_18 +. _x_19 +. _x_20 in let (_x_22 : real) = 66419/200000 * _x_5 in let (_x_23 : real) = 25399/190100 * _x_8 in let (_x_24 : real) = 449/29020000 * _x_0 in let (_x_25 : real) = 3841/3110000 * _x_1 in let (_x_26 : real) = (-25741/4250000) * _x_2 in let (_x_27 : real) = 58299/640000 * _x_3 in let (_x_28 : real) = if _x_22 +. _x_23 +. _x_24 +. _x_25 +. _x_26 +. _x_27 <= (-317131778543/1534287400000) then 0 else 317131778543/1534287400000 +. _x_22 +. _x_23 +. _x_24 +. _x_25 +. _x_26 +. _x_27 in let (_x_29 : real) = 23799/100000 * _x_5 in let (_x_30 : real) = (-18071/95050) * _x_8 in let (_x_31 : real) = 38981/29020000 * _x_0 in let (_x_32 : real) = 1727/194375 * _x_1 in let (_x_33 : real) = (-61231/8500000) * _x_2 in let (_x_34 : real) = (-1831/320000) * _x_3 in let (_x_35 : real) = if _x_29 +. _x_30 +. _x_31 +. _x_32 +. _x_33 +. _x_34 <= (-89188713933/1534287400000) then 0 else 89188713933/1534287400000 +. _x_29 +. _x_30 +. _x_31 +. _x_32 +. _x_33 +. _x_34 in let (_x_36 : real) = 10277/200000 * _x_5 in let (_x_37 : real) = (-28841/190100) * _x_8 in let (_x_38 : real) = 4637/29020000 * _x_0 in let (_x_39 : real) = 3601/388750 * _x_1 in let (_x_40 : real) = 5957/8500000 * _x_2 in let (_x_41 : real) = (-22041/640000) * _x_3 in let (_x_42 : real) = if _x_36 +. _x_37 +. _x_38 +. _x_39 +. _x_40 +. _x_41 <= (-372238333/2454859840) then 0 else 372238333/2454859840 +. _x_36 +. _x_37 +. _x_38 +. _x_39 +. _x_40 +. _x_41 in let (_x_43 : real) = 13901/50000 * _x_5 in let (_x_44 : real) = (-803/38020) * _x_8 in let (_x_45 : real) = 10557/29020000 * _x_0 in let (_x_46 : real) = 60757/3110000 * _x_1 in let (_x_47 : real) = (-16157/4250000) * _x_2 in let (_x_48 : real) = 47933/640000 * _x_3 in let (_x_49 : real) = if _x_43 +. _x_44 +. _x_45 +. _x_46 +. _x_47 +. _x_48 <= 72146699557/306857480000 then 0 else (-72146699557/306857480000) +. _x_43 +. _x_44 +. _x_45 +. _x_46 +. _x_47 +. _x_48 in let (_x_50 : real) = 1568904513/1250000000 * _x_14 +. (-1400061773/1250000000) * _x_21 +. (-889978969/400000000) * _x_28 +. (-787784679/2500000000) * _x_35 +. (-19189866047/10000000000) * _x_42 +. 5337652199/2000000000 * _x_49 in not ((0 <= _x_0) && (_x_0 <= 500) && (0 <= _x_1) && (_x_1 <= 40) && (0 <= _x_2) && (_x_2 <= 100) && (0 <= _x_3) && (_x_3 <= 15)) || ((if _x_50 <= (-341987779/312500000) then 28114831522503/7812500000000 +. 67395431164941/31250000000000 * _x_14 +. (-60142453582761/31250000000000) * _x_21 +. (-38230826571333/10000000000000) * _x_28 +. (-33840866455803/62500000000000) * _x_35 +. (-824339075780979/250000000000000) * _x_42 +. 229289525512443/50000000000000 * _x_49 else if _x_50 <= (-29487779/312500000) then 213430965464483/31250000000000 +. 732799213218501/125000000000000 * _x_14 +. (-653936652747521/125000000000000) * _x_21 +. (-415688706903613/40000000000000) * _x_28 +. (-367956104513283/250000000000000) * _x_35 +. (-8963145063634619/1000000000000000) * _x_42 +. 2493094576152323/200000000000000 * _x_49 else if _x_50 <= 283012221/312500000 then 1852306369389/244140625000 +. 124497279820089/7812500000000 * _x_14 +. (-111099101872869/7812500000000) * _x_21 +. (-70622501127057/2500000000000) * _x_28 +. (-62513077632687/15625000000000) * _x_35 +. (-1522773440427591/62500000000000) * _x_42 +. 423558714947247/12500000000000 * _x_49 else if _x_50 <= 595512221/312500000 then … else …) >= 0)expansions: []
rewrite_steps: forward_chaining: - Unsat
Loading..
Loading..
Finally, we'll try something slightly more ambitious and test a hypothesis. All other things remaining equal, we would expect that the higher the temperature, the larger the area of forest that would be burned. Due to the imperfections in our model (because of limited data, stochasticity in training, the complicated patterns present in natural physical phenomena, and so on) this assertion is in fact easily falsifiable by Imandra.
In [23]:
verify (fun a b ->
is_valid_nn a &&
is_valid_nn b &&
a.month = b.month &&
a.day = b.day &&
a.dmc = b.dmc &&
a.rh = b.rh &&
a.rain = b.rain &&
a.temp >=. b.temp ==>
nn_model a >=. nn_model b)
Out[23]:
- : nn_input -> nn_input -> bool = <fun> module CX : sig val a : nn_input val b : nn_input end
Counterexample (after 0 steps, 0.815s):
let a : nn_input =
{month = Jan; day = Tue;
dmc =
24071693176255305204995774355157911171745916535164711/130812696337961989065667223239362401085882856200000;
temp =
28740379267551135462365274169038593/80313472375754846344478853462320000;
rh = 1749390517427770976867/145708429369777734000;
rain =
10830863650220655949604684927151011046139629487337/4087896760561312158302100726230075033933839256250}
let b : nn_input =
{month = Jan; day = Tue;
dmc =
24071693176255305204995774355157911171745916535164711/130812696337961989065667223239362401085882856200000;
temp = 0; rh = 1749390517427770976867/145708429369777734000;
rain =
10830863650220655949604684927151011046139629487337/4087896760561312158302100726230075033933839256250}
Refuted
Loading..
proof attempt
| ground_instances: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| definitions: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| inductions: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| search_time: | 0.815s | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| details: | Expand
|
Expand
start[0.815s] let (_x_0 : real) = ( :var_0: ).dmc in let (_x_1 : real) = ( :var_0: ).temp in let (_x_2 : real) = ( :var_0: ).rh in let (_x_3 : real) = ( :var_0: ).rain in let (_x_4 : real) = ( :var_1: ).dmc in let (_x_5 : real) = ( :var_1: ).temp in let (_x_6 : real) = ( :var_1: ).rh in let (_x_7 : real) = ( :var_1: ).rain in let (_x_8 : real) = 5031/25000 * … +. (-7861/50000) * … +. (-19063/100000) * … +. (-27281/50000) * … +. 137/4000 * … +. 6263/12500 * … +. (-173/6250) in let (_x_9 : real) = 29103/100000 * … +. 159/5000 * … +. (-1021/6250) * … +. 17919/100000 * … +. 32971/100000 * … +. (-21603/50000) * … +. (-131/5000) in let (_x_10 : real) = 66419/100000 * … +. 25399/100000 * … +. 449/100000 * … +. 3841/100000 * … +. (-25741/50000) * … +. 58299/100000 * … +. 5929/50000 in let (_x_11 : real) = 23799/50000 * … +. (-18071/50000) * … +. 38981/100000 * … +. 1727/6250 * … +. (-61231/100000) * … +. (-1831/50000) * … +. (-289/10000) in let (_x_12 : real) = 10277/100000 * … +. (-28841/100000) * … +. 4637/100000 * … +. 3601/12500 * … +. 5957/100000 * … +. (-22041/100000) * … +. 1827/10000 in let (_x_13 : real) = 13901/25000 * … +. (-803/20000) * … +. 10557/100000 * … +. 60757/100000 * … +. (-16157/50000) * … +. 47933/100000 * … +. (-6219/25000) in let (_x_14 : real) = 444323/100000 * (3531/12500 * (if _x_8 > 0 then _x_8 else 0) +. (-3151/12500) * (if _x_9 > 0 then _x_9 else 0) +. (-2003/4000) * (if _x_10 > 0 then _x_10 else 0) +. (-1773/25000) * (if _x_11 > 0 then _x_11 else 0) +. (-43189/100000) * (if _x_12 > 0 then _x_12 else 0) +. 12013/20000 * (if _x_13 > 0 then _x_13 else 0) +. 1473/3125) in let (_x_15 : real) = if _x_14 <= 1 then (_x_14 - 0) * 42957/25000 else if _x_14 <= 2 then (_x_14 - 15803/25000) * 467077/100000 else if _x_14 <= 3 then (_x_14 - 149679/100000) * 79353/6250 else if _x_14 <= 4 then … else … in (0 <= _x_0) && ((_x_0 <= 500) && ((0 <= _x_1) && ((_x_1 <= 40) && ((0 <= _x_2) && ((_x_2 <= 100) && ((0 <= _x_3) && (_x_3 <= 15))))))) && ((0 <= _x_4) && ((_x_4 <= 500) && ((0 <= _x_5) && ((_x_5 <= 40) && ((0 <= _x_6) && ((_x_6 <= 100) && ((0 <= _x_7) && (_x_7 <= 15))))))) && ((( :var_0: ).month = ( :var_1: ).month) && ((( :var_0: ).day = ( :var_1: ).day) && ((_x_0 = _x_4) && ((_x_2 = _x_6) && ((_x_3 = _x_7) && (_x_1 >= _x_5))))))) ==> _x_15 >= _x_15simplify
into: let (_x_0 : real) = ( :var_0: ).dmc in let (_x_1 : real) = ( :var_0: ).temp in let (_x_2 : real) = ( :var_0: ).rh in let (_x_3 : real) = ( :var_0: ).rain in let (_x_4 : real) = ( :var_1: ).dmc in let (_x_5 : real) = ( :var_1: ).temp in let (_x_6 : real) = ( :var_1: ).rh in let (_x_7 : real) = ( :var_1: ).rain in let (_x_8 : month) = ( :var_0: ).month in let (_x_9 : month) = ( :var_1: ).month in let (_x_10 : day) = ( :var_0: ).day in let (_x_11 : day) = ( :var_1: ).day in let (_x_12 : real) = if _x_8 = Jan then 67/500 else if _x_8 = Feb then 1/2 else if _x_8 = Mar then 1 else if _x_8 = Apr then 3/2 else … in let (_x_13 : real) = 5031/50000 * _x_12 in let (_x_14 : real) = if _x_10 = Mon then 377/1000 else if _x_10 = Tue then 1223/1000 else if (_x_10 = Wed) || (_x_10 = Thu) then 1901/1000 else if _x_10 = Fri then 1223/1000 else … in let (_x_15 : real) = (-7861/95050) * _x_14 in let (_x_16 : real) = (-19063/29020000) * _x_0 in let (_x_17 : real) = (-27281/1555000) * _x_1 in let (_x_18 : real) = 137/340000 * _x_2 in let (_x_19 : real) = 6263/80000 * _x_3 in let (_x_20 : real) = if _x_13 +. _x_15 +. _x_16 +. _x_17 +. _x_18 +. _x_19 <= (-1716983137/306857480000) then 0 else 1716983137/306857480000 +. _x_13 +. _x_15 +. _x_16 +. _x_17 +. _x_18 +. _x_19 in let (_x_21 : real) = 29103/200000 * _x_12 in let (_x_22 : real) = 159/9505 * _x_14 in let (_x_23 : real) = (-1021/1813750) * _x_0 in let (_x_24 : real) = 17919/3110000 * _x_1 in let (_x_25 : real) = 32971/8500000 * _x_2 in let (_x_26 : real) = (-21603/320000) * _x_3 in let (_x_27 : real) = if _x_21 +. _x_22 +. _x_23 +. _x_24 +. _x_25 +. _x_26 <= 73983893263/767143700000 then 0 else (-73983893263/767143700000) +. _x_21 +. _x_22 +. _x_23 +. _x_24 +. _x_25 +. _x_26 in let (_x_28 : real) = 66419/200000 * _x_12 in let (_x_29 : real) = 25399/190100 * _x_14 in let (_x_30 : real) = 449/29020000 * _x_0 in let (_x_31 : real) = 3841/3110000 * _x_1 in let (_x_32 : real) = (-25741/4250000) * _x_2 in let (_x_33 : real) = 58299/640000 * _x_3 in let (_x_34 : real) = if _x_28 +. _x_29 +. _x_30 +. _x_31 +. _x_32 +. _x_33 <= (-317131778543/1534287400000) then 0 else 317131778543/1534287400000 +. _x_28 +. _x_29 +. _x_30 +. _x_31 +. _x_32 +. _x_33 in let (_x_35 : real) = 23799/100000 * _x_12 in let (_x_36 : real) = (-18071/95050) * _x_14 in let (_x_37 : real) = 38981/29020000 * _x_0 in let (_x_38 : real) = 1727/194375 * _x_1 in let (_x_39 : real) = (-61231/8500000) * _x_2 in let (_x_40 : real) = (-1831/320000) * _x_3 in let (_x_41 : real) = if _x_35 +. _x_36 +. _x_37 +. _x_38 +. _x_39 +. _x_40 <= (-89188713933/1534287400000) then 0 else 89188713933/1534287400000 +. _x_35 +. _x_36 +. _x_37 +. _x_38 +. _x_39 +. _x_40 in let (_x_42 : real) = 10277/200000 * _x_12 in let (_x_43 : real) = (-28841/190100) * _x_14 in let (_x_44 : real) = 4637/29020000 * _x_0 in let (_x_45 : real) = 3601/388750 * _x_1 in let (_x_46 : real) = 5957/8500000 * _x_2 in let (_x_47 : real) = (-22041/640000) * _x_3 in let (_x_48 : real) = if _x_42 +. _x_43 +. _x_44 +. _x_45 +. _x_46 +. _x_47 <= (-372238333/2454859840) then 0 else 372238333/2454859840 +. _x_42 +. _x_43 +. _x_44 +. _x_45 +. _x_46 +. _x_47 in let (_x_49 : real) = 13901/50000 * _x_12 in let (_x_50 : real) = (-803/38020) * _x_14 in let (_x_51 : real) = 10557/29020000 * _x_0 in let (_x_52 : real) = 60757/3110000 * _x_1 in let (_x_53 : real) = (-16157/4250000) * _x_2 in let (_x_54 : real) = 47933/640000 * _x_3 in let (_x_55 : real) = if _x_49 +. _x_50 +. _x_51 +. _x_52 +. _x_53 +. _x_54 <= 72146699557/306857480000 then 0 else (-72146699557/306857480000) +. _x_49 +. _x_50 +. _x_51 +. _x_52 +. _x_53 +. _x_54 in let (_x_56 : real) = 1568904513/1250000000 * _x_20 +. (-1400061773/1250000000) * _x_27 +. (-889978969/400000000) * _x_34 +. (-787784679/2500000000) * _x_41 +. (-19189866047/10000000000) * _x_48 +. 5337652199/2000000000 * _x_55 in let (_x_57 : bool) = _x_9 = Mar in let (_x_58 : bool) = _x_9 = Feb in let (_x_59 : bool) = _x_9 = Jan in let (_x_60 : real) = if _x_59 then 67/500 else if _x_58 then 1/2 else if _x_57 then 1 else if _x_9 = Apr then 3/2 else … in let (_x_61 : real) = 5031/50000 * _x_60 in let (_x_62 : bool) = (_x_11 = Wed) || (_x_11 = Thu) in let (_x_63 : bool) = _x_11 = Tue in let (_x_64 : bool) = _x_11 = Mon in let (_x_65 : real) = if _x_64 then 377/1000 else if _x_63 then 1223/1000 else if _x_62 then 1901/1000 else if _x_11 = Fri then 1223/1000 else … in let (_x_66 : real) = (-7861/95050) * _x_65 in let (_x_67 : real) = (-19063/29020000) * _x_4 in let (_x_68 : real) = (-27281/1555000) * _x_5 in let (_x_69 : real) = 137/340000 * _x_6 in let (_x_70 : real) = 6263/80000 * _x_7 in let (_x_71 : real) = 29103/200000 * _x_60 in let (_x_72 : real) = 159/9505 * _x_65 in let (_x_73 : real) = (-1021/1813750) * _x_4 in let (_x_74 : real) = 17919/3110000 * _x_5 in let (_x_75 : real) = 32971/8500000 * _x_6 in let (_x_76 : real) = (-21603/320000) * _x_7 in let (_x_77 : real) = if _x_71 +. _x_72 +. _x_73 +. _x_74 +. _x_75 +. _x_76 <= 73983893263/767143700000 then 0 else (-73983893263/767143700000) +. _x_71 +. _x_72 +. _x_73 +. _x_74 +. _x_75 +. _x_76 in let (_x_78 : real) = 66419/200000 * _x_60 in let (_x_79 : real) = 25399/190100 * _x_65 in let (_x_80 : real) = 449/29020000 * _x_4 in let (_x_81 : real) = 3841/3110000 * _x_5 in let (_x_82 : real) = (-25741/4250000) * _x_6 in let (_x_83 : real) = 58299/640000 * _x_7 in let (_x_84 : real) = if _x_78 +. _x_79 +. _x_80 +. _x_81 +. _x_82 +. _x_83 <= (-317131778543/1534287400000) then 0 else 317131778543/1534287400000 +. _x_78 +. _x_79 +. _x_80 +. _x_81 +. _x_82 +. _x_83 in let (_x_85 : real) = 23799/100000 * _x_60 in let (_x_86 : real) = (-18071/95050) * _x_65 in let (_x_87 : real) = 38981/29020000 * _x_4 in let (_x_88 : real) = 1727/194375 * _x_5 in let (_x_89 : real) = (-61231/8500000) * _x_6 in let (_x_90 : real) = (-1831/320000) * _x_7 in let (_x_91 : real) = if _x_85 +. _x_86 +. _x_87 +. _x_88 +. _x_89 +. _x_90 <= (-89188713933/1534287400000) then 0 else 89188713933/1534287400000 +. _x_85 +. _x_86 +. _x_87 +. _x_88 +. _x_89 +. _x_90 in let (_x_92 : real) = 10277/200000 * _x_60 in let (_x_93 : real) = (-28841/190100) * _x_65 in let (_x_94 : real) = 4637/29020000 * _x_4 in let (_x_95 : real) = 3601/388750 * _x_5 in let (_x_96 : real) = 5957/8500000 * _x_6 in let (_x_97 : real) = (-22041/640000) * _x_7 in let (_x_98 : real) = if _x_92 +. _x_93 +. _x_94 +. _x_95 +. _x_96 +. _x_97 <= (-372238333/2454859840) then 0 else 372238333/2454859840 +. _x_92 +. _x_93 +. _x_94 +. _x_95 +. _x_96 +. _x_97 in let (_x_99 : real) = 13901/50000 * _x_60 in let (_x_100 : real) = (-803/38020) * _x_65 in let (_x_101 : real) = 10557/29020000 * _x_4 in let (_x_102 : real) = 60757/3110000 * _x_5 in let (_x_103 : real) = (-16157/4250000) * _x_6 in let (_x_104 : real) = 47933/640000 * _x_7 in let (_x_105 : real) = if _x_99 +. _x_100 +. _x_101 +. _x_102 +. _x_103 +. _x_104 <= 72146699557/306857480000 then 0 else (-72146699557/306857480000) +. _x_99 +. _x_100 +. _x_101 +. _x_102 +. _x_103 +. _x_104 in let (_x_106 : real) = 1568904513/1250000000 * (if _x_61 +. _x_66 +. _x_67 +. _x_68 +. _x_69 +. _x_70 <= (-1716983137/306857480000) then 0 else (1716983137/306857480000 +. _x_61 +. _x_66 +. _x_67 +. _x_68 +. _x_69 +. _x_70)) +. (-1400061773/1250000000) * _x_77 +. (-889978969/400000000) * _x_84 +. (-787784679/2500000000) * _x_91 +. (-19189866047/10000000000) * _x_98 +. 5337652199/2000000000 * _x_105 in let (_x_107 : real) = 5031/50000 * (if _x_59 then 67/500 else if _x_58 then 1/2 else if _x_57 then 1 else …) in let (_x_108 : real) = (-7861/95050) * (if _x_64 then 377/1000 else if _x_63 then 1223/1000 else if _x_62 then 1901/1000 else …) in let (_x_109 : real) = if _x_107 +. _x_108 +. _x_67 +. _x_68 +. _x_69 +. _x_70 <= (-1716983137/306857480000) then 0 else 1716983137/306857480000 +. _x_107 +. _x_108 +. _x_67 +. _x_68 +. _x_69 +. _x_70 in not ((0 <= _x_0) && (_x_0 <= 500) && (0 <= _x_1) && (_x_1 <= 40) && (0 <= _x_2) && (_x_2 <= 100) && (0 <= _x_3) && (_x_3 <= 15) && (0 <= _x_4) && (_x_4 <= 500) && (0 <= _x_5) && (_x_5 <= 40) && (0 <= _x_6) && (_x_6 <= 100) && (0 <= _x_7) && (_x_7 <= 15) && (_x_8 = _x_9) && (_x_10 = _x_11) && (_x_0 = _x_4) && (_x_2 = _x_6) && (_x_3 = _x_7) && (_x_1 >= _x_5)) || ((if _x_56 <= (-341987779/312500000) then 28114831522503/7812500000000 +. 67395431164941/31250000000000 * _x_20 +. (-60142453582761/31250000000000) * _x_27 +. (-38230826571333/10000000000000) * _x_34 +. (-33840866455803/62500000000000) * _x_41 +. (-824339075780979/250000000000000) * _x_48 +. 229289525512443/50000000000000 * _x_55 else if _x_56 <= (-29487779/312500000) then 213430965464483/31250000000000 +. 732799213218501/125000000000000 * _x_20 +. (-653936652747521/125000000000000) * _x_27 +. (-415688706903613/40000000000000) * _x_34 +. (-367956104513283/250000000000000) * _x_41 +. (-8963145063634619/1000000000000000) * _x_48 +. 2493094576152323/200000000000000 * _x_55 else if _x_56 <= 283012221/312500000 then 1852306369389/244140625000 +. 124497279820089/7812500000000 * _x_20 +. (-111099101872869/7812500000000) * _x_27 +. (-70622501127057/2500000000000) * _x_34 +. (-62513077632687/15625000000000) * _x_41 +. (-1522773440427591/62500000000000) * _x_48 +. 423558714947247/12500000000000 * _x_55 else if _x_56 <= 595512221/312500000 then … else …) >= (if _x_106 <= (-341987779/312500000) then 28114831522503/7812500000000 +. 67395431164941/31250000000000 * _x_109 +. (-60142453582761/31250000000000) * _x_77 +. (-38230826571333/10000000000000) * _x_84 +. (-33840866455803/62500000000000) * _x_91 +. (-824339075780979/250000000000000) * _x_98 +. 229289525512443/50000000000000 * _x_105 else if _x_106 <= (-29487779/312500000) then 213430965464483/31250000000000 +. 732799213218501/125000000000000 * _x_109 +. (-653936652747521/125000000000000) * _x_77 +. (-415688706903613/40000000000000) * _x_84 +. (-367956104513283/250000000000000) * _x_91 +. (-8963145063634619/1000000000000000) * _x_98 +. 2493094576152323/200000000000000 * _x_105 else if _x_106 <= 283012221/312500000 then 1852306369389/244140625000 +. 124497279820089/7812500000000 * _x_109 +. (-111099101872869/7812500000000) * _x_77 +. (-70622501127057/2500000000000) * _x_84 +. (-62513077632687/15625000000000) * _x_91 +. (-1522773440427591/62500000000000) * _x_98 +. 423558714947247/12500000000000 * _x_105 else if _x_106 <= 595512221/312500000 then … else …))expansions: []
rewrite_steps: forward_chaining: - Sat (Some let a : nn_input = {month = Jan; day = Tue; dmc = (Q.of_string "24071693176255305204995774355157911171745916535164711/130812696337961989065667223239362401085882856200000"); temp = (Q.of_string "28740379267551135462365274169038593/80313472375754846344478853462320000"); rh = (Q.of_string "1749390517427770976867/145708429369777734000"); rain = (Q.of_string "10830863650220655949604684927151011046139629487337/4087896760561312158302100726230075033933839256250")} let b : nn_input = {month = Jan; day = Tue; dmc = (Q.of_string "24071693176255305204995774355157911171745916535164711/130812696337961989065667223239362401085882856200000"); temp = (Q.of_nativeint (0n)); rh = (Q.of_string "1749390517427770976867/145708429369777734000"); rain = (Q.of_string "10830863650220655949604684927151011046139629487337/4087896760561312158302100726230075033933839256250")} )
Loading..
In [24]:
CX.a.temp;;
CX.b.temp;;
nn_model CX.a;;
nn_model CX.b;;
Out[24]:
- : real = 0.357852529811 - : real = 0. - : real = 1.37347847547 - : real = 1.37651315396
Although the network doesn't satisfy our original verification statement we can restrict our setting in a sensible way in order to prove something slightly weaker:
- There is very little data from winter months, and so the model is unlikely to generalise well here, hence we'll only consider non-winter months
- We'll increase the tolerance in temperature to 10 degrees celsius
- We'll increase the tolerance in area burned to 25 hectares
In [25]:
let winter month = month = Oct || month = Nov || month = Dec || month = Jan || month = Feb
verify (fun a b ->
is_valid_nn a &&
is_valid_nn b &&
a.month = b.month &&
not (winter a.month) &&
a.day = b.day &&
a.dmc = b.dmc &&
a.rh = b.rh &&
a.rain = b.rain &&
(a.temp -. 10.0) >=. b.temp ==>
(nn_model a +. 25.0) >=. nn_model b)
Out[25]:
val winter : month -> bool = <fun> - : nn_input -> nn_input -> bool = <fun>
Proved
proof
| ground_instances: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| definitions: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| inductions: | 0 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| search_time: | 22.109s | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| details: | Expand
|
Expand
start[22.109s] let (_x_0 : real) = ( :var_0: ).dmc in let (_x_1 : real) = ( :var_0: ).temp in let (_x_2 : real) = ( :var_0: ).rh in let (_x_3 : real) = ( :var_0: ).rain in let (_x_4 : real) = ( :var_1: ).dmc in let (_x_5 : real) = ( :var_1: ).temp in let (_x_6 : real) = ( :var_1: ).rh in let (_x_7 : real) = ( :var_1: ).rain in let (_x_8 : month) = ( :var_0: ).month in let (_x_9 : real) = 5031/25000 * … +. (-7861/50000) * … +. (-19063/100000) * … +. (-27281/50000) * … +. 137/4000 * … +. 6263/12500 * … +. (-173/6250) in let (_x_10 : real) = 29103/100000 * … +. 159/5000 * … +. (-1021/6250) * … +. 17919/100000 * … +. 32971/100000 * … +. (-21603/50000) * … +. (-131/5000) in let (_x_11 : real) = 66419/100000 * … +. 25399/100000 * … +. 449/100000 * … +. 3841/100000 * … +. (-25741/50000) * … +. 58299/100000 * … +. 5929/50000 in let (_x_12 : real) = 23799/50000 * … +. (-18071/50000) * … +. 38981/100000 * … +. 1727/6250 * … +. (-61231/100000) * … +. (-1831/50000) * … +. (-289/10000) in let (_x_13 : real) = 10277/100000 * … +. (-28841/100000) * … +. 4637/100000 * … +. 3601/12500 * … +. 5957/100000 * … +. (-22041/100000) * … +. 1827/10000 in let (_x_14 : real) = 13901/25000 * … +. (-803/20000) * … +. 10557/100000 * … +. 60757/100000 * … +. (-16157/50000) * … +. 47933/100000 * … +. (-6219/25000) in let (_x_15 : real) = 444323/100000 * (3531/12500 * (if _x_9 > 0 then _x_9 else 0) +. (-3151/12500) * (if _x_10 > 0 then _x_10 else 0) +. (-2003/4000) * (if _x_11 > 0 then _x_11 else 0) +. (-1773/25000) * (if _x_12 > 0 then _x_12 else 0) +. (-43189/100000) * (if _x_13 > 0 then _x_13 else 0) +. 12013/20000 * (if _x_14 > 0 then _x_14 else 0) +. 1473/3125) in let (_x_16 : real) = if _x_15 <= 1 then (_x_15 - 0) * 42957/25000 else if _x_15 <= 2 then (_x_15 - 15803/25000) * 467077/100000 else if _x_15 <= 3 then (_x_15 - 149679/100000) * 79353/6250 else if _x_15 <= 4 then … else … in (0 <= _x_0) && ((_x_0 <= 500) && ((0 <= _x_1) && ((_x_1 <= 40) && ((0 <= _x_2) && ((_x_2 <= 100) && ((0 <= _x_3) && (_x_3 <= 15))))))) && ((0 <= _x_4) && ((_x_4 <= 500) && ((0 <= _x_5) && ((_x_5 <= 40) && ((0 <= _x_6) && ((_x_6 <= 100) && ((0 <= _x_7) && (_x_7 <= 15))))))) && ((_x_8 = ( :var_1: ).month) && (not ((_x_8 = Oct) || ((_x_8 = Nov) || ((_x_8 = Dec) || ((_x_8 = Jan) || (_x_8 = Feb))))) && ((( :var_0: ).day = ( :var_1: ).day) && ((_x_0 = _x_4) && ((_x_2 = _x_6) && ((_x_3 = _x_7) && (_x_1 - 10 >= _x_5)))))))) ==> _x_16 +. 25 >= _x_16simplify
into: let (_x_0 : real) = ( :var_0: ).dmc in let (_x_1 : real) = ( :var_0: ).temp in let (_x_2 : real) = ( :var_0: ).rh in let (_x_3 : real) = ( :var_0: ).rain in let (_x_4 : real) = ( :var_1: ).dmc in let (_x_5 : real) = ( :var_1: ).temp in let (_x_6 : real) = ( :var_1: ).rh in let (_x_7 : real) = ( :var_1: ).rain in let (_x_8 : month) = ( :var_0: ).month in let (_x_9 : month) = ( :var_1: ).month in let (_x_10 : bool) = _x_8 = Jan in let (_x_11 : bool) = _x_8 = Feb in let (_x_12 : day) = ( :var_0: ).day in let (_x_13 : day) = ( :var_1: ).day in let (_x_14 : bool) = _x_8 = Mar in let (_x_15 : real) = if _x_10 then 67/500 else if _x_11 then 1/2 else if _x_14 then 1 else … in let (_x_16 : real) = 5031/50000 * _x_15 in let (_x_17 : bool) = (_x_12 = Wed) || (_x_12 = Thu) in let (_x_18 : bool) = _x_12 = Tue in let (_x_19 : bool) = _x_12 = Mon in let (_x_20 : real) = if _x_19 then 377/1000 else if _x_18 then 1223/1000 else if _x_17 then 1901/1000 else … in let (_x_21 : real) = (-7861/95050) * _x_20 in let (_x_22 : real) = (-19063/29020000) * _x_0 in let (_x_23 : real) = (-27281/1555000) * _x_1 in let (_x_24 : real) = 137/340000 * _x_2 in let (_x_25 : real) = 6263/80000 * _x_3 in let (_x_26 : real) = if _x_16 +. _x_21 +. _x_22 +. _x_23 +. _x_24 +. _x_25 <= (-1716983137/306857480000) then 0 else 1716983137/306857480000 +. _x_16 +. _x_21 +. _x_22 +. _x_23 +. _x_24 +. _x_25 in let (_x_27 : real) = 29103/200000 * _x_15 in let (_x_28 : real) = 159/9505 * _x_20 in let (_x_29 : real) = (-1021/1813750) * _x_0 in let (_x_30 : real) = 17919/3110000 * _x_1 in let (_x_31 : real) = 32971/8500000 * _x_2 in let (_x_32 : real) = (-21603/320000) * _x_3 in let (_x_33 : real) = if _x_27 +. _x_28 +. _x_29 +. _x_30 +. _x_31 +. _x_32 <= 73983893263/767143700000 then 0 else (-73983893263/767143700000) +. _x_27 +. _x_28 +. _x_29 +. _x_30 +. _x_31 +. _x_32 in let (_x_34 : real) = 66419/200000 * _x_15 in let (_x_35 : real) = 25399/190100 * _x_20 in let (_x_36 : real) = 449/29020000 * _x_0 in let (_x_37 : real) = 3841/3110000 * _x_1 in let (_x_38 : real) = (-25741/4250000) * _x_2 in let (_x_39 : real) = 58299/640000 * _x_3 in let (_x_40 : real) = if _x_34 +. _x_35 +. _x_36 +. _x_37 +. _x_38 +. _x_39 <= (-317131778543/1534287400000) then 0 else 317131778543/1534287400000 +. _x_34 +. _x_35 +. _x_36 +. _x_37 +. _x_38 +. _x_39 in let (_x_41 : real) = 23799/100000 * _x_15 in let (_x_42 : real) = (-18071/95050) * _x_20 in let (_x_43 : real) = 38981/29020000 * _x_0 in let (_x_44 : real) = 1727/194375 * _x_1 in let (_x_45 : real) = (-61231/8500000) * _x_2 in let (_x_46 : real) = (-1831/320000) * _x_3 in let (_x_47 : real) = if _x_41 +. _x_42 +. _x_43 +. _x_44 +. _x_45 +. _x_46 <= (-89188713933/1534287400000) then 0 else 89188713933/1534287400000 +. _x_41 +. _x_42 +. _x_43 +. _x_44 +. _x_45 +. _x_46 in let (_x_48 : real) = 10277/200000 * _x_15 in let (_x_49 : real) = (-28841/190100) * _x_20 in let (_x_50 : real) = 4637/29020000 * _x_0 in let (_x_51 : real) = 3601/388750 * _x_1 in let (_x_52 : real) = 5957/8500000 * _x_2 in let (_x_53 : real) = (-22041/640000) * _x_3 in let (_x_54 : real) = if _x_48 +. _x_49 +. _x_50 +. _x_51 +. _x_52 +. _x_53 <= (-372238333/2454859840) then 0 else 372238333/2454859840 +. _x_48 +. _x_49 +. _x_50 +. _x_51 +. _x_52 +. _x_53 in let (_x_55 : real) = 13901/50000 * _x_15 in let (_x_56 : real) = (-803/38020) * _x_20 in let (_x_57 : real) = 10557/29020000 * _x_0 in let (_x_58 : real) = 60757/3110000 * _x_1 in let (_x_59 : real) = (-16157/4250000) * _x_2 in let (_x_60 : real) = 47933/640000 * _x_3 in let (_x_61 : real) = if _x_55 +. _x_56 +. _x_57 +. _x_58 +. _x_59 +. _x_60 <= 72146699557/306857480000 then 0 else (-72146699557/306857480000) +. _x_55 +. _x_56 +. _x_57 +. _x_58 +. _x_59 +. _x_60 in let (_x_62 : real) = 1568904513/1250000000 * _x_26 +. (-1400061773/1250000000) * _x_33 +. (-889978969/400000000) * _x_40 +. (-787784679/2500000000) * _x_47 +. (-19189866047/10000000000) * _x_54 +. 5337652199/2000000000 * _x_61 in let (_x_63 : real) = if _x_10 then 67/500 else if _x_11 then 1/2 else if _x_14 then 1 else if _x_8 = Apr then 3/2 else … in let (_x_64 : real) = 5031/50000 * _x_63 in let (_x_65 : real) = if _x_19 then 377/1000 else if _x_18 then 1223/1000 else if _x_17 then 1901/1000 else if _x_12 = Fri then 1223/1000 else … in let (_x_66 : real) = (-7861/95050) * _x_65 in let (_x_67 : real) = if _x_64 +. _x_66 +. _x_22 +. _x_23 +. _x_24 +. _x_25 <= (-1716983137/306857480000) then 0 else 1716983137/306857480000 +. _x_64 +. _x_66 +. _x_22 +. _x_23 +. _x_24 +. _x_25 in let (_x_68 : real) = 29103/200000 * _x_63 in let (_x_69 : real) = 159/9505 * _x_65 in let (_x_70 : real) = if _x_68 +. _x_69 +. _x_29 +. _x_30 +. _x_31 +. _x_32 <= 73983893263/767143700000 then 0 else (-73983893263/767143700000) +. _x_68 +. _x_69 +. _x_29 +. _x_30 +. _x_31 +. _x_32 in let (_x_71 : real) = 66419/200000 * _x_63 in let (_x_72 : real) = 25399/190100 * _x_65 in let (_x_73 : real) = if _x_71 +. _x_72 +. _x_36 +. _x_37 +. _x_38 +. _x_39 <= (-317131778543/1534287400000) then 0 else 317131778543/1534287400000 +. _x_71 +. _x_72 +. _x_36 +. _x_37 +. _x_38 +. _x_39 in let (_x_74 : real) = 23799/100000 * _x_63 in let (_x_75 : real) = (-18071/95050) * _x_65 in let (_x_76 : real) = if _x_74 +. _x_75 +. _x_43 +. _x_44 +. _x_45 +. _x_46 <= (-89188713933/1534287400000) then 0 else 89188713933/1534287400000 +. _x_74 +. _x_75 +. _x_43 +. _x_44 +. _x_45 +. _x_46 in let (_x_77 : real) = 10277/200000 * _x_63 in let (_x_78 : real) = (-28841/190100) * _x_65 in let (_x_79 : real) = if _x_77 +. _x_78 +. _x_50 +. _x_51 +. _x_52 +. _x_53 <= (-372238333/2454859840) then 0 else 372238333/2454859840 +. _x_77 +. _x_78 +. _x_50 +. _x_51 +. _x_52 +. _x_53 in let (_x_80 : real) = 13901/50000 * _x_63 in let (_x_81 : real) = (-803/38020) * _x_65 in let (_x_82 : real) = if _x_80 +. _x_81 +. _x_57 +. _x_58 +. _x_59 +. _x_60 <= 72146699557/306857480000 then 0 else (-72146699557/306857480000) +. _x_80 +. _x_81 +. _x_57 +. _x_58 +. _x_59 +. _x_60 in let (_x_83 : bool) = _x_9 = Mar in let (_x_84 : bool) = _x_9 = Feb in let (_x_85 : bool) = _x_9 = Jan in let (_x_86 : real) = if _x_85 then 67/500 else if _x_84 then 1/2 else if _x_83 then 1 else if _x_9 = Apr then 3/2 else … in let (_x_87 : real) = 5031/50000 * _x_86 in let (_x_88 : bool) = (_x_13 = Wed) || (_x_13 = Thu) in let (_x_89 : bool) = _x_13 = Tue in let (_x_90 : bool) = _x_13 = Mon in let (_x_91 : real) = if _x_90 then 377/1000 else if _x_89 then 1223/1000 else if _x_88 then 1901/1000 else if _x_13 = Fri then 1223/1000 else … in let (_x_92 : real) = (-7861/95050) * _x_91 in let (_x_93 : real) = (-19063/29020000) * _x_4 in let (_x_94 : real) = (-27281/1555000) * _x_5 in let (_x_95 : real) = 137/340000 * _x_6 in let (_x_96 : real) = 6263/80000 * _x_7 in let (_x_97 : real) = 29103/200000 * _x_86 in let (_x_98 : real) = 159/9505 * _x_91 in let (_x_99 : real) = (-1021/1813750) * _x_4 in let (_x_100 : real) = 17919/3110000 * _x_5 in let (_x_101 : real) = 32971/8500000 * _x_6 in let (_x_102 : real) = (-21603/320000) * _x_7 in let (_x_103 : real) = 66419/200000 * _x_86 in let (_x_104 : real) = 25399/190100 * _x_91 in let (_x_105 : real) = 449/29020000 * _x_4 in let (_x_106 : real) = 3841/3110000 * _x_5 in let (_x_107 : real) = (-25741/4250000) * _x_6 in let (_x_108 : real) = 58299/640000 * _x_7 in let (_x_109 : real) = if _x_85 then 67/500 else if _x_84 then 1/2 else if _x_83 then 1 else … in let (_x_110 : real) = (-18071/95050) * _x_91 in let (_x_111 : real) = 38981/29020000 * _x_4 in let (_x_112 : real) = 1727/194375 * _x_5 in let (_x_113 : real) = (-61231/8500000) * _x_6 in let (_x_114 : real) = (-1831/320000) * _x_7 in let (_x_115 : real) = if 23799/100000 * _x_86 +. _x_110 +. _x_111 +. _x_112 +. _x_113 +. _x_114 <= (-89188713933/1534287400000) then 0 else 89188713933/1534287400000 +. 23799/100000 * _x_109 +. _x_110 +. _x_111 +. _x_112 +. _x_113 +. _x_114 in let (_x_116 : real) = 10277/200000 * _x_86 in let (_x_117 : real) = (-28841/190100) * _x_91 in let (_x_118 : real) = 4637/29020000 * _x_4 in let (_x_119 : real) = 3601/388750 * _x_5 in let (_x_120 : real) = 5957/8500000 * _x_6 in let (_x_121 : real) = (-22041/640000) * _x_7 in let (_x_122 : real) = if _x_116 +. _x_117 +. _x_118 +. _x_119 +. _x_120 +. _x_121 <= (-372238333/2454859840) then 0 else 372238333/2454859840 +. _x_116 +. _x_117 +. _x_118 +. _x_119 +. _x_120 +. _x_121 in let (_x_123 : real) = 13901/50000 * _x_86 in let (_x_124 : real) = (-803/38020) * _x_91 in let (_x_125 : real) = 10557/29020000 * _x_4 in let (_x_126 : real) = 60757/3110000 * _x_5 in let (_x_127 : real) = (-16157/4250000) * _x_6 in let (_x_128 : real) = 47933/640000 * _x_7 in let (_x_129 : real) = if _x_123 +. _x_124 +. _x_125 +. _x_126 +. _x_127 +. _x_128 <= 72146699557/306857480000 then 0 else (-72146699557/306857480000) +. _x_123 +. _x_124 +. _x_125 +. _x_126 +. _x_127 +. _x_128 in let (_x_130 : real) = 1568904513/1250000000 * (if _x_87 +. _x_92 +. _x_93 +. _x_94 +. _x_95 +. _x_96 <= (-1716983137/306857480000) then 0 else (1716983137/306857480000 +. _x_87 +. _x_92 +. _x_93 +. _x_94 +. _x_95 +. _x_96)) +. (-1400061773/1250000000) * (if _x_97 +. _x_98 +. _x_99 +. _x_100 +. _x_101 +. _x_102 <= 73983893263/767143700000 then 0 else ((-73983893263/767143700000) +. _x_97 +. _x_98 +. _x_99 +. _x_100 +. _x_101 +. _x_102)) +. (-889978969/400000000) * (if _x_103 +. _x_104 +. _x_105 +. _x_106 +. _x_107 +. _x_108 <= (-317131778543/1534287400000) then 0 else (317131778543/1534287400000 +. _x_103 +. _x_104 +. _x_105 +. _x_106 +. _x_107 +. _x_108)) +. (-787784679/2500000000) * _x_115 +. (-19189866047/10000000000) * _x_122 +. 5337652199/2000000000 * _x_129 in let (_x_131 : real) = 5031/50000 * _x_109 in let (_x_132 : real) = if _x_90 then 377/1000 else if _x_89 then 1223/1000 else if _x_88 then 1901/1000 else … in let (_x_133 : real) = (-7861/95050) * _x_132 in let (_x_134 : real) = if _x_131 +. _x_133 +. _x_93 +. _x_94 +. _x_95 +. _x_96 <= (-1716983137/306857480000) then 0 else 1716983137/306857480000 +. _x_131 +. _x_133 +. _x_93 +. _x_94 +. _x_95 +. _x_96 in let (_x_135 : real) = 29103/200000 * _x_109 in let (_x_136 : real) = 159/9505 * _x_132 in let (_x_137 : real) = if _x_135 +. _x_136 +. _x_99 +. _x_100 +. _x_101 +. _x_102 <= 73983893263/767143700000 then 0 else (-73983893263/767143700000) +. _x_135 +. _x_136 +. _x_99 +. _x_100 +. _x_101 +. _x_102 in let (_x_138 : real) = 66419/200000 * _x_109 in let (_x_139 : real) = 25399/190100 * _x_132 in let (_x_140 : real) = if _x_138 +. _x_139 +. _x_105 +. _x_106 +. _x_107 +. _x_108 <= (-317131778543/1534287400000) then 0 else 317131778543/1534287400000 +. _x_138 +. _x_139 +. _x_105 +. _x_106 +. _x_107 +. _x_108 in not ((0 <= _x_0) && (_x_0 <= 500) && (0 <= _x_1) && (_x_1 <= 40) && (0 <= _x_2) && (_x_2 <= 100) && (0 <= _x_3) && (_x_3 <= 15) && (0 <= _x_4) && (_x_4 <= 500) && (0 <= _x_5) && (_x_5 <= 40) && (0 <= _x_6) && (_x_6 <= 100) && (0 <= _x_7) && (_x_7 <= 15) && (_x_8 = _x_9) && not ((_x_8 = Oct) || (_x_8 = Nov) || (_x_8 = Dec) || _x_10 || _x_11) && (_x_12 = _x_13) && (_x_0 = _x_4) && (_x_2 = _x_6) && (_x_3 = _x_7) && (_x_1 >= 10 +. _x_5)) || ((if 1568904513/1250000000 * _x_67 +. (-1400061773/1250000000) * _x_70 +. (-889978969/400000000) * _x_73 +. (-787784679/2500000000) * _x_76 +. (-19189866047/10000000000) * _x_79 +. 5337652199/2000000000 * _x_82 <= (-341987779/312500000) then 28114831522503/7812500000000 +. 67395431164941/31250000000000 * _x_67 +. (-60142453582761/31250000000000) * _x_70 +. (-38230826571333/10000000000000) * _x_73 +. (-33840866455803/62500000000000) * _x_76 +. (-824339075780979/250000000000000) * _x_79 +. 229289525512443/50000000000000 * _x_82 else if _x_62 <= (-29487779/312500000) then 213430965464483/31250000000000 +. 732799213218501/125000000000000 * _x_26 +. (-653936652747521/125000000000000) * _x_33 +. (-415688706903613/40000000000000) * _x_40 +. (-367956104513283/250000000000000) * _x_47 +. (-8963145063634619/1000000000000000) * _x_54 +. 2493094576152323/200000000000000 * _x_61 else if _x_62 <= 283012221/312500000 then 1852306369389/244140625000 +. 124497279820089/7812500000000 * _x_26 +. (-111099101872869/7812500000000) * _x_33 +. (-70622501127057/2500000000000) * _x_40 +. (-62513077632687/15625000000000) * _x_47 +. (-1522773440427591/62500000000000) * _x_54 +. 423558714947247/12500000000000 * _x_61 else if _x_62 <= 595512221/312500000 then … else …) >= (-25) +. (if _x_130 <= (-341987779/312500000) then 28114831522503/7812500000000 +. 67395431164941/31250000000000 * _x_134 +. (-60142453582761/31250000000000) * _x_137 +. (-38230826571333/10000000000000) * _x_140 +. (-33840866455803/62500000000000) * _x_115 +. (-824339075780979/250000000000000) * _x_122 +. 229289525512443/50000000000000 * _x_129 else if _x_130 <= (-29487779/312500000) then 213430965464483/31250000000000 +. 732799213218501/125000000000000 * _x_134 +. (-653936652747521/125000000000000) * _x_137 +. (-415688706903613/40000000000000) * _x_140 +. (-367956104513283/250000000000000) * _x_115 +. (-8963145063634619/1000000000000000) * _x_122 +. 2493094576152323/200000000000000 * _x_129 else if _x_130 <= 283012221/312500000 then 1852306369389/244140625000 +. 124497279820089/7812500000000 * _x_134 +. (-111099101872869/7812500000000) * _x_137 +. (-70622501127057/2500000000000) * _x_140 +. (-62513077632687/15625000000000) * _x_115 +. (-1522773440427591/62500000000000) * _x_122 +. 423558714947247/12500000000000 * _x_129 else if _x_130 <= 595512221/312500000 then … else …))expansions: []
rewrite_steps: forward_chaining: - Unsat
Loading..
Loading..
We hope you've enjoyed this short introduction to one of the many ways in which formal methods can be applied to machine learning. If you're interested in our work be sure to check our other notebooks, find out more and get email updates on our website, join the discussion on our Discord channel, and subscribe to our Medium publication.