<jupyter_start><jupyter_text>[//]:  (Copyright c 2021, <NAME>, <NAME>, <NAME>, <NAME>, <NAME>)[//]:  (All rights reserved.)[//]:  (This source code is licensed under the BSD-style license found in the)[//]:  (LICENSE file in the root directory of this source tree. ) FOSSIL BenchmarksThis notebook serves as a demonstration of the tool benchmarks. A set seed is used for repeatability.[FOSSIL-playground](FOSSIL-playground.ipynb). Lyapunov Function Benchmarks1.  [Nonpoly 0](non-poly0)1.  [Nonpoly 1](non-poly1)1.  [Nonpoly 2](non-poly3)1.  [Nonpoly 3](non-poly3)1.  [Poly 1](poly1)1.  [Poly 2](poly2)1.  [Poly 3](poly3)1.  [Poly 4](poly4)1.  [Hybrid Lyapunov](hi-lyap) Barrier Function Benchmarks1.  [Barrier 1](darboux)1.  [Barrier 2](elementary)1.  [Barrier 3](polynomial)1.  [Barrier 4](obstacle)1.  [Hybrid Barrier](hybrid)1.  [Hi-Ord4](hi-ord4)1.  [Hi-Ord6](hi-ord6)1.  [Hi-Ord8](hi-ord8)<jupyter_code># % Imports
import sys
sys.path.append('..')
from experiments.playground_utils import *
from experiments.benchmarks.benchmarks_bc import *
from experiments.benchmarks.benchmarks_lyap import twod_hybrid as hy_lyap 
from src.plots.plot_lyap import plot_lyapunov_fcn
from src.plots.plot_barriers import *<jupyter_output><empty_output><jupyter_text>Non-poly 0\begin{cases}\dot{x} =  -x+xy, \\\dot{y} =  -y, \end{cases}<jupyter_code>torch.manual_seed(167)
N_Dimensions = 2

x0, x1 = initialise_states(N_Dimensions)

dynamics = [
    -x0 + x0 * x1,
    -x1
]
activations =  [ActivationType.SQUARE]
neurons = [2] 
parameters = {CegisConfig.VERIFIER.k:VerifierType.DREAL, CegisConfig.ACTIVATION.k: activations, 
              CegisConfig.N_HIDDEN_NEURONS.k:neurons,   CegisConfig.POSITIVE_DOMAIN.k:True,
              CegisConfig.LLO.k:True, CegisConfig.SP_HANDLE.k:False}

mode = PrimerMode.LYAPUNOV

f_n, f_s = synthesise(dynamics, mode, OUTER_RADIUS=10, INNER_RADIUS=0.01,CEGIS_PARAMETERS=parameters)

x = np.array([x0,x1]).reshape(-1,1)
plot_lyapunov_fcn(x, f_s, dynamics)<jupyter_output>Single Equilibrium point found: 
 [(0, 0)]
================================================================================
  learner   0
================================================================================
0 - loss: 6.13293981552124 - acc: 58.6 %
================================================================================
  translator   0
================================================================================
Candidate: (pow(( - 0.244 * x0 - 0.676 * x1), 2) + pow(( - 0.146 * x0 + 1.216 * x1), 2))
================================================================================
  verifier   0
================================================================================
Counterexample Found: x0 : [9.846872884332737996, 9.846873195223373898]
x1 : [1.743292668714171656, 1.743292895789005925]
V(ctx) =  13.289696553428621
Vdot(ctx) =  -5.4261789728116128e-07
================================================================================
  consolidator   0
=======[...]<jupyter_text>Non-poly 1\begin{cases}\dot{x} = -x + 2x^2y \\\dot{y} = - y, \end{cases}<jupyter_code>torch.manual_seed(167)
N_Dimensions = 2
x0, x1 = initialise_states(N_Dimensions)

dynamics = [
    -x0 +2*x0**2 * x1,
    -x1
]
activations =  [ActivationType.LINEAR, ActivationType.SQUARE]
neurons = [20, 20] 
parameters = {CegisConfig.ACTIVATION.k: activations, CegisConfig.N_HIDDEN_NEURONS.k:neurons, 
              CegisConfig.POSITIVE_DOMAIN.k:True, CegisConfig.LLO.k:True, CegisConfig.SP_HANDLE.k:False}

mode = PrimerMode.LYAPUNOV

f_n, f_s = synthesise(dynamics, mode, OUTER_RADIUS=10, INNER_RADIUS=0.01, CEGIS_PARAMETERS=parameters)

x = np.array([x0,x1]).reshape(-1,1)
plot_lyapunov_fcn(x, simplify_f(f_s), dynamics)<jupyter_output>Single Equilibrium point found: 
 [(0, 0)]
================================================================================
  learner   0
================================================================================
0 - loss: 842.2959594726562 - acc: 45.0 %
================================================================================
  translator   0
================================================================================
Candidate: (... +
 ... +
 ... +
 ... +
 ... +
 ... +
 ... +
 ... +
 ... +
 ... +
 ... +
 ... +
 ... +
 ... +
 ... +
 ... +
 ... +
 ... +
 ... +
 ...)*
...
================================================================================
  verifier   0
================================================================================
Counterexample Found: [x1 = 1/16, x0 = 9]
V(ctx) =  19476106836999190301158611130771506218760983162774394466609609140902032497/6400000000000000000000000000000000000000000000000000000000000000000000000
Vdot(ctx) =  34479285408621[...]<jupyter_text>Non-poly 2\begin{cases}\dot{x} = -x \\\dot{y} = - 2y + 0.1 x y^2 + z \\\dot{z} = -z -1.5 y, \end{cases}<jupyter_code>torch.manual_seed(167)
N_Dimensions = 3
x0, x1, x2 = initialise_states(N_Dimensions)

dynamics = [
    -x0,
    -2*x1 + 0.1*x0*x1**2 + x2,
    -x2 - 1.5*x1
]
activations =  [ActivationType.LINEAR, ActivationType.SQUARE]
neurons = [10, 10]
parameters = {CegisConfig.ACTIVATION.k: activations, CegisConfig.N_HIDDEN_NEURONS.k:neurons,
              CegisConfig.POSITIVE_DOMAIN.k:True, CegisConfig.LLO.k:True, CegisConfig.SP_HANDLE.k:False,
              CegisConfig.BATCH_SIZE.k: 750}
 
mode = PrimerMode.LYAPUNOV
f_n, f_s = synthesise(dynamics, mode, OUTER_RADIUS=10, INNER_RADIUS=0.01, CEGIS_PARAMETERS=parameters)<jupyter_output>Single Equilibrium point found: 
 [(0, 0, 0)]
================================================================================
  learner   0
================================================================================
0 - loss: 0.30259019136428833 - acc: 98.53333333333333 %
================================================================================
  translator   0
================================================================================
Candidate: (... + ... + ... + ... + ... + ... + ... + ... + ... + ...)*
...
================================================================================
  verifier   0
================================================================================
No counterexamples found!
================================================================================
  consolidator   0
================================================================================
Found a Lyapunov function
Learner times: total=0.01936735599883832s,min=0.01936735[...]<jupyter_text>Non-poly 3\begin{cases}\dot{x} = -3x -0.1 x y^3 \\\dot{y} = - y + z \\\dot{z} = -z.  \end{cases}<jupyter_code>torch.manual_seed(167)
N_Dimensions = 3
x0, x1, x2 = initialise_states(N_Dimensions)

dynamics = [
    -3*x0 - 0.1*x0*x1**3,
    -x1 + x2,
    -x2
]
activations =  [ActivationType.SQUARE]
neurons = [4] 
parameters = {CegisConfig.ACTIVATION.k: activations, CegisConfig.N_HIDDEN_NEURONS.k:neurons,
              CegisConfig.POSITIVE_DOMAIN.k:True, CegisConfig.LLO.k:True, CegisConfig.SP_HANDLE.k:True}

mode = PrimerMode.LYAPUNOV

f_n, f_s = synthesise(dynamics, mode, OUTER_RADIUS=10, INNER_RADIUS=0.01, CEGIS_PARAMETERS=parameters)<jupyter_output>Single Equilibrium point found: 
 [(0, 0, 0)]
================================================================================
  learner   0
================================================================================
0 - loss: 0.10331675410270691 - acc: 93.2 %
================================================================================
  translator   0
================================================================================
Candidate: 5106310015144349/10000000000000000*x1**2 +
11768349883639817/50000000000000000*x2**2 +
1884519960920811/2000000000000000*x0**2 +
19247983988046613/1000000000000000000*x1*x2 +
1740600376153001/100000000000000000*x0*x1 +
646275979959011/2000000000000000*x0*x2
================================================================================
  verifier   0
================================================================================
No counterexamples found!
================================================================================
  [...]<jupyter_text>Poly 1\begin{cases}\dot{x} = - x^3 - x z^2, \\\dot{y} = -y - x^2 x_1, \\\dot{z} = -z - \dfrac{3 z}{z^2 + 1} + 3 x^2 z.\end{cases} Note that $ z^2 + 1 > 0$<jupyter_code>torch.manual_seed(167)
N_Dimensions = 3
x0, x1, x2 = initialise_states(N_Dimensions)

dynamics = dynamics = [
    -x0**3 - x0*x2**2,
    -x1 - x0**2 * x1,
    -x2 - 3*x2 + 3*x0**2*x2
]
activations =  [ActivationType.SQUARE]
neurons = [5] 
parameters = {CegisConfig.VERIFIER.k: VerifierType.DREAL, CegisConfig.ACTIVATION.k: activations,
              CegisConfig.N_HIDDEN_NEURONS.k: neurons,
              CegisConfig.LLO.k: True, CegisConfig.SP_HANDLE.k: False, CegisConfig.N_VARS.k: 3}

mode = PrimerMode.LYAPUNOV

f_n, f_s = synthesise(dynamics, mode, OUTER_RADIUS=10.0, INNER_RADIUS=0.01, CEGIS_PARAMETERS=parameters)<jupyter_output>Single Equilibrium point found: 
 [(0, 0, 0)]
================================================================================
  learner   0
================================================================================
0 - loss: 12.154703140258789 - acc: 93.2 %
================================================================================
  translator   0
================================================================================
Candidate: (pow(( - 0.649 * x0 + 0.465 * x1 - 0.059 * x2), 2) + pow((0.155 * x0 - 0.443 * x1 - 0.113 * x2), 2) + pow((0.324 * x0 - 0.325 * x1 + 0.374 * x2), 2) + pow((0.447 * x0 + 0.654 * x1 - 0.011 * x2), 2) + pow((0.565 * x0 + 0.371 * x1 - 0.186 * x2), 2))
================================================================================
  verifier   0
================================================================================
No counterexamples found!
================================================================================
  consolidato[...]<jupyter_text>Poly 2\begin{cases}\dot{x} = - x^3 + y &  \\ \dot{y} = -x -y. & \end{cases}<jupyter_code>torch.manual_seed(167)
N_Dimensions = 3
x0, x1, x2 = initialise_states(N_Dimensions)

dynamics = [
    -x0**3 + x1,
    -x0 - x1
]
activations =  [ActivationType.SQUARE]
neurons = [10] 
parameters = {CegisConfig.ACTIVATION.k: activations, CegisConfig.N_HIDDEN_NEURONS.k:neurons, 
              CegisConfig.LLO.k:True, CegisConfig.SP_HANDLE.k:False
             }

mode = PrimerMode.LYAPUNOV

f_n, f_s = synthesise(dynamics, mode, OUTER_RADIUS=10, INNER_RADIUS=0.01, CEGIS_PARAMETERS=parameters)
x = np.array([x0,x1]).reshape(2,1)
plot_lyapunov_fcn(x, simplify_f(f_s), dynamics)<jupyter_output>Single Equilibrium point found: 
 [(0, 0)]
================================================================================
  learner   0
================================================================================
0 - loss: 0.19706033170223236 - acc: 98.0 %
100 - loss: -0.00997925829142332 - acc: 99.8 %
================================================================================
  translator   0
================================================================================
Candidate: (... + ... + ... + ... + ... + ... + ... + ... + ... + ...)*
...
================================================================================
  verifier   0
================================================================================
Counterexample Found: [x1 = 0, x0 = 1/8]
V(ctx) =  53932241350183527931655680135008929/640000000000000000000000000000000000
Vdot(ctx) =  387521826328191812608820024814339871/20480000000000000000000000000000000000
=============================================[...]<jupyter_text>Poly 3\begin{cases}\dot{x}= -x^3 - y^2, \\\dot{y}= xy - y^3.\end{cases}<jupyter_code>torch.manual_seed(167)
N_Dimensions = 2
x0, x1 = initialise_states(N_Dimensions)

dynamics = [
    -x0**3 -x1**2,
    x0*x1 - x1**3
    
]
activations =  [ActivationType.SQUARE]
neurons = [10] 
parameters = {CegisConfig.VERIFIER.k:VerifierType.DREAL, CegisConfig.ACTIVATION.k: activations, 
              CegisConfig.N_HIDDEN_NEURONS.k:neurons, CegisConfig.LLO.k:True, CegisConfig.SP_HANDLE.k:False}

mode = PrimerMode.LYAPUNOV

f_n, f_s = synthesise(dynamics, mode, OUTER_RADIUS=10, INNER_RADIUS = 0.01, CEGIS_PARAMETERS=parameters)
x = np.array([x0,x1]).reshape(2,1)
plot_lyapunov_fcn(x, simplify_f(f_s), dynamics)<jupyter_output>Single Equilibrium point found: 
 [(0, 0)]
================================================================================
  learner   0
================================================================================
0 - loss: -0.04395664855837822 - acc: 98.2 %
100 - loss: -0.09272778034210205 - acc: 99.4 %
200 - loss: -0.022348348051309586 - acc: 99.6 %
300 - loss: -0.024965103715658188 - acc: 99.6 %
400 - loss: -0.02986432984471321 - acc: 99.8 %
500 - loss: -0.03802625089883804 - acc: 99.8 %
600 - loss: -0.050862569361925125 - acc: 99.6 %
700 - loss: -0.0715465247631073 - acc: 99.8 %
800 - loss: -0.10505744069814682 - acc: 99.8 %
900 - loss: -0.15920929610729218 - acc: 99.8 %
999 - loss: -0.018043139949440956 - acc: 99.8 %
================================================================================
  translator   0
================================================================================
Candidate: (pow(( - 31.758 * x0 + 5.189 * x1), 2) + pow(( - 31.171 * x0 + 5.679 * x1[...]<jupyter_text>Poly 4\begin{cases}\dot{x}= - x - 1.5 x^2 y^3,\\\dot{y}=-y^3 + 0.5x^3 y^2.\end{cases}<jupyter_code>torch.manual_seed(167)
N_Dimensions = 2
x0, x1 = initialise_states(N_Dimensions)

dynamics = [
    -x0 - 1.5*x0**2*x1**3,
    -x1**3 + 0.5*x0**3*x1**2
]
activations =  [ActivationType.SQUARE]
neurons = [5] 
parameters = {CegisConfig.VERIFIER.k:VerifierType.DREAL,CegisConfig.ACTIVATION.k: activations, 
              CegisConfig.N_HIDDEN_NEURONS.k:neurons, CegisConfig.LLO.k:True, CegisConfig.SP_HANDLE.k:False}

mode = PrimerMode.LYAPUNOV

f_n, f_s = synthesise(dynamics, mode, OUTER_RADIUS=10, INNER_RADIUS = 0.01, CEGIS_PARAMETERS=parameters)
x = np.array([x0,x1]).reshape(2,1)
plot_lyapunov_fcn(x, simplify_f(f_s), dynamics)<jupyter_output>Single Equilibrium point found: 
 [(0, 0)]
================================================================================
  learner   0
================================================================================
0 - loss: 341.4746398925781 - acc: 80.4 %
================================================================================
  translator   0
================================================================================
Candidate: (pow(( - 0.119 * x0 - 0.071 * x1), 2) + pow((0.067 * x0 - 0.392 * x1), 2) + pow((0.17 * x0 + 0.503 * x1), 2) + pow((0.345 * x0 - 0.584 * x1), 2) + pow((0.355 * x0 + 0.343 * x1), 2))
================================================================================
  verifier   0
================================================================================
No counterexamples found!
================================================================================
  consolidator   0
================================================================[...]<jupyter_text>Hybrid Lyapunov$$ f(x, y) = \begin{cases}f_1 & \text{if } y < 0, \\f_2 & \text{otherwise},\end{cases}$$where $$f_1 = \begin{cases}\dot{x} = -x, \\\dot{y} = - y - 0.5 x^3, \\\end{cases}$$$$f_2 = \begin{cases}\dot{x} = -x, \\\dot{y} =  -y -x^2 - 0.25 y^3, \\\end{cases}$$<jupyter_code>torch.manual_seed(167)
dynamics = hy_lyap
dimension = 2
activations =  [ActivationType.SQUARE]
neurons = [10]
verifier_type = VerifierType.DREAL

parameters = {CegisConfig.N_VARS.k: dimension, CegisConfig.VERIFIER.k: VerifierType.Z3, 
              CegisConfig.ACTIVATION.k: activations, CegisConfig.N_HIDDEN_NEURONS.k:neurons, 
              CegisConfig.SP_HANDLE.k: False, CegisConfig.SP_SIMPLIFY.k: False,
              CegisConfig.LLO.k: True, CegisConfig.BATCH_SIZE.k: 1000}

mode = PrimerMode.LYAPUNOV

f_n, f_s = synthesise(dynamics, mode, OUTER_RADIUS=10, CEGIS_PARAMETERS=parameters)

x = np.array([x0,x1]).reshape(2,1)
plot_lyapunov_fcn(x, simplify_f(f_s), dynamics)<jupyter_output>================================================================================
  learner   0
================================================================================
0 - loss: 785.2838745117188 - acc: 68.4 %
================================================================================
  translator   0
================================================================================
Candidate: (... + ... + ... + ... + ... + ... + ... + ... + ... + ...)*
...
================================================================================
  verifier   0
================================================================================
No counterexamples found!
================================================================================
  consolidator   0
================================================================================
Found a Lyapunov function
Learner times: total=0.33901313800015487s,min=0.33901313800015487s,max=0.33901313800015487s,avg=0.33901313800015487s
[...]<jupyter_text>Barrier Function Benchmarks  Barrier 1$$ \begin{cases} \dot{x} = y + 2xy  \\ \dot{y} = -x - y^2 + 2x^2 \end{cases}$$$$\begin{align*}& X = \{ -2 \leq x, y \leq 2 \}, \\& X_0 =  \{ 0 \leq x \leq 1, 1 \leq y \leq 2 \}, \\& X_u = \{ x+y^2 \leq 0 \}\end{align*}$$<jupyter_code>torch.manual_seed(167)
dynamics = barr_1
dimension = 2
activations =  [ActivationType.LINEAR]
neurons = [10] * len(activations)
verifier_type = VerifierType.DREAL

parameters = {CegisConfig.VERIFIER.k: verifier_type, CegisConfig.ACTIVATION.k: activations, 
              CegisConfig.N_HIDDEN_NEURONS.k:neurons, CegisConfig.N_VARS.k: dimension}

mode = PrimerMode.BARRIER

f_n, f_s = synthesise(dynamics, mode, CEGIS_PARAMETERS=parameters)
x = np.array([initialise_states(2)]).reshape(-1,1)
plot_darboux_bench(x, f_s)<jupyter_output>================================================================================
  learner   0
================================================================================
0 - loss: 0.35143595933914185 - accuracy init-unsafe: 50.0 - accuracy belt: 0 - points in belt: 0
100 - loss: -3.5243349075317383 - accuracy init-unsafe: 100.0 - accuracy belt: 61.71617161716171 - points in belt: 303
200 - loss: -3.51829195022583 - accuracy init-unsafe: 100.0 - accuracy belt: 61.07382550335571 - points in belt: 298
300 - loss: -3.5757029056549072 - accuracy init-unsafe: 100.0 - accuracy belt: 61.07382550335571 - points in belt: 298
400 - loss: -3.5718491077423096 - accuracy init-unsafe: 99.9 - accuracy belt: 60.94276094276094 - points in belt: 297
500 - loss: -3.5985488891601562 - accuracy init-unsafe: 100.0 - accuracy belt: 61.07382550335571 - points in belt: 298
600 - loss: -3.629819393157959 - accuracy init-unsafe: 100.0 - accuracy belt: 61.461794019933556 - points in belt: 301
700 - loss: -3.[...]<jupyter_text>Barrier 2$$\begin{cases}\dot{x} = e^{-x} + y - 1 \\\dot{y} = - \sin^2 x\end{cases}$$$$\begin{align*}& X = \{-2 \leq x, y  \leq 2 \} \\ & X_0 = \{(x+0.5)^2+(y - 0.5)^2 \leq 0.16 \} \\ & X_u  = \{ (x - 0.7)^2+(y+0.7)^2 \leq 0.09 \}\end{align*}$$<jupyter_code>torch.manual_seed(167)
dynamics = barr_2
dimension = 2
activations =  [ActivationType.SOFTPLUS]
neurons = [20] 
verifier_type = VerifierType.DREAL

parameters = {CegisConfig.VERIFIER.k:verifier_type,CegisConfig.ACTIVATION.k: activations,
              CegisConfig.N_VARS.k: dimension,
              CegisConfig.N_HIDDEN_NEURONS.k:neurons, CegisConfig.SP_HANDLE.k:False, 
              CegisConfig.SP_SIMPLIFY.k:False, CegisConfig.SYMMETRIC_BELT.k: False}

mode = PrimerMode.BARRIER
f_n, f_s = synthesise(dynamics, mode, CEGIS_PARAMETERS=parameters)

x = np.array([initialise_states(2)]).reshape(-1,1)
plot_exponential_bench(x, f_s)<jupyter_output>================================================================================
  learner   0
================================================================================
0 - loss: -0.2198912501335144 - accuracy init-unsafe: 50.0 - accuracy belt: 91.53225806451613 - points in belt: 496
100 - loss: -5.212582111358643 - accuracy init-unsafe: 100.0 - accuracy belt: 88.03191489361703 - points in belt: 376
200 - loss: -4.903604507446289 - accuracy init-unsafe: 99.9 - accuracy belt: 82.86445012787723 - points in belt: 391
300 - loss: -5.296963214874268 - accuracy init-unsafe: 98.1 - accuracy belt: 88.93709327548807 - points in belt: 461
400 - loss: -5.770838260650635 - accuracy init-unsafe: 99.6 - accuracy belt: 97.73299748110831 - points in belt: 397
500 - loss: -5.895694255828857 - accuracy init-unsafe: 100.0 - accuracy belt: 98.48484848484848 - points in belt: 396
600 - loss: -5.845238208770752 - accuracy init-unsafe: 100.0 - accuracy belt: 97.98994974874371 - points in belt: 398
700[...]<jupyter_text>Barrier 3$$ \begin{cases} \dot{x} = y  \\ \dot{y} = -x - y + \frac{1}{3} x^3 \end{cases}$$$$\begin{align*}& X = \{ -3.5 \leq x \leq 2,-2 \leq y \leq 1 \} \\& X_0 = \{ (x-1.5)^2+y^2 \leq 0.25 \vee (x \geq -1.8 \wedge x \leq -1.2 \wedge y \geq -0.1 \wedge y \leq 0.1) \\& \qquad\qquad \vee  (x \geq -1.4 \wedge x \leq -1.2 \wedge y\geq -0.5\wedge y \leq 0.1) \} \\& X_u = \{ (x+1)^2+(y+1)^2 \leq 0.16 \vee(x\geq 0.4 \wedge x\leq 0.6 \wedge y \geq 0.1 \wedge y\leq 0.5) \\& \qquad\qquad \vee (x \geq 0.4 \wedge x \leq 0.8 \wedge y \geq 0.1 \wedge y \leq 0.3) \}\end{align*}$$<jupyter_code>torch.manual_seed(167)
dynamics = barr_3

dimension = 2
activations =  [ActivationType.SIGMOID, ActivationType.SIGMOID]
neurons = [20, 20] 
verifier_type = VerifierType.DREAL

parameters = {CegisConfig.VERIFIER.k:verifier_type,CegisConfig.ACTIVATION.k: activations, 
              CegisConfig.N_VARS.k: dimension,
              CegisConfig.N_HIDDEN_NEURONS.k:neurons, CegisConfig.SYMMETRIC_BELT.k:False,
              CegisConfig.SP_HANDLE.k:False, CegisConfig.SP_SIMPLIFY.k:False}

mode = PrimerMode.BARRIER
f_n, f_s = synthesise(dynamics, mode, CEGIS_PARAMETERS=parameters)

x = np.array([initialise_states(2)]).reshape(-1,1)
plot_pjmod_bench(x, f_s)<jupyter_output>================================================================================
  learner   0
================================================================================
0 - loss: 0.23090709745883942 - accuracy init-unsafe: 50.0 - accuracy belt: 0 - points in belt: 0
100 - loss: 0.06377644836902618 - accuracy init-unsafe: 68.20866141732283 - accuracy belt: 15.625 - points in belt: 288
200 - loss: -3.4263501167297363 - accuracy init-unsafe: 63.48425196850393 - accuracy belt: 65.21739130434783 - points in belt: 368
300 - loss: -5.2791361808776855 - accuracy init-unsafe: 89.76377952755905 - accuracy belt: 97.61092150170649 - points in belt: 293
400 - loss: -5.944088459014893 - accuracy init-unsafe: 99.70472440944881 - accuracy belt: 100.0 - points in belt: 312
500 - loss: -5.975905895233154 - accuracy init-unsafe: 99.80314960629921 - accuracy belt: 100.0 - points in belt: 309
600 - loss: -5.908348083496094 - accuracy init-unsafe: 99.50787401574803 - accuracy belt: 98.72204472843451 [...]<jupyter_text>Barrier 4$$\begin{cases}    \dot{x} = v \sin \varphi, \\    \dot{y} = v \cos \varphi, \\    \dot{\varphi} = u, \quad \textrm{ where } \quad u = - \sin \varphi + 3 \cdot \frac{x \sin \varphi + y \cos \varphi}{0.5 + x^2 + y^2},    \end{cases}$$,    $$\begin{align*}    & X = \{ -2 \leq x,y \leq 2,-\frac{\pi}{2}< \varphi < \frac{\pi}{2} \}, \\    & X_0 = \{ -0.1 \leq x \leq 0.1, - 2 \leq y \leq -1.8,-\frac{\pi}{6}< \varphi< \frac{\pi}{6} \}, \\    & X_u = \{ x^2+ y^2  \leq 0.04 \},    \end{align*}$$,<jupyter_code>torch.manual_seed(167)
dynamics = obstacle_avoidance

dimension = 3
activations =  [ActivationType.LIN_TO_CUBIC]
neurons = [5] 
verifier_type = VerifierType.DREAL

parameters = {CegisConfig.VERIFIER.k:verifier_type,CegisConfig.ACTIVATION.k: activations, 
              CegisConfig.N_VARS.k: dimension,
              CegisConfig.N_HIDDEN_NEURONS.k:neurons,
              CegisConfig.SP_HANDLE.k:False, CegisConfig.SP_SIMPLIFY.k:False, CegisConfig.BATCH_SIZE.k:2000}

mode = PrimerMode.BARRIER
f_n, f_s = synthesise(dynamics, mode, CEGIS_PARAMETERS=parameters)<jupyter_output>================================================================================
  learner   0
================================================================================
0 - loss: -0.24276743829250336 - accuracy init-unsafe: 96.25 - accuracy belt: 38.91304347826087 - points in belt: 460
100 - loss: -3.008453369140625 - accuracy init-unsafe: 99.675 - accuracy belt: 50.847457627118644 - points in belt: 472
200 - loss: -3.925248384475708 - accuracy init-unsafe: 100.0 - accuracy belt: 65.50387596899225 - points in belt: 516
300 - loss: -5.763478755950928 - accuracy init-unsafe: 100.0 - accuracy belt: 96.1767204757859 - points in belt: 1177
400 - loss: -5.796407699584961 - accuracy init-unsafe: 99.55 - accuracy belt: 97.28155339805825 - points in belt: 1030
================================================================================
  translator   0
================================================================================
Candidate: ( - 3.775 * (-3.5510001182556152 - 1.4459[...]<jupyter_text>Hybrid Barrier$$f_1 = \begin{cases}\dot{x} = y \newline\dot{y} = - x - 0.5 x^3 \newline\end{cases}\qquadf_2 = \begin{cases}\dot{x} = y \newline\dot{y} =  x - 0.25 y^2 \newline\end{cases}$$$$ \text{Domain for } f_1 = \{ (x,y): x < 0 \} \qquad \text{Domain for } f_2 = \{ (x,y): x\geq 0 \}$$$$\begin{align*}& X = \{ x^2 + y^2 \leq 4 \} \\ & X_0 = \{ (x+1)^2 + (y+1)^2 \leq 0.25 \} \\ & X_u = \{ (x-1)^2 + (y-1)^2 \leq 0.25 \}\end{align*}$$<jupyter_code>torch.manual_seed(167)

dynamics = twod_hybrid
dimension = 2
activations =  [ActivationType.LIN_SQUARE]
neurons = [3] 
verifier_type = VerifierType.Z3

parameters = {CegisConfig.VERIFIER.k:verifier_type,CegisConfig.ACTIVATION.k: activations, 
              CegisConfig.N_VARS.k: dimension,
              CegisConfig.N_HIDDEN_NEURONS.k:neurons, CegisConfig.SYMMETRIC_BELT.k:False, 
              CegisConfig.SP_HANDLE.k:False, CegisConfig.SP_SIMPLIFY.k:False}

mode = PrimerMode.BARRIER
f_n, f_s = synthesise(dynamics, mode, CEGIS_PARAMETERS=parameters)<jupyter_output>================================================================================
  learner   0
================================================================================
0 - loss: 0.07103800028562546 - accuracy init-unsafe: 29.3 - accuracy belt: 7.643312101910828 - points in belt: 314
100 - loss: -5.815310478210449 - accuracy init-unsafe: 100.0 - accuracy belt: 99.41520467836257 - points in belt: 342
200 - loss: -5.8463945388793945 - accuracy init-unsafe: 100.0 - accuracy belt: 99.69788519637463 - points in belt: 331
300 - loss: -5.857110500335693 - accuracy init-unsafe: 100.0 - accuracy belt: 99.6951219512195 - points in belt: 328
400 - loss: -5.858522891998291 - accuracy init-unsafe: 100.0 - accuracy belt: 99.6845425867508 - points in belt: 317
================================================================================
  translator   0
================================================================================
Candidate: (-10115000009536743/5000000000000000*
 (-219999[...]<jupyter_text>Hi-Ord 4$$\begin{align}& 2273 x^{(4)} + 3980 x^{(3)} + 4180 x^{(2)} + 2400 x^{(1)} + 576 = 0, \end{align}$$where $ x^i $ represents the $i^{th}$ derivative of $x$.<jupyter_code>torch.manual_seed(167)

dynamics = hi_ord_4
dimension = 4
activations =  [ActivationType.LINEAR]
neurons = [20] 
verifier_type = VerifierType.DREAL

parameters = {CegisConfig.VERIFIER.k:verifier_type,CegisConfig.ACTIVATION.k: activations, 
              CegisConfig.N_VARS.k: dimension, CegisConfig.BATCH_SIZE.k: 1000,
              CegisConfig.N_HIDDEN_NEURONS.k:neurons, CegisConfig.SYMMETRIC_BELT.k:False, 
              CegisConfig.SP_HANDLE.k:True, CegisConfig.SP_SIMPLIFY.k:True, CegisConfig.ROUNDING.k: 2}

mode = PrimerMode.BARRIER
f_n, f_s = synthesise(dynamics, mode, CEGIS_PARAMETERS=parameters)<jupyter_output>================================================================================
  learner   0
================================================================================
0 - loss: -3.373413324356079 - accuracy init-unsafe: 98.05 - accuracy belt: 56.22568093385214 - points in belt: 514
100 - loss: -5.212804317474365 - accuracy init-unsafe: 100.0 - accuracy belt: 86.86006825938567 - points in belt: 586
200 - loss: -5.214147567749023 - accuracy init-unsafe: 100.0 - accuracy belt: 86.88245315161839 - points in belt: 587
300 - loss: -5.212803840637207 - accuracy init-unsafe: 100.0 - accuracy belt: 86.86006825938567 - points in belt: 586
400 - loss: -5.238133430480957 - accuracy init-unsafe: 100.0 - accuracy belt: 87.28222996515679 - points in belt: 574
500 - loss: -5.317925930023193 - accuracy init-unsafe: 100.0 - accuracy belt: 88.61209964412811 - points in belt: 562
600 - loss: -5.363837718963623 - accuracy init-unsafe: 100.0 - accuracy belt: 89.37728937728937 - points in belt: 546
[...]<jupyter_text>Hi-Ord 6$$\begin{align}& 170 x^{(6)} + 800 x^{(5)} + 2273 x^{(4)} + 3980 x^{(3)} \\ \nonumber& + 4180 x^{(2)} + 2400 x^{(1)} + 576 = 0, \end{align}$$where $ x^i $ represents the $i^{th}$ derivative of $x$.<jupyter_code>torch.manual_seed(167)

dynamics = hi_ord_6
dimension = 6
activations =  [ActivationType.LINEAR]
neurons = [10] 
verifier_type = VerifierType.DREAL

parameters = {CegisConfig.VERIFIER.k:verifier_type,   CegisConfig.ACTIVATION.k: activations, 
              CegisConfig.N_VARS.k: dimension,        CegisConfig.BATCH_SIZE.k: 1000,
              CegisConfig.N_HIDDEN_NEURONS.k:neurons, CegisConfig.SYMMETRIC_BELT.k:False, 
              CegisConfig.SP_HANDLE.k:True,           CegisConfig.SP_SIMPLIFY.k:True, 
              CegisConfig.ROUNDING.k: 2}

mode = PrimerMode.BARRIER
f_n, f_s = synthesise(dynamics, mode, CEGIS_PARAMETERS=parameters)<jupyter_output>================================================================================
  learner   0
================================================================================
0 - loss: -3.8546576499938965 - accuracy init-unsafe: 100.0 - accuracy belt: 64.27525622254758 - points in belt: 683
100 - loss: -5.8685221672058105 - accuracy init-unsafe: 100.0 - accuracy belt: 97.78869778869779 - points in belt: 407
200 - loss: -5.8685221672058105 - accuracy init-unsafe: 100.0 - accuracy belt: 97.78869778869779 - points in belt: 407
300 - loss: -5.8685221672058105 - accuracy init-unsafe: 100.0 - accuracy belt: 97.78869778869779 - points in belt: 407
400 - loss: -5.869493007659912 - accuracy init-unsafe: 100.0 - accuracy belt: 97.8048780487805 - points in belt: 410
500 - loss: -5.855214595794678 - accuracy init-unsafe: 100.0 - accuracy belt: 97.5669099756691 - points in belt: 411
600 - loss: -5.8562726974487305 - accuracy init-unsafe: 100.0 - accuracy belt: 97.58454106280193 - points in belt: 4[...]<jupyter_text>Hi-Ord 8\begin{align}	& x^{(8)} + 20 x^{(7)} + 170 x^{(6)} + 800 x^{(5)} + 2273 x^{(4)} 	\\ \nonumber 	& \qquad + 3980 x^{(3)} + 4180 x^{(2)} + 2400 x^{(1)} + 576 = 0, \end{align}where $ x^i $ represents the $i^{th}$ derivative of $x$.<jupyter_code>torch.manual_seed(167)

dynamics = hi_ord_8
dimension = 8
activations =  [ActivationType.LINEAR]
neurons = [10] 
verifier_type = VerifierType.DREAL

parameters = {CegisConfig.VERIFIER.k:verifier_type,CegisConfig.ACTIVATION.k: activations, 
              CegisConfig.N_VARS.k: dimension, CegisConfig.BATCH_SIZE.k: 1000, 
              CegisConfig.N_HIDDEN_NEURONS.k:neurons, CegisConfig.SYMMETRIC_BELT.k:False, 
              CegisConfig.SP_HANDLE.k:True, CegisConfig.SP_SIMPLIFY.k:True, CegisConfig.ROUNDING.k: 2}

mode = PrimerMode.BARRIER
f_n, f_s = synthesise(dynamics, mode, CEGIS_PARAMETERS=parameters)<jupyter_output>================================================================================
  learner   0
================================================================================
0 - loss: -2.765930652618408 - accuracy init-unsafe: 0.0 - accuracy belt: 54.936708860759495 - points in belt: 790
100 - loss: -5.620918273925781 - accuracy init-unsafe: 100.0 - accuracy belt: 93.66197183098592 - points in belt: 142
200 - loss: -5.62357759475708 - accuracy init-unsafe: 100.0 - accuracy belt: 93.7062937062937 - points in belt: 143
300 - loss: -5.6313371658325195 - accuracy init-unsafe: 100.0 - accuracy belt: 93.83561643835617 - points in belt: 146
400 - loss: -5.638783931732178 - accuracy init-unsafe: 100.0 - accuracy belt: 93.95973154362416 - points in belt: 149
500 - loss: -5.559482097625732 - accuracy init-unsafe: 100.0 - accuracy belt: 92.63803680981596 - points in belt: 163
600 - loss: -5.623841285705566 - accuracy init-unsafe: 100.0 - accuracy belt: 93.71069182389937 - points in belt: 159
70[...]
{'fraction_non_alphanumeric': 0.32230276926810036, 'fraction_numerical': 0.13224544268858623, 'mean_word_length': 4.704152249134948, 'pattern_counts': {'":': 0, '<': 67, '<?xml version=': 0, '>': 62, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 11, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '18', 'dir': 'jupyter-structured-clean-dedup', 'id': '300916', 'license': 'BSD-3-Clause', 'n_tokens_mistral': 14200, 'n_tokens_neox': 11072, 'n_words': 2177, 'path': 'experiments/FOSSIL-benchmarks.ipynb', 'repo_name': 'oxford-oxcav/fossil', 'size': '33008'}