search

oxford-oxcav / fossil

BSD 3-Clause "New" or "Revised" License
16 stars 5 forks source link

ROA Lyapunov Constraints #4

Open af-a opened 9 months ago

af-a commented 9 months ago

Hello.

We have been exploring the FOSSIL framework and we had a question regarding the symbolic representation of the ROA certificate's constraints that is defined in this get_constraints function in certificate.py.

While using this certificate, we noticed that the verifier component returns counter-examples that are outside and very far away from our small domain set. It seems like the symbolic expression within that function might be checking the constraints for samples anywhere in the state space and not only in the domain set, as is done for example here in the corresponding function of the Lyapunov class.

We wanted to know whether this is the intended behaviour for the ROA certificate or if it is supposed to apply the same constraint.

Many thanks in advance!

AndreaPuffo commented 8 months ago

Hi,

thanks for writing us! Short answer: unfortunately, this is expected behaviour.

The ROA certificate checks that the domain entirely lies within a level set of V. If V has level sets particularly elliptical, they can stretch very far away from the domain of interest. One way to mitigate this issue could be by adding an additional loss term, to incentivise a more 'round' shape of the level sets. This translates in asking to have a paraboloid-shaped V, so you may add a loss term like V - ||x||2, which pushes the V to be more similar to ||x||2, which has circular level sets. Naturally, this is a soft constraint, hence no guarantee of success; further, adding an extra loss term may impair the training convergence.

A final note: if the counterexamples are something in order of 1e308 -- or any other crazy high number -- this is dReal reaching its limits. For particularly nasty formulae (e.g. a whole bunch of tanh(tanh( ...)) ), I think dReal simply gives up. I am pretty sure there exists a paper (one of the original works on dReal) mentioning this, but I could not find it. If this is the case, you can just add a max_bound constraint to the verification. We have such kind of fail-safe in place, here, for 1e300. You might try to decrease that number; after all, for physical systems, it is pretty difficult to reach any value close to those bounds.

Hope this helps. In case you have more questions, feel free to drop us an email, we are happy to chat.