Outcome indistinguishability

Stream: Program verification

[Geoffrey Irving]

https://github.com/girving/debate/blob/main/Learn/Indistinguishable.lean formalises Dwork et al. 2022's multiplicative weights algorithm for outcome indistinguishability, using a simple model of real-valued circuits over an arbitrary primitive set.

Roughly, the theorem is that if we have a ground-truth distribution of input/output pairs (x,y) for y : Y, and a class of [-1,1]-bounded functions which act to distinguish ground truth from an attempted learned distribution, then we can learn an ε-indistinguishable circuit of size O(|Y| log |Y| / ε^2).

Caveat: The theorem in Dwork et al. pays attempt to sample complexity and the size of the distinguisher set. For our application we'll need only the existence of the small circuit, so I haven't formalised that part.

[Shreyas Srinivas]

Hey, so do you need a notion of substitution in your arithmetic circuits ?

[Shreyas Srinivas]

I am trying to find the substitution operation

[Shreyas Srinivas]

In our (not yet public) formalisation of arithmetic circuit complexity I carry a context of circuits and use natural number metavars.

[Shreyas Srinivas]

Our goal is to formalise certain lower bounds relevant to the VP vs VNP problem.

[Shreyas Srinivas]

I can’t immediately find the definition of substitution in your repository

[Geoffrey Irving]

I don’t need or define substitution currently. My Circuit type is admittedly a bit weird as it is defined relative to a set of primitives which take (1) one input x from a fixed type X and (2) some number of circuits. As a result, there are no “leaves” in the circuit, just calls to primitives that take (1) but not (2).

This is the kind of circuit I need for indistinguishability (and the downstream AI safety complexity theory), but it’s certainly weaker than a general circuit type.

I initially tried to define a Circuit type that took a bunch more type arguments, so that Circuits of different types could be plugged together when inputs and outputs matched. However, I ran into problems with Lean refusing to define recursive functions when the parameter types of the thing you’re inducting on vary. And then I realized I didn’t need that, and stopped trying (at least for the moment).

[Shreyas Srinivas]

But do you need a list of types? Aren’t all these circuits just taking in and outputting reals?

[Shreyas Srinivas]

Okay I think I am beginning to wrap my head around what you mean by these circuits. My circuits are different in that they are doing pure arithmetic (ring operations) to compute polynomials

[Geoffrey Irving]

The circuits always take X (which can be anything) and output a real. When eval’ed on x : X, x is passed as the first argument to every node in the circuit.

And yeah, these are fundamentally real-valued circuits rather than arithmetic circuits: we want to prove theorems that hold even if the set of primitives is very arbitrary, and then we construct very nonlinear stuff on top of that when doing the proof here.