Comment by WorldMaker
1 hour ago
But again, the context is not about humans trying very hard to stick to problems in "terminating space" when writing software, but about LLMs with no such compunctions/boundaries finding inputs that break "terminating space assumptions". (Whether or not you also believe that LLMs are capable of staying within the lines of "terminating space" when generating code.)
Generally speaking, yes, humans want to design programs as best they can in the world of safely terminating applications. Humans aren't perfect at it today, given practical real world data such as CVE databases. Trying to hope humans become perfect to safeguard the world against LLMs like the Googler quote way above is the thing I find futile. Humans aren't going to magically get perfect. We need good enough solutions more than we need perfect solutions. The fear is that LLMs can greatly outpace humans in breaking "good enough" than humans can keep up in building "good enough".
You can prove a program is correct and terminates for all inputs and, absent a hardware or other assumption vulnerability that breaks the abstract machine assumptions, there would be no inputs that "break" anything. In fact, almost any human-designed program that is correct and terminates would not just be provable, but "easy" to prove algorithmically (in the theoretical sense, in a practical sense existing techniques are insufficient to prove complex programs).
Even ignoring isolation guarantees that could generically prevent unbounded escalation for arbitrary programs, you can just reject anything that is not "easy" to prove. Humans are really dumb, so anything that is not directly proven or easy to prove automatically is almost certainly not correct, so you can just err on the safe side and just reject them if you care about global correctness.