# 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.

• Cool! This re­minds me of di­men­sional ana­lysis, but with types in­stead of di­men­sions (and types have more struc­ture cos “->” is not com­mut­at­ive).

Also, I guess be­cause of de­pend­ent types’ con­nec­tion with con­struct­ive math­em­at­ics, this works less well if you want to cre­ate a proof that uses ex­cluded middle? I sup­pose you would end up with some­thing of the type (P → ⊥) → ⊥ and then be stuck

(Minor point: is the reason you say “ba­sic­ally two op­tions” for be­cause you could also have h(h(fxx)) etc.? I guess we even­tu­ally prove that that would be the same func­tion!)

• Di­men­sional ana­lysis is ab­so­lutely an in­stance of what I’m talk­ing about!

As for only be­ing able to do con­struct­ive stuff, you ac­tu­ally can do clas­sical stuff as well, but you have to ex­pli­citly as­sume the law of the ex­cluded middle. For ex­ample, if in Lean I write

ax­iom lem (P: Prop): P ∨ ¬P

then I can start do­ing clas­sical reas­on­ing.

Also, you’re totally right that you could also do and so on as much as you want, but there’s no real reason to do so, since if you start from the simplest pos­sible way to do it you’ll solve the prob­lem by the time you get to .

• Ah, cool thanks! I also real­ised that if you were just us­ing the type checker in your head, once you got to (P → ⊥) → ⊥, you could con­sider your proof done by your (out­side of the type checker) as­sump­tion of LEM. But I see no we don’t need to as­sume it out­side of the type checker!