Has any Circuit Complexity been formalized?

Stream: general

[Morgan Sinclaire]

I am wondering if any circuit complexity has been done in Lean or any other proof assistant? For example, the Shannon/Lupanov lower/upper bounds on maximal circuit sizes or Hastad’s switching lemma?

I’m aware that some mainstream complexity theory has been done (e.g. this discussion). After some quick searches I saw a bit of stuff on quantum circuits and some more applied work on VLSI circuits, but that was it.

[Shreyas Srinivas]

Nope. I did discuss this. Basically you need to figure a way to make binders work for circuits to represent them as DAGs instead of trees. This is relevant for circuit size. But it is otherwise a low hanging fruit. The Jukna book can be used

[Shreyas Srinivas]

One other challenge you will quickly encounter is that almost all interesting circuit complexity deals with uniform circuits. This is not a big deal as long as the complexity of circuit construction is irrelevant. But it becomes an issue as soon as you have to deal with something like DLOGTIME-uniform AC0. Because the DLOGTIME bit is defined w.r.t. a TM

[Shreyas Srinivas]

There is a TM library in mathlib but it doesn't count steps afaik. Further you need a convenient DSL to describe TMs. Then you need to count the steps taken up to asymptotics and then decode their output string to your circuit. At least this is the straightforward way

[Morgan Sinclaire]

Right, I am generally familiar with the things that make TMs/complexity theory hard to work with (and I don't want to fuss with with those problems at the moment). But the point is that, as far as I can tell, those reasons don't seem to apply to nonuniform complexity. Circuits are a bit more complicated to define than boolean formulas, but compared to TMs they seem much easier to set up and prove some basic constructions (e.g. a lot of circuit proofs can be done by induction). A colleague and I just made our own quick-and-dirty implementations of a straight-line program as a list of logic gates, where each gate can refer to an input variable or a gate earlier in the list (these could also be defined layer-by-layer or as DAGs).

In proportional terms, it is true that "most" of the interesting nonuniform complexity results involve uniformity in some way, there's also quite a lot that don't: Shannon/Lupanov (and sharper) bounds, Parity not in AC0, Yao's XOR lemma. Anyways, I think we're gonna have a go at some of this in Coq/Lean, but we're highly interested to hear about any related work people have done / are doing!

[Shreyas Srinivas]

So far there are no widely known attempts in lean

[Shreyas Srinivas]

Starting with non uniform classes is definitely a good idea.

[Luigi Massacci]

I think Yannic Forster at Inria in Paris has done a bunch of complexity in Coq and formalised several kinds of machines, I don't know about circuits, but it might be worth checking out

[Shreyas Srinivas]

That's on the lambda calculus with some call by push value eval rule

[Shreyas Srinivas]

It is not complexity theory in a form that complexity theorists would recognise (or would be found in a standard textbook on the subject)

[Shreyas Srinivas]

In particular it isn't circuit complexity. It is another matter that maybe complexity theorists ought to explore it more.

[Shreyas Srinivas]

A small update: A complexity theorist has approached me expressing an interest on formalising arithmetic complexity in lean. The good news is that this area deals largely with non-uniform circuits. We have worked out which source material to follow. A repository will materialise in the next few weeks.