Support for strict inequalities?

[MatthewDaggitt]

Current the Marabou property format seems to support =/<=/>= (see my comment in #490). However it does not support any of != /</>. While I recognise that at first glance the difference between <= and < is pretty small when you're working over the real numbers, it's causing me some significant ergonomic issues while trying to connect Marabou to interactive theorem provers like Agda.

How difficult would it be to add support for < and >?

Motivation

(Note that I use high-level descriptions of the properties I'm trying to prove below, not Marabou's property input format)

As a bit of motivation I'm trying to replicate the verification of classic Boyer-Green-Moore controller with the deltaV component replaced with a neural network. If I can prove in Marabou that the neural network deltaV obeys the property:

(1)   forall x . | currentPosition x | <= 3    =>   | deltaV x + (2 * currentPosition x) - prevPosition x | <= 2

then I can prove in Agda that the controller is always safe:

(2) forall wind . | wind | <= 1   =>   finalPosition wind x  <= 3

The problem is that when I translate (1) to Marabou, I need to transform it into an existential by negating the whole thing which turns it into:

exists x . | currentPosition x | < 3    and   | deltaV x + (2 * currentPosition x) - prevPosition x | > 2

which isn't supported by Marabou because of the strict inequalities.

The only solution I can see is to use strict inequalities in the original property:

(1')   forall x . | currentPosition x | < 3    =>   | deltaV x + (2 * currentPosition x) - prevPosition x | < 2

however logically (1') is now a very different statement than (1) and it makes proving a variant of (2) far far more complicated.

[MatthewDaggitt]

Hmm actually the absence of a strict inequality is far worse than I'd thought, it actually makes it impossible to translate the modulus operator into a marabou query!

Take the definition of the modulus operator | a | = if a R 0 then a else - a where R is either >= or > and consider translating the high-level property | f x | <= 2 for some network f and input x into a set of marabou queries:

| f x | <= 2                                                   <=> (1)
(if x R 0 then x else - x) <= 2                                <=> (2)
(if x R 0 then x <= 2 else - x <= 2)                           <=> (3)
(f x R 0 and f x <= 2) or (not (f x R 0) and - f x <= 2)           (4)

which translates into the two marabou queries:

+y0 R 0
+y0 <= 2

and

+y0 (not R) 0
-y0 <= 2

As one can see, no matter what your choice of R, then one of the two queries is going to contain a strict inequality!

[AleksandarZeljic]

Hi @MatthewDaggitt, there are few things to consider here:

• Marabou does not use negation, therefore expressing strict inequalities is not possible like you observed.
• Marabou's semantics is based on floating-point computation, rather than reals, which means that there is a smallest increment between two adjacent numbers (which depends on the value of the exponent). This increment is called unit in last place (or ulp in short). You can use this smallest increment to define a strict inequality in your encoding of the problem from Agda to Marabou. In practice you probably want to specify this threshold to be a fixed value for all computation and you can choose the value based on the precision of the other components in the system you are modelling.
• Finally, Marabou allows specification of that precision threshold for all of its floating-point computation. So integrating a threshold of choice on Marabou's end is not an issue.

Hope this clarifies the situation a bit.

[MatthewDaggitt]

Hi @AleksandarZeljic, thanks for your thorough reply. I've just returned to this and have a few more questions:

Marabou allows specification of that precision threshold for all of its floating-point computation

How does one do that? What's the default value? I can't see any likely looking option when looking at --help.

If Marabou already knows what the precision threshold is, would it make sense to add support for strict inequalities on Marabou's end? The InputQueryParser could simply translate x < y to x <= y - ulp.

[AleksandarZeljic]

For performance reasons, the precision parameter is specified at compilation time and is specified in GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISON.

Regarding implementation in Marabou, I think that such choices need to be explicitly left to the user, since any chosen semantics might not be what the user intuitively expects/needs. I will bring it up with the team and see what their thoughts are.

[MatthewDaggitt]

For performance reasons, the precision parameter is specified at compilation time and is specified in GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISON.

Ah that makes sense, thanks!

Regarding implementation in Marabou, I think that such choices need to be explicitly left to the user, since any chosen semantics might not be what the user intuitively expects/needs. I will bring it up with the team and see what their thoughts are.

Hmm, okay so in our situation we're writing a compiler that allows users to write high-level specifications which then, amongst other things, get compiled down to Marabou queries. See, for example, the complete ACAS Xu spec in our language.

However the upshot of this is that we're not the end user and therefore we probably won't be the one who has installed Marabou so at the moment have no idea what epsilon has been set to. So as far as I see it there are two options:

1. Have Marabou implement strict inequalities natively as described above. I see your point about this not necessarily matching the user's semantics if the value of epsilon is not consistent with the implementation of floating point numbers they're using. But doesn't Marabou already have that problem? If the user ignores the epsilon parameter and doesn't set it appropriately then Marabou will give the wrong answers regardless of whether it supports strict inequalities in the manner suggested above. For example I had no idea about the epsilon parameter until you mentioned it just now, which may mean the results Marabou have given me are suspect.

   I think the real solution is to try and make the user pick the right epsilon value for Marabou by either a) improving the documentation about the epsilon, or b) forcing the user to specifically provide a value at compile time. If epsilon is correctly set by the user, then the translation of strict inequalities above is sound right?

2. Add the ability to ask Marabou what its current epsilon is. If my suggestion above is not adopted, then we'll need to get this value from Marabou programatically. Best option would probably be via a command line argument --comparison-epsilon, or something similar, which would simply print out its value.

Interested to see what the Marabou team thinks about this. More than happy to provide further information about our use case if needed or join discussions if that would be helpful.

[idan0610]

This issue has most likely become stale and is being closed. If you think this issue is still relevant, please open a new issue.

[MatthewDaggitt]

Nope, has not become stale, very much still a problem. I'm reopening.

[idan0610]

Oh sorry about that, my bad