Research on zero knowledge verification for frontier AI

I'd like to hire people (mostly postdocs, research engineers, PhD students) to work on developing open-source verification mechanisms to regulate frontier AI training; the idea is to aggregate a research community around Paris, exploiting the good talent pool there. We might spin up subgroups elsewhere in Western Europe, and will coordinate with the other actors working on open-source proposals.
We will be focusing, at least at first, on technical solutions that do not require hardware development, so they are quicker to deploy, with zero-knowledge protocols to ensure privacy.
We will coordinate closely with the GPAI Policy Lab to make sure our work stays relevant from a policy perspective.

Some research directions, more might appear as we go**:**

-Strengthening Inference verification [priority]: optimizing the protocols enables more generous sampling, thus better soundness. These gains will also be useful for agent auditing and watchdogs!

-Co-designing approximate/surrogate architectures for lowering costs of inference ZKPs: the classical example, already widely used, is fixed-point quantization for compatibility with finite fields; one can try to go further for the nonlinear operations, e.g. "piecewise polynomial approximations of exponential on negative values". These architectures can be used either for "approximate proofs for float-native LLMs", or natively for the audit agents and watchdogs (see below).

-Formal proofs for error bounds: to make sure the approximate methods above are sound enough, we need to compute error bounds. We want formal proofs, say in Lean, but these are not fully trustworthy either. So, carefully pre-building relevant reliable libraries and algorithms for computing and proving those can help make proofs shorter, which then makes auditing for fishy parts easier [possibly using LLM auditors, see below].

-Automation of the previous points: less critical, but could help for streamlining. Once we have good baselines for co-design and formal error bounds proofs, we can try to have [open-weights] LLMs do the heavy work there, i.e. given architecture and weights, produce a "close easier-to-ZKProve" copy, with a formal proofs for error bounds. Require ZKPs of execution for the process. Dedicated harnesses and fine-tuned versions of "frontier" open-weights LLMs could help improve efficieny and reliability.

-Agent auditing, with ZKPs of execution, as well as ZKPs for use of mech interp techniques to mitigate jailbreaking (probes, CoT monitoring, etc.). One can also consider having a "watchdog" [likely smaller than the usual audit agents, more optimized for inference ZKPs] that runs continously, checking for suspicious activity.

-Proofs of Useful Work, memory challenges, memory control: to mitigate the issue of "we do not know exactly how much computing power inference operations take, due to possible optimizations", one can focus on memory instead of throughput. One direction is having a small program required to run continuously on each GPU, managing memory by filling empty space with "unusable stuff" whenever it appears, typically during inference cycles. Execution of this would be required to be proved, most likely in zero-knowledge.

-Hybrid protocols: combining sampling-based bit-exact verifications with broader, weaker, cheaper checks [typically, approximate ones], can yield better tradeoffs than either kind of check alone. This principle could be used for both training and inference verification, though we expect it to be most useful for training.

-Interactivity and beacons: given issues with Fiat-Shamir (grinding and others), keeping some interactivity in the zero-knowledge protocol could be a better choice for soundness. Then, one might need to design a multi-party protocol, with e.g. public beacons, to avoid concentrating trust on a single verifier actor.

-Red-teaming and countermeasures: since we already found a rather serious potential issue for training verification [weight smuggling], we believe it is worth having people focusing mostly on finding [high-level concepts and possibly implementations for] attacks, e.g. exotic training techniques, and helping understand how to mitigate them.
This also includes abstract modelling of the problem [memory and computations, the control goal, etc.] to make the "search" more efficient, as well as, hopefully, prove positive results [under some assumptions, of course].

Important remarks:

-I think the project can scale very well with funding, up to around $20M; we might start hitting diminishing marginal returns at that point, but not before.
-Got several candidate hires already, can thus guarantee about $2M spend in the first year with all those, and $10M in the first 18 months is >80% likely.

Budget estimates:

-Up to $5M in hardware and compute, to run experiments, accelerate research, and help with cyberdefence; first big milestone at $500k here.

-For each person-year: around $100k-200k, depending on experience.
For each of the research threads above, having 2-3 persons per thread would be a good start.