When the tools in I4: Incremental inference of inductive invariants for verification of distributed protocols and On Symmetry and Quantification: A New Approach to Verify Distributed Protocols search for an inductive invariant of a distributed system, the search procedure instantiates a series of small finite models and tries to infer from their truth tables a series of logical formulae that hold over those finite models. These formulae are found by running the Quine-McCluskey algorithm for minimization of Boolean functions. The prime implicants found by Quine-McCluskey have a latent symmetry that can be abstracted into quantified formulae. There are only so many small numbers, and so small finite models may propose formulae that do not hold at larger sizes. However, if you find a formula that holds at size $𝑛$ as well as size $𝑛+1$, then it is likely a good candidate to hold at all sizes. You need to be a little careful if your protocol is indexed by several variables, but mostly this general idea holds when abstracting to a protocol of unbounded size. Further discussion of this idea can be found in SAT-based quantified symmetric minimization of the reachable states of distributed protocols: An update.

My observation was that Quine-McCluskey is just a special instance of Buchberger’s algorithm for computing Gröbner Bases. That is, you can describe Boolean formulae as polynomials over the field with two elements, and in this translation Quine-McCluskey and Buchberger each compute the same data. This observation isn’t new in and of itself, but it does open up an opportunity to generalize the invariant search procedure that is used above.

The place I went looking to apply this idea was in the search of polynomial loop invariants. If a loop had an invariant that is expressible as a polynomial relation between the program variables, then you could apply the same idea as above to infer the loop invariant.

Suppose ${𝑥}_1,\dots ,{𝑥}_{𝑛}$ are the variables in scope of program $𝑆$ and $𝑆$ contains a loop that we want to infer an invariant for. Denote the value of ${𝑥}_{𝑖}$ at the $𝑗$-th loop iteration by ${𝑥}_{𝑖,𝑗}$. The invariant search procedure proceeds intuitively as the following: we will keep track of the minimal set of polynomials that could interpolate between all of the variable assignments that we have witnessed thus far. Formally this is kept track of by the ideal of polynomials. At the $𝑗$-th loop iteration we add a new generator to the ideal which corresponds to the assignments ${𝑥}_{1,𝑗},\dots ,{𝑥}_{𝑛,𝑗}$. The Gröbner basis for this ideal provides the minimal data needed to generate all the assignments witnessed thus far, so if this process saturates then the Gröbner basis encodes a polynomial loop invariant. The nice thing about polynomials is that they have finite degree which guarantees that this process does indeed saturate (provided that the degree of the invariant is smaller than the number of loop iterations).

I was so excited to find this idea. I’d felt like it was my first good idea in grad school. Then I read Automatic Generation of Polynomial Loop Invariants: Algebraic Foundations and found out someone had done this 20 years ago. I still wonder from time to time if there is room to further refine this idea or perhaps further generalize it. For instance, there is further generalization beyond Quine-McCluskey or Buchberger to the Knuth-Bendix algorithm, which seems to be a more general instance of both of these algorithms. So perhaps this search procedure can be weakened to an even more general class? Although, I’m not yet familiar much with the Knuth-Bendix algorithm.

My understanding for how one may prove a safety property $𝑃$ for a neural network $𝑁$ is as follows. First, express $𝑃$ as an input-output property. That is, choose some region $𝐷$ in the domain of $𝑁$ to represent the inputs of interest. Further choose some region $𝐴$ in the codomain of $𝑁$ to describe safe outputs. Then describe $𝑃$ as the property:

For instance, this is more or less how Reluplex, Marabou, and $𝛼𝛽$-CROWN each work. Squinting my eyes, this is the only such method for verifying a safety property for $𝑁$. That is, this is the only way to get a 100% guarantee that $𝑃$ holds rather than some high measure of confidence.

I believe in this formalism I have an idea for how to express the property “$𝑁$ is translationally invariant” where $𝑁$ is an image classifying net.

To this end, we need a continuous artifact that captures what it means to translate an image. We can express an image as a matrix of pixels $𝐼$ (or perhaps several parallel matrices if we care about color channels, but stick to a single grayscale matrix for now). To shift $𝐼$ over by a single pixel, we may left-multiply $𝐼$ by the shift matrix $𝑆$, where $𝑆$ is the matrix filled with zeros and has 1′s on the subdiagonal. Note that all the directions of shifting $𝐼$ are captured by the combinations of left/right multiplication by $𝑆$, ${𝑆}^{𝑇}$.

Shifting by multiple pixels is now expressed by the matrix ${𝑆}^{𝑛}𝐼$, however this is still a discrete dynamical system. We don’t have a continuous object by which we can test our safety property. My initial thought to continuousify this system was to express some sort of exponential flow by $𝑆$. That is, consider the matrix

${𝑆}^{𝑡}𝐼$ then captures what it means to translate the image $𝐼$ over by $𝑡$, a real-valued “amount of shifting”. This choice of continuous artifact could then be used for a verification effort, however there are some issues related to numerical stability because $𝑆$ isn’t invertible. Because it is not invertible, $\text{𝗅𝗈𝗀}(𝑆)$ doesn’t actually exist. So to make the above construction work, we need to mildly perturb $𝑆$ and take a pseudoinverse. This sort of works and makes it so ${𝑆}^{𝑡}𝐼$ does capture some real valued shift, but it is only accurate when $𝑡$ is small. So this is maybe problematic for our verification effort. This may be resolvable by chopping up the problem into subproblems, each of which is thin enough for the current iteration is accurate enough on that subproblem. However, there are two big things to consider.

1. The exponential approach above is probably too complicated. It seems

likely that you may be able to take some (sequence of) linear interpolation(s) between the ${𝑆}^{𝑛}𝐼$’s. This will still be some continuous object that captures a real-valued shift and it will be much more stable than the approach above.

1. Even if we sort out which continuous object represents translation

of an image, I cannot for the life of me train any neural network that is translationally invariant. So the proof method is useless if there is nothing that it would ever apply to.

Precisely in this last point, I have mostly focused on trying to train a small CNN for MNIST handwritten digit classification that preserves the output class for small, reasonable translations of the digit. I’ve used data augmentation to predispose the network to being translationally invariant, and even though I can get a high degree of invariance, I cannot get a network that is invariant for all of the examples even in the training set or a reserved testing set.

It may be the case that the method I propose for measuring this invariance could be used to adversarially train a network to have better invariance. It may also be the case that all CNNs are bound to suffer from small degrees of translational sensitivity. I cannot find the citation at the moment, but there was a paper that suggested that CNNs suffer from weird issues of translational sensitivity that relate to the size of the convolutional window. So maybe this approach is doomed to fail anyway.

On the whole, I will say that machine learning verification almost sounds like an oxymoron. That is, if you have the expressivity to properly state a sophisticated safety property, then you likely understand the problem enough to not need to resort to machine learning in the first place. So almost tautologically, it seems that there cannot be satisfying verification of neural nets, as the tasks of machine learning and verification live on very different epistemic foundations.

The related works I could liberate from Zotero may be found below.