Cunningham’s law: I make assertions about what the (emerging) field of AI verification should aim for, and people with experience in international policy, cybersecurity and any relevant field of engineering can point out what this draft gets wrong.
I used to like this law pre-LLMs, but it presumes verification is cheap relative to generation and lately that doesn’t fully stand.
A frame I kept applying while reading is on a separation between security and safety. I had it described as: - security asks how we stop the world from breaking into a system; - safety asks how we stop a system from breaking into the world.
The threat model contains two agents, which are both human coalitions. with no description for the compliant-prover / adversarial-model case. A model scheming through sanctioned channels can produce traffic that hashes clean and has syntactic checks passing because the syntax is faithful to the computation. The Aumann–Lindell inversion doesn’t transfer there, as deterrence assumes an adversary that values futures in which it got caught, whilist a misaligned model may not be playing an iterated game. Is the adversarial-model case in scope here, or left to another layer by design?
Also, the bilateral setting seems to hand the prover the sampling protocol, the batching scheme, the fault budget, and control of the workload-to-hash-space mapping; can’t fully see it right now, but that feels gameable.
I used to like this law pre-LLMs, but it presumes verification is cheap relative to generation and lately that doesn’t fully stand.
A frame I kept applying while reading is on a separation between security and safety. I had it described as:
- security asks how we stop the world from breaking into a system;
- safety asks how we stop a system from breaking into the world.
The threat model contains two agents, which are both human coalitions. with no description for the compliant-prover / adversarial-model case. A model scheming through sanctioned channels can produce traffic that hashes clean and has syntactic checks passing because the syntax is faithful to the computation. The Aumann–Lindell inversion doesn’t transfer there, as deterrence assumes an adversary that values futures in which it got caught, whilist a misaligned model may not be playing an iterated game. Is the adversarial-model case in scope here, or left to another layer by design?
Also, the bilateral setting seems to hand the prover the sampling protocol, the batching scheme, the fault budget, and control of the workload-to-hash-space mapping; can’t fully see it right now, but that feels gameable.