To me it looks like that this allows you to sandbox a mathematical AI pretty securely as far as today’s cybersecurity practices go:
Write your theorem statement by hand. You can of course make mistakes here, but there is no adversarial pressure.
Run the AI on some sandboxed machine. From here, you export serialized proof objects (not Lean code).
Deserialize and verify the proof on some other machine. The attack surface becomes the deserializer + the two independent kernel implementations (you have to find bugs in both kernels simultaneously to exploit).
The question is whether this is relevant in any way?
If alignment issues become capability issues in hard-to-verify reward-hackable domains (I think we are already seeing some of this for coding), could areas like this with easy-to-verify non-hackable rewards see disproportionate capability growth?
If we get a “mathematical superintelligence” (that companies like https://harmonic.fun/ are claiming to want to build), we could probably get a bunch of formally verified software/hardware out of it, how does that change the world? (Is writing specifications going to become the bottleneck? That’s unclear to me.)
Is such a mathematical superintelligence useful for alignment research?
I just noticed that Lean now has a documented method to verify potentially malicious proofs: https://lean-lang.org/doc/reference/latest/ValidatingProofs/#validating-comparator https://github.com/leanprover/comparator
To me it looks like that this allows you to sandbox a mathematical AI pretty securely as far as today’s cybersecurity practices go:
Write your theorem statement by hand. You can of course make mistakes here, but there is no adversarial pressure.
Run the AI on some sandboxed machine. From here, you export serialized proof objects (not Lean code).
Deserialize and verify the proof on some other machine. The attack surface becomes the deserializer + the two independent kernel implementations (you have to find bugs in both kernels simultaneously to exploit).
The question is whether this is relevant in any way?
If alignment issues become capability issues in hard-to-verify reward-hackable domains (I think we are already seeing some of this for coding), could areas like this with easy-to-verify non-hackable rewards see disproportionate capability growth?
If we get a “mathematical superintelligence” (that companies like https://harmonic.fun/ are claiming to want to build), we could probably get a bunch of formally verified software/hardware out of it, how does that change the world? (Is writing specifications going to become the bottleneck? That’s unclear to me.)
Is such a mathematical superintelligence useful for alignment research?