3 ms·
I would think of two: 1) Much easier to state the problem and basically all the knowledge we have of math is not in the form of Lean proofs 2) It can be appli
by margorczynski 2y ago
I would think of two:
1) Much easier to state the problem and basically all the knowledge we have of math is not in the form of Lean proofs
2) It can be applied to a much broader range of domains, math is kinda unique as in most cases verifying something is 100% correct is impossible (and getting such a signal for RL)
- dimask 2y ago1) Then more math should get formalised in lean. 2) How is a solution by LLMs supposed to be verified without such a formalisation?
- sterlind 2y ago1) You could train a different language model to translate between Lean and English. Use AlphaProof to do the hard work of theorem proving; use the translation model for interpretability and as a user interface. In fact, such a system could be ideal for formalizing a hundred years of English-language proofs. 2) This model is already specialized for math; applying it to other domains is out of scope. And as you point out, speaking Lean (and thus being verifiable) gives you an RL reward signal that's way more precise and readily available than piddly RLHF from human reviewers. Gyms like this are where AGI will happen. (P.S. if anyone wants to work with me on reproducing AlphaProof, hit me up on Discord.)
- hackpert 2y agoHi! I've been working on theorem proving systems for some time now. I would love to help out with an AlphaProof reproduction, but I can't reach you on discord for some reason!
- sterlind 2y agoack! try again, I forgot to update my account name since Discord got rid of # tags. I also put my email as a fallback.