ABEL

Stream: Machine Learning for Theorem Proving

[Fabian Glöckle]

@Jannis Limperg and I made a REPL based on Aesop that doesn't take "states = current goal stack" but allows to disentangle independent goals, allowing for methods like Hypertree proof search (https://arxiv.org/abs/2205.11491).

We are planning to open source the code soon. Paper: https://openreview.net/pdf?id=kk3mSjVCUO

[Mert Ünsal]

Hey Fabian - I saw your paper, very interesting results! I saw the Github repository but wasn’t able to easily hack it into something I can use.

Please let us know when you release this!

[Fabian Glöckle]

Which GitHub?

[Fabian Glöckle]

Aesoprepl is not public yet (on it!), you'll need 200 lines on top of Aesop.

[Mert Ünsal]

I was talking about github repo of ABEL but not even sure if it has the code for this - apparently not.

Let us know when we can use Aesoprepl :)

[Fabian Glöckle]

oh no, i just realized the name conflict to https://github.com/GAIR-NLP/abel -- it's unrelated

[Mert Ünsal]

I was actually refering to this: https://github.com/facebookresearch/Evariste which is the Github repository for your paper, right?

[Fabian Glöckle]

no it's the GitHub repo for facebook's 2022 paper https://arxiv.org/abs/2205.11491, but it's no longer used/maintained

[Notification Bot]

8 messages were moved here from #Machine Learning for Theorem Proving > Interacting with Lean 4 by Jason Rute.

[Fabian Glöckle]

To give a bit more context: this recreates HTPS (https://arxiv.org/abs/2205.11491) with a modern stack: Lean4, twice larger mathlib, Aesop, larger language models, faster language model inference code.

We view reinforcement learning as an inference technique: throw in all your theorems, let it run for some hours, get back as many proofs as it found. (Others would call this "life-long learning". :p)

The results exceed the reinforcement learnning baselines from before 2022 with a fraction of the compute. We're slightly below DeepSeekProver and InternLM2-StepProver without adding any additional data and likely also with a fraction of their compute (they don't release theirs).

[Huajian Xin]

Excellent work! I'm really looking forward to the open-sourcing of AesopRepl and the online RL algorithms!

[Albert Jiang]

Fabulous

[Albert Jiang]

Fabulous

[Charlie Meyer]

Any updates on open-sourcing AesopREPL?