4 ms·

Isn't it the case that you can only prove that a program halts if it can be reduced/transformed to a computational model (e.g., a model that is effectively calc

by AlanYx 2y ago

Isn't it the case that you can only prove that a program halts if it can be reduced/transformed to a computational model (e.g., a model that is effectively calculable) that is less powerful than a Turing machine? Had they framed their research as "how can we design models that are limited enough that we can guarantee their safety" (rather than how can we design a powerful extrinsic inspector to supervise), that would have made total sense to me. But if you can do that, many of the motivations for superalignment don't exist. Put another way, implicit in the superalignment game is the idea that models that require superalignment are going to be at least as powerful as what's on the horizon, not some reduceable subset thereof.

6gvONxR4sf7o 2y ago
> Isn't it the case that you can only prove that a program halts if it can be reduced/transformed to a computational model (e.g., a model that is effectively calculable) that is less powerful than a Turing machine? Models less power than a turing machine are still incredibly powerful. Some useful general purpose languages only accept programs that terminate. Hell, every useful program I ever wrote could be (in principle) proved to halt (excepting a `while True: do useful terminating thing again` main loop, of course).
ndriscoll 2y ago
In practice, most real world programs can be written in a way that only uses bounded recursion, so the halting problem doesn't really need to affect real-world programs. Or you can trivially ensure a program halts: add a timeout (and real-world programs like web servers do this all the time). I suppose the analogy for models is that if it can't decide whether output of another model is "safe", then it is not safe, so terminate. In practice, this could possibly be useful in the way a web server that times out after 1 second is still useful when its response times are normally measured in milliseconds. (Assuming of course that safety means anything in the first place)

by AlanYx 2y ago

6gvONxR4sf7o 2y ago

> Isn't it the case that you can only prove that a program halts if it can be reduced/transformed to a computational model (e.g., a model that is effectively calculable) that is less powerful than a Turing machine? Models less power than a turing machine are still incredibly powerful. Some useful general purpose languages only accept programs that terminate. Hell, every useful program I ever wrote could be (in principle) proved to halt (excepting a `while True: do useful terminating thing again` main loop, of course).

ndriscoll 2y ago

In practice, most real world programs can be written in a way that only uses bounded recursion, so the halting problem doesn't really need to affect real-world programs. Or you can trivially ensure a program halts: add a timeout (and real-world programs like web servers do this all the time). I suppose the analogy for models is that if it can't decide whether output of another model is "safe", then it is not safe, so terminate. In practice, this could possibly be useful in the way a web server that times out after 1 second is still useful when its response times are normally measured in milliseconds. (Assuming of course that safety means anything in the first place)