Comment by d4hines on Is anyone working on formally verified AI toolchains? · 2024-06-21T01:09:22.017Z · LW · GW

Alas, formal methods can't really help with that part. If you have the correct spec, formal methods can help you know with as much certainty as we know how to get that your program implements the spec without failing in undefined ways on weird edge cases. But even experienced, motivated formal methods practitioners sometimes get the spec wrong.  I suspect "getting the sign of the reward function" right is part of the spec, where theorem provers don't provide much leverage beyond what a marker and whiteboard (or program and unit tests) give you.