I suspect that this fails at the part where we actually make sure that the spec/formalization reflects what we think it does in natural language/human concepts (though, the exact setup found in the linked tweet is unusually clean/clever).
Off the top of my head, some possible failure modes I can imagine with the quoted scheme are:
Somehow the agent can write code that reproduces the honeypot’s contents for a very large, practically relevant set of honeypots.
Somehow the agent is able to achieve things by means other than writing code. (This is a special case of having the wrong formal model of the system.)
Somehow the formal model of the system is just wrong in some sort of way, so we make assumptions about what is achievable by writing code that are just not true.
It’s conceivable that the last one is solvable by some sort of rigorous practice but I’m not sure about the other two.
I’d be excited about a hillclimbed construction similar to this post or this post. Ie, a general way to superpose circuits such that the asymptotic bounds (and ideally fixed-budget bounds) are as tight as possible. One could also incorporate toy cases of hierarchy between circuits as an affordance to lower the bounds. I expect we’d learn interesting things from looking at the model’s solution.
what are some difficult but very well defined math problems that would help with alignment/interpretability?
I’m also curious about this. My sense is that there aren’t any.
Formally verify that an agent can’t escape from a sandbox.
I suspect that this fails at the part where we actually make sure that the spec/formalization reflects what we think it does in natural language/human concepts (though, the exact setup found in the linked tweet is unusually clean/clever). Off the top of my head, some possible failure modes I can imagine with the quoted scheme are:
Somehow the agent can write code that reproduces the honeypot’s contents for a very large, practically relevant set of honeypots.
Somehow the agent is able to achieve things by means other than writing code. (This is a special case of having the wrong formal model of the system.)
Somehow the formal model of the system is just wrong in some sort of way, so we make assumptions about what is achievable by writing code that are just not true.
It’s conceivable that the last one is solvable by some sort of rigorous practice but I’m not sure about the other two.
Perhaps ARC White-Box Estimation Challenge
I’d be excited about a hillclimbed construction similar to this post or this post. Ie, a general way to superpose circuits such that the asymptotic bounds (and ideally fixed-budget bounds) are as tight as possible. One could also incorporate toy cases of hierarchy between circuits as an affordance to lower the bounds. I expect we’d learn interesting things from looking at the model’s solution.