I’ve spent some time investigating/working on this. There are two approximate proof standards of relevance: constant error tolerance and relative error tolerance. A constant error bound proof (which can guarantee whp that there are less than c errors for some small constant c) seems to require complex zk-STARK/SNARK type circuit conversions. For the relaxed constraint of a c relative error bound for larger parallel computations much faster small overhead approaches are possible. So it seems you can combine these—use the very fast low overhead relative error bound proof for one or a few steps of your large parallel ANN,and then use the slower zk-STARK circuit for a serial proof over the chain of inner receipts.
The tradeoff is you no longer can prove strict correctness, and instead can only prove that the actual computation graph was similar to the claimed graph, and used about the same amount of compute. For DL training in particular seems like that is probably enough as you can prove the claimed circuit was the result of the claimed training algorithm on the claimed dataset up to a small constant number of ‘bitflip’ type dropout/dropin errors (which of course could be adversarial), and then you can include a tighter proof of a bound of the loss on a small hold out test set (which requires a more complex mechanism to prove that the test set wasn’t part of the training set or wasn’t available at that time yet, but that also seems doable).
So I think it is possible to get reasonable low cost DL training proofs, but that is all assuming deterministic computation, which is unfortunate as much of the remaining hardware gains at the end of moore’s law require non-deterministic approx computation (hardware level stochastic rounding, as in brains/neuromorphic computers). There may be some way to still scale probabilistic proofs in that regime, not sure yet.
One is just that I’m working in social computing, but a deeper interest is in relation to the ongoing conversation in techno-eschatology about whether advanced agents tend towards or away from mutual transparency, which is to say, towards coordination, peace, trade, or towards war and oppression
Compute proofs have interesting use cases but this seems a bit optimistic? If you are conversing with an open source agent A that can provide a complete proof of it’s computation graph that seems useful sure but you can only be certain that A exists in some sense, and never certain that A is not actually ‘imprisoned’ in some form and controlled by some other agent B.
Also there is a significant cost for being a fully open source agent. Not only does it give up much of the economic potential invested in the agent’s training, but it also—from the agent’s perspective—opens it up to sim imprisonment and associated torture/manipulation.
I’ve spent some time investigating/working on this. There are two approximate proof standards of relevance: constant error tolerance and relative error tolerance. A constant error bound proof (which can guarantee whp that there are less than c errors for some small constant c) seems to require complex zk-STARK/SNARK type circuit conversions. For the relaxed constraint of a c relative error bound for larger parallel computations much faster small overhead approaches are possible. So it seems you can combine these—use the very fast low overhead relative error bound proof for one or a few steps of your large parallel ANN,and then use the slower zk-STARK circuit for a serial proof over the chain of inner receipts.
The tradeoff is you no longer can prove strict correctness, and instead can only prove that the actual computation graph was similar to the claimed graph, and used about the same amount of compute. For DL training in particular seems like that is probably enough as you can prove the claimed circuit was the result of the claimed training algorithm on the claimed dataset up to a small constant number of ‘bitflip’ type dropout/dropin errors (which of course could be adversarial), and then you can include a tighter proof of a bound of the loss on a small hold out test set (which requires a more complex mechanism to prove that the test set wasn’t part of the training set or wasn’t available at that time yet, but that also seems doable).
So I think it is possible to get reasonable low cost DL training proofs, but that is all assuming deterministic computation, which is unfortunate as much of the remaining hardware gains at the end of moore’s law require non-deterministic approx computation (hardware level stochastic rounding, as in brains/neuromorphic computers). There may be some way to still scale probabilistic proofs in that regime, not sure yet.
Compute proofs have interesting use cases but this seems a bit optimistic? If you are conversing with an open source agent A that can provide a complete proof of it’s computation graph that seems useful sure but you can only be certain that A exists in some sense, and never certain that A is not actually ‘imprisoned’ in some form and controlled by some other agent B.
Also there is a significant cost for being a fully open source agent. Not only does it give up much of the economic potential invested in the agent’s training, but it also—from the agent’s perspective—opens it up to sim imprisonment and associated torture/manipulation.