I was thinking that the formal guarantees would be about state evaluations (i.e. state → badness bounds) - which would require sth like “showing there is no zero-day” (since “a code-base with a zero-day” might be catastrophically bad if no constraints are put on actions). Thanks for pointing out they can be about action (i.e. (state, action) → badness bounds), which seem intuitively easier to get good bounds for (you don’t need to show there are no zero-days, just that the currently considered action is extremely unlikely to exploit a potential zero-day).
I’d be curious to know what kind of formal process could prove that (codebase, codebase-interaction) pairs are provably not-bad (with high probability, and with a false positive rate low enough if you trained an AI to minimize it). My guess is that there is nothing like that on the horizon (that could become competitive at all), but I could be wrong.
(“let you see what program is running” was an example of a very minimal safety guarantee I would like to have, not a representative safety guarantee. My point is that I’d be surprised if people got even such a simple and easy safety guarantee anytime soon, using formal methods to check AI actions that actually do useful stuff.)
I was thinking that the formal guarantees would be about state evaluations (i.e. state → badness bounds) - which would require sth like “showing there is no zero-day” (since “a code-base with a zero-day” might be catastrophically bad if no constraints are put on actions). Thanks for pointing out they can be about action (i.e. (state, action) → badness bounds), which seem intuitively easier to get good bounds for (you don’t need to show there are no zero-days, just that the currently considered action is extremely unlikely to exploit a potential zero-day).
I’d be curious to know what kind of formal process could prove that (codebase, codebase-interaction) pairs are provably not-bad (with high probability, and with a false positive rate low enough if you trained an AI to minimize it). My guess is that there is nothing like that on the horizon (that could become competitive at all), but I could be wrong.
(“let you see what program is running” was an example of a very minimal safety guarantee I would like to have, not a representative safety guarantee. My point is that I’d be surprised if people got even such a simple and easy safety guarantee anytime soon, using formal methods to check AI actions that actually do useful stuff.)