dReal4 check the Lyapunov stability out of the basin of interest

[kimukook]

Hi all, I am trying to use dReal4 to check the requirements of Lyapunov stability. The Lyapunov function is generated by a Neural network. The region where I would like dReal4 to check for Lyapunov stability is 0.5<=||x||_2<=1.5. However, dReal4 found the invalid box region that is inside ||x||_2<=0.5. I appreciate any feedback on how to modify this. Thank you for your help!

The code I am using is appended below:

x1 = dreal.Variable("x1")
x2 = dreal.Variable("x2")
vars_ = [x1, x2]

config = dreal.Config()
config.use_polytope_in_forall = True
config.use_local_optimization = True
config.precision = 1e-2
epsilon = 0
# Checking candidate V within a ball around the origin (ball_lb ≤ sqrt(∑xᵢ²) ≤ ball_ub)
ball_lb = 0.5
ball_ub = 1

result = CheckLyapunov(vars_, f, V_learn, ball_lb, ball_ub, config, epsilon)

[scungao]

Is the violation example close to ||x||=0.5? The numerical relaxation can soften the constraints. Try strengthening the inequalities like setting ball_lb to 0.6 or something.

[kimukook]

Is the violation example close to ||x||=0.5? The numerical relaxation can soften the constraints. Try strengthening the inequalities like setting ball_lb to 0.6 or something.

Dear prof. Gao,

Thank you so much for your info! I found points violating the constraints at [0.2185, 0.4662] which is somehow close to the lower bound 0.5. I will increase the lower bound and test it again.

It might be not appropriate to mention here, but I am also interested in generating Lyapunov function for a highly nonlinear system using neural network. (Apologize first if I bring this up in an improper situation.) I found two layers structure could not find a valid Lyapunov function in 2000 training iterations. I am trying up to 5 layers( 4 hidden layers + 1 output layer) with tanh as the activation function, still couldn't a valid one. I really appreciate any suggestion on this. Thank you so much again for your help!

[scungao]

email me and we can discuss