Acorn and the future of (AI?) theorem proving

https://lmao.bearblog.dev/acorn-ai-proving/

by LolWolf • 11 months ago

31 6 11 months ago

lmao.bearblog.dev

echostone• 11 months ago

Did not know about Acorn and it was an interesting read! However, I did a bit of digging and haven't found further details on how Acorn's internal prover "AI" works (saying it is an "ML" model makes me think it's some sort of oldschool model like random forests, but not sure yet). Though whatever it is, I wonder how they're going to keep it consistent over time (e.g., some proof steps suddenly becoming "unclear" after an update due to randomness of the ML model). I'm also not sure how this prover really fits in the AI proof scheme. Sure, even Terence Tao would likely admit that formalizing proofs with Acorn is easier than with Lean, but formalizing existing/ongoing proofs is only part of the picture.

To me the more intriguing question is: how would Acorn's "natural" interface cooperate with LM-based theorem provers? The best LLM provers + Lean combo right now can already crack IMO-level math, and what if they now write proofs in this more natural style? Will Acorn be better than Lean as an RL signal in this case?

LolWolf3• 11 months ago

it's some sort of oldschool model like random forests

It is a simple model, I think it's just a little dense NN with some hand-picked features. (https://github.com/acornprover/acorn/blob/master/python/mode...) Though Kevin has mentioned that, hopefully soon, we'll be able to have small-ish language models trained/fine-tuned on acornlib, but this requires some overhaul of the current approach to search.

I wonder how they're going to keep it consistent over time (e.g., some proof steps suddenly becoming "unclear" after an update due to randomness of the ML model)

The idea (which I realize I didn't write about in the blogpost) is that each model iteration will be trained on `acornlib` along with previous traces. While it's possible that sometimes the model will fail to find a given proof for a fact (and therefore require some help when it didn't previously), the idea is that the model is learning both from its previous proofs and also new proofs that have been developed in the library since its previous training. In this sense, the model is constantly being "added" to and so should (ideally!) perform at least as well, as the acornlib gets larger.

Sure, even Terence Tao would likely admit that formalizing proofs with Acorn is easier than with Lean, but formalizing existing/ongoing proofs is only part of the picture.

I think the point here is that, once the model gets good enough, you can just _write_ statements that you think might be true (and are, say, very nonobvious!) and then the Acorn engine would either automatically find a proof or give you a counterexample to the provided statement, which is much more akin to theorem proving with the computer.

The best LLM provers + Lean combo right now can already crack IMO-level math, and what if they now write proofs in this more natural style?

For sure, my guess is LLM provers will find this style substantially "easier" though they do just fine at Lean, too.

Will Acorn be better than Lean as an RL signal in this case?

I think this is the hope! The flywheel I think looks something like:

1. Train models using the standard library

2. Models can now discover new proofs of interesting facts and help in proving those more easily

3. Add those to the standard library + reasoning/proof traces

4. Train a new model on that

5. ???

6. Profit?

trueismywork• 11 months ago

Acorn is the software I had in mind in 2012 but was too unskilled/busy/young/poor to write.

LolWolf3• 11 months ago

It's neat stuff imo!

griffzhowl• 11 months ago

Definitely looks like a smoother experience than using Lean from this presentation. I guess their library is less fleshed-out than mathlib at the moment but that can only grow I suppose (hence acorn??). Will be curious to see how it develops

LolWolf3• 11 months ago

It is definitely less fleshed out since the project is very new (I think the first usable instance is like beginning of this year!) whereas afaik Lean 4's mathlib was ported from Lean 3 which has been around for at least 8 years and has had active contributions from around then too.

On the other hand, the `acornlib` (https://github.com/acornprover/acornlib) repo happily takes PRs that pass for many objects such as `Group`s (especially those in the standard library). so if there's something you're interested in proving, I would highly recommend just cloning it and proving it directly in the standard library and then PRing!

Acorn and the future of (AI?) theorem proving

Related Stories