Right now, we create a single expression for a neural network; which has many duplicates. The downside is a (possibly exponential) blow-up on the size of the expression.

As a solution, let's Introduce intermediate variables for each neuron of the network. this will drastically decrease the size of expressions, and improve solver efficiency.

At the moment, learning is the most time-consuming phase of the CEGIS loop. Using a GPU during training should be able to reduce this time.

As we have access to GPUs with CUDA support, the goal will be to train models on a GPU (when possible).

The following need to be fixed:

• Model combination C should no longer be used. Change everything to V instead.
• There is no longer C_tgt and C_dec. We have a single sample set S.
• Change the verifier to use DReal; this is what should be done, so the general case can be handled.

Look at chapter 5 of the following book by Aws Albarghouthi: https://arxiv.org/abs/2109.10317.

There, a formalized method of translating NNs into SMT constraints is presented. This method also introduces ways for encoding nonlinear activation functions.

We can consider using this method in our symbolic translators.

The current encoding of combining A, B, and V cannot exploit Marabou at all! This is due to the fact that the abstract interpreter is effectively turned off.

There is a new method for combining A, B, and V so that the resulting NN will look like a normal NN (with well-formed layers and activation functions). We need to switch to this encoding to use Marabou effectively.

• Get more symbolic functions to return in the (output, constraints) format.