Generalize .spec to allow optimization over stability radii

[fbrausse]

The current .spec is a list of per-feature annotations (see doc/spec for details):

• label: (used for variable naming as well as for feature names in the dataset when training / preparing)
• data type (called range there): int, float or explicit list of categorical values
• purpose (called type there): knob, input, response
• non-response vars:
  • stability radius: rad-abs or rad-rel, each with a numeric constant
  • optional list of safe values ("the grid")
  • optional default value (unused by the solver, as of now)

Example for the Timing variable:

{ "label": "Timing","type": "knob","range": "int","rad-abs": 0 }

This format is too restrictive for the optimization we decided to employ for Shai: Include a new knob variable labelled trad in the formula, of type int which is used to specify the rad-abs around the original Timing variable. trad does not need any particular stability radius, so we can just require a counter-example's trad to be the same as the candidate's. This is possible in our FMCAD formulation by a specific \theta(a,b): a.trad = b.trad /\ -a.trad <= a.Timing - b.Timing < a.trad. It is not possible in the current .spec format, for two reasons:

1. All variables are assumed to be features of the training dataset as well as the network.
2. There is is no way to refer to other parts of the solution in rad-abs or rad-rel.

In any case, item 1. above is not easy to change and my suggestion is to move to a new .spec version, which might look something like this:

{
  "version": 2,

  # same list as .spec before, except for `rad-abs: 0` in `Timing`
  "network": [{ "label": "Timing","type": "knob","range": "int" }, ...],

  # additional variables to be quantified over, not part of the NN's domain
  "add-vars": [{ "label": "trad", "type": "knob", "range": "int"}],

  # nested lists, interpreted as CNF obtained by interpreting the strings
  # as Python expressions in some predefined namespace (here, including all
  # variable names as well as "rad_abs"
  "add-constraints": [[ "0 <= trad" ], [ "rad_abs(Timing, trad)" ]]
}

There are at least two options to solve item 2. above:

1. allow the .spec to give arbitrary predicates \theta and fail if they cannot be encoded to at least our fallback solver Z3
2. allow a new format to refer to other variables in the rad-abs/rad-rel part, e.g., use rad-abs: "trad" for Timing

[fbrausse]

In the light of #3, another option is to get rid of the .spec entirely and let the v2-API user-code construct an equivalent of it when interacting with the server's API. That would be the approach I'd most likely chose until we come up with an alternative .spec format that would also include multiple networks to specify objectives, etc.

[fbrausse]

[...] get rid of the .spec entirely and let the v2-API user-code construct an equivalent of it when interacting with the server's API [...] until we come up with an alternative .spec format that would also include multiple networks to specify objectives, etc.

During today's meeting this was agreed upon. In addition, @konstantin-korovin suggested to rename "network" in the .spec version 2.

[fbrausse]

Clarification: trad (restricting the Timing input to the NN) is not part of the neural network's inputs (or outputs), but a separate variable, constraints over which are constructed in the final optimization formula. These additional constraints are specified in "add-constraints" above.

[fbrausse]

KK: split "network" into input-features and output-features.

"add-vars" specifies variables that can be used in additional constraints and the objective functions
Example: \exists Timing, ..., delta, trad \forall Timing', ..., delta', trad'. [..]
where trad is the additional variable, which also can be maximised over.

[fbrausse]

"objectives": [ "max(trad)", "max(delta)" ]
in contrast to what we did for Shai earlier:
"objectives": [ "max(shai_obj(trad, delta))" ]
These objectives could also look like ite(delta < trad, delta + trad*trad, trad). The concrete namespace for these expressions need to be documented.