I believe that the current trends for formal verification, say, of traditional programs or small neural networks, are more about conservative overapproximations (called abstract interpretations). You might want to have a look at this: https://caterinaurban.github.io/pdf/survey.pdf
To be more precise, it appears that so-called “incomplete formal methods” (3.1.1.2 in the survey I linked) are more computationally efficient, even though they can produce false negatives.
Does that answer your question ?
Paul W(Paul W)
Karma: 13
As far as I know (I’m not an expert), such absolute guarantees are too hard right now, especially if the AI you’re trying to verify is arbitrarily complex. However, the training process ought to yield an AI with specific properties. I’m not entirely sure I got what you meant by “a guaranteed no-zero-day evaluation and deployment codebase”. Would you mind explaining more ?
I think that’s closer to the idea: you {reject and penalize, during training} as soon as the AI tries something that might be “exploiting a zero-day”, in the sense that the world-model can’t rule out this possibility with high confidence[1]. That way, the training process is expected to reward simpler, more easily verified actions.
Then, a key question is “what else you do want from your AI ?”: of course, it is supposed to perform critical tasks, not just “let you see what program is running”[2], so there is tension between the various specifications you enter. The question of how far you can actually go, how much you can actually ask for, is both crucial, and wide open, as far as I can tell.
Some of the uncertainty lies in how accurate and how conservative the world-model is; you won’t get a “100% guarantee” anyway, especially since you’re only aiming for probabilistic bounds within the model.
Otherwise, a sponge would do.