Depend­ent Type The­ory and Zero-Shot Reasoning

I.

When I sit down to write code, I can safely throw everything I can think of at the prob­lem and just keep try­ing to run the code un­til it works—and when it works, I can ac­tu­ally see it work­ing. If my code runs, it means I ac­tu­ally had to un­der­stand enough of the mov­ing parts to get it to run. This is es­pe­cially true in lan­guages like Haskell with strong type con­straints pre­vent­ing me from do­ing any­thing too stu­pid.

When I sit down to prove a the­orem, I have to be much more care­ful. One mis­step in my reas­on­ing and my whole proof will be in­valid, without me even know­ing I made a mis­take un­til I or someone else catches it later. If my proof goes through, it’s pos­sible I un­der­stood enough of the mov­ing parts to make it work, but it’s also pos­sible I didn’t.

The stand­ard solu­tion to the prob­lem of not hav­ing some­thing to test your proof against when do­ing math is to use a proof checker, which lets you turn an ar­bit­rary math prob­lem into a pro­gram­ming prob­lem. In­stead of hav­ing to just get the right an­swer without ever be­ing able to ac­tu­ally check your an­swer, you get lots of chances to test pos­sible solu­tions.

Proof check­ers are great, but tra­di­tional proof check­ers are also pretty lim­ited. Con­cepts like equal­ity re­quire spe­cial­ized ma­chinery like para­mod­u­la­tion to prop­erly re­solve, in­tro­du­cing new data types re­quires writ­ing out long lists of PA-like ax­ioms and in gen­eral mod­ern func­tional pro­gram­ming tools that make writ­ing out math easier like pat­tern-match­ing, ADTs, mon­ads, etc. are just miss­ing. When I wrote my own the­orem prover/​proof checker a while ago I ran into ex­actly these sorts of prob­lems.

Depend­ent type the­ory is the mod­ern way to solve all of these prob­lems. Both equal­ity and the nat­ural num­bers are defined just by giv­ing the con­struct­ors, no ax­ioms needed. For-alls and im­plic­a­tions are just func­tions. Prov­ing the­or­ems really just feels like writ­ing Haskell code.

I’m not go­ing to try and give a de­pend­ent type the­ory tu­torial here, be­cause I don’t think I would be able to do bet­ter than the one I used, The­orem Prov­ing in Lean, which I highly re­com­mend tak­ing a look at. That be­ing said, I do want to give a couple ex­amples of what I mean be­fore I move on. Don’t worry if you don’t un­der­stand this part, I just want to show you some ac­tual code in a de­pend­ent type the­ory.

I said equal­ity and the nat­ural num­bers were just data types, but to show you what I mean here is the ac­tual defin­i­tion of the nat­ural num­bers in the Lean stand­ard library

in­duct­ive nat
| zero : nat
| succ (n : nat) : nat­

where : means “has type of.” Those few lines are all that are re­quired to com­pletely define the se­mantics of the nat­ural num­bers—the in­duc­tion rule is auto­mat­ic­ally syn­thes­ized from the above defin­i­tion.

Equal­ity is slightly more com­plex, but only be­cause you need a little bit more boil­er­plate. Here is the ac­tual defin­i­tion of equal­ity in the Lean stand­ard library

in­duct­ive eq {α : Sort u} (a : α) : α → Prop
| refl : eq a

which is really just the Lean trans­la­tion of the Haskell

data Equals a = Refl

where eq a rep­res­ents a = a and refl stands for re­flex­iv­ity, the rule that a = a al­ways holds.

II.

Even des­pite all of the ad­vances in auto­mated proof check­ing with de­pend­ent type the­ory, there’s still a big dis­ad­vant­age to typ­ing up all of your proofs in a de­pend­ent type the­ory like Lean: form­al­ity. When you write a proof by hand, you have the abil­ity to elide over all sorts of de­tails that you have to make ex­pli­cit when you type them up into a proof checker. Thus, the main reason not to use a proof checker is the very reason to use one in the first place.

I think there ex­ists a middle ground between these two ex­tremes, how­ever. One thing which has most im­pressed me work­ing with Nate Soares is his abil­ity to con­struct massive math­em­at­ical proofs on pa­per without a proof checker. When I asked him how he did this, he told me he used the type checker in his head. I’ve been try­ing to do this as well re­cently, and I want to try to share what that looks like.

Lawvere’s the­orem is a gen­eral res­ult in cat­egory the­ory that states that if there ex­ists a sur­ject­ive func­tion (tech­nic­ally but we’ll elide that de­tail), then has the prop­erty that any func­tion has some fixed point such that . To give you a sense of how im­port­ant this the­orem is, it’s the gen­eral res­ult un­der­ly­ing both Gödel’s in­com­plete­ness the­or­ems and Löb’s the­orem. I claim that Lawvere’s the­orem is nearly trivial to prove if you just ima­gine you have a type checker in your head.

Our start­ing en­vir­on­ment, where the rep­res­ents the thing we’re try­ing to prove, is

from which point the only pos­sible way to pro­ceed is to use , which, un­der the in­ter­pret­a­tion where for-alls are func­tions, re­quires us to pass it some . If you think about how to con­struct a with the right type out of what we cur­rently have avail­able, there really aren’t very many op­tions. In fact, I think there are ba­sic­ally just the two: and , but since we know we’re try­ing to prove some­thing about , the defin­i­tion with in it seems like the safest bet. Thus, we get

which, passing to , gives us

which we can (clas­sic­ally) un­pack into

and if two func­tions are equal, then they must be equal on all in­puts, and the only pos­sible in­put avail­able is , so we get

which, where , com­pletes the proof.

III.

I was talk­ing with Scott Gar­rabrant late one night re­cently and he gave me the fol­low­ing prob­lem: how do you get a fixed num­ber of DFA-based ro­bots to tra­verse an ar­bit­rary maze (if the ro­bots can loc­ally com­mu­nic­ate with each other)? My ap­proach to this prob­lem was to come up with and then try to falsify vari­ous pos­sible solu­tions. I star­ted with a hy­po­thesis, threw it against counter­examples, fixed it to re­solve the counter­examples, and it­er­ated. If I could find a hy­po­thesis which I could prove was un­falsifi­able, then I’d be done.

When Scott no­ticed I was us­ing this ap­proach, he re­marked on how dif­fer­ent it was than what he was used to when do­ing math. Scott’s ap­proach, in­stead, was to just start prov­ing all of the things he could about the sys­tem un­til he man­aged to prove that he had a solu­tion. Thus, while I was work­ing back­wards by com­ing up with pos­sible solu­tions, Scott was work­ing for­wards by ex­pand­ing the scope of what he knew un­til he found the solu­tion.

I think that the dif­fer­ence between my ap­proach and Scott’s ap­proach elu­cid­ates an im­port­ant dis­tinc­tion re­gard­ing strategies for solv­ing prob­lems in gen­eral. In Alex Zhu’s post on zero-shot reas­on­ing he talked about the dif­fer­ence between zero-shot reas­on­ing, where you solve the prob­lem without ever test­ing your solu­tion, and many-shot reas­on­ing, where you solve the prob­lem by test­ing your solu­tion re­peatedly. In many ways, Scott’s ap­proach to the ro­bot prob­lem was a zero-shot ap­proach, whereas my ap­proach was a many-shot ap­proach.

One thing that’s in­ter­est­ing in this ana­logy, how­ever, is that neither Scott or I were ac­tu­ally us­ing any tools to solve the prob­lem aside from our own brains. Thus, in some sense, both of our ap­proaches were zero-shot. And yet, my ap­proach cer­tainly feels far more many-shot than Scott’s. I’m go­ing to call what I did in this situ­ation many-shot reas­on­ing for a zero-shot prob­lem, and I think this idea is one that ap­plies a lot more broadly than just in that con­ver­sa­tion. One pos­sible way to un­der­stand the dis­tinc­tion between MIRI’s and Paul Chris­ti­ano’s strategies to­wards AI align­ment, for ex­ample, is us­ing this dis­tinc­tion. In this in­ter­pret­a­tion, MIRI is solv­ing the zero-shot prob­lem with zero-shot reas­on­ing, whereas Paul is solv­ing the zero-shot prob­lem with many-shot reas­on­ing.

In par­tic­u­lar, I think this idea maps well onto why I find de­pend­ent type the­ory so use­ful for solv­ing math prob­lems. When I write up a math prob­lem in Lean, I’m turn­ing what is fun­da­ment­ally a zero-shot prob­lem into some­thing more like a many-shot prob­lem, since it gives me a way to con­stantly be test­ing my hy­po­theses. But some­thing even more in­ter­est­ing is hap­pen­ing when I’m us­ing the type checker in my head. In that case, I’m do­ing some­thing more like what I did in the ro­bot prob­lem, where I’m us­ing many-shot reas­on­ing to solve a zero-shot prob­lem. I’m never ac­tu­ally us­ing any­thing to test my hy­po­theses—in­stead, I’m build­ing a model in my head of the thing which would test my hy­po­theses, and then test­ing them against that.

I think this hints at what a solu­tion to the zero-shot reas­on­ing prob­lem might look like: if you can build a model of the cor­res­pond­ing many-shot prob­lem which is ac­cur­ate enough, then you can use many-shot reas­on­ing on that model to solve the ori­ginal zero-shot prob­lem.