6 ms·
LeanDojo: Theorem Proving in Lean Using LLMs
- simonw 2y agoUseful context: https://en.m.wikipedia.org/wiki/Lean_(proof_assistant) https://en.m.wikipedia.org/wiki/Lean_(proof_assistant) - "Lean is a proof assistant and a functional programming language. It is based on the calculus of constructions with inductive types. "
- thomasahle 2y agoI wonder if they could integrate with the reinforcement learning approach from AlphaProof (this week). Having an IMO silver level proof copilot would pretty neat!
- Davidzheng 2y agoI wish someone could do a cost analysis of how much compute could replicate alphaproof. Alphazero was replicated in open source, hopefully this will be too!
- ijustlovemath 2y agoThis is precisely how Google built AlphaProof! Read the article, Lean's role is quite critical to its success. Privately, I think Lean could be incredibly powerful if baked deep into an ML's kernel/structure/training process. I think an AI proof of something like the Riemann Hypothesis may well be possible if you get enough resources behind it.
- mathinaly 2y agoIt's possible that the hypothesis is independent of the existing axiomatic systems for mathematics and a computer can't discover that on its own. It will loop forever looking for a proof that will never show up in the search. Computers are useful for doing fast calculations but attributing intelligence to them beyond that is mostly a result of confused ontologies and metaphysics about what computers are capable of doing. Computation is a subset of mathematics and can never actually be a replacement for it. The incompleteness theorem for example is a meta-mathematical statement about the limits of axiomatic systems that can not be discovered with axiomatic systems alone.
- ijustlovemath 2y agoPerhaps true of the class of problems that are undecidable in, say, the Peano axioms / ZFC. However, there are many things these axioms can prove that are still useful! For example, the multiplicity of the totient function, applications of which power much of modern cryptography. Riemann is so widely believed to be true that there are entire branches of mathematics dedicated to seeing what cool things you can learn about primes/combinatorics etc by taking Riemann to be true as an assumption.
- skissane 2y ago> It's possible that the hypothesis is independent of the existing axiomatic systems for mathematics and a computer can't discover that on its own. Humans have discovered independence proofs, e.g. Paul Cohen’s 1963 proof that the continuum hypothesis is independent of ZFC. I can’t see any reason in principle why a computer couldn’t do the same. If the Riemann hypothesis is independent of ZFC, and there exists a proof of that independence which is of tractable length, then in principle if a human could discover it, why couldn’t a sufficiently advanced computer system? Of course, it may turn out either that (a) Riemann hypothesis isn’t independent of ZFC (what most mathematicians think), or (b) it is independent but no proof exists, or (c) the shortest proof is so astronomically long nobody will ever be able to know it > The incompleteness theorem for example is a meta-mathematical statement about the limits of axiomatic systems that can not be discovered with axiomatic systems alone. We have proofs of Gödel‘s theorems. I see no reason in principle why a (sufficiently powerful) automated theorem prover couldn’t discover those proofs for itself. And maybe even one day discover proofs of novel theorems in the same vein
- mathinaly 2y agoNo computer has ever discovered the concept of a Turing machine and the associated halting problem (incompleteness theorem). If you think a search in an axiomatic system can discover an incompleteness result it is because your ontology about what computers can do is confused. People are not computers.
- bubblyworld 2y ago
- sva_ 2y ago> if baked deep into an ML's kernel/structure/training process Not sure of the feasibility of implementing lean as a GPU kernel, if you meant that. Also I'm not sure it makes sense to run Lean inside the (mostly matmul) training process. Now to use it to prepare some training data, it seems more realistic. But that seems to be what AlphaProof tries to do in the reinforcement step, if I'm not mistaken.
- magicalhippo 2y agoIt could perhaps also be used to guide the sampling step at the end, or? Similar to those syntax-constrained samplers to ensure the LLM spits out eg valid JSON.
- ijustlovemath 2y agoSyntax constraints are usually expressible as grammars, but the language of math is often very unique and domain specific, which makes this kind of approach tricky to get right
- Vecr 2y agoThankfully Lean exists, so the LLM can write that instead of the math syntax used in papers.
- magicalhippo 2y agoSo yea that was my thought. Use it to spit out valid Lean syntax, and potentially also to backtrack if it outputs inconsistent or erroneous proofs.
- namibj 2y agoIt's fairly good at valid syntax already, and did the backtracking for a long time due to it doing tree search guided by it's predictions for how likely that tactic will end up finishing the tree leaf it's applied to.
- thomasahle 2y ago> This is precisely how Google built AlphaProof! Read the article, Lean's role is quite critical to its success. I read the article. It doesn't say anything about generating new proofs to train on. It only mentions scraping Github for lean theorems+proofs.
- Davidzheng 2y agoI'm not sure if you're confusing alphaproof with leandojo here? Alphaproof generated its own proofs on 100M formal problems and did RL on this process.
- thomasahle 2y agoYes, I know AlphaProof did that. I wrote that it would be exciting "if they [LeanDojo] could integrate the reinforcement learning approach from AlphaProof". This would give LeanDojo a lot more training data, and hopefully give us an open source proof assistant at IMO Silver level.
- deleted 2y ago[deleted]
- Davidzheng 2y agoSorry!
- dkga 2y agoPerhaps a simpler and more reachable approach at this point would be to use the mathlib documentation to fuel a RAG on top of the fine-tuned/specialised model.
- pfdietz 2y agoI want to see a system that automates formalization of the existing math literature. LLMs are supposed to be good on language, right? So get them to read math papers and fill in the blanks, spitting out formalized versions of the results in Lean. We have centuries of literature to process, and when we're done there will be all of mathematics formalized to serve as training data for theorem provers moving into new mathematics.
- ijustlovemath 2y agoThe big problem with this is that many domains of math use hyper specialized notation, novel terms, different styles etc, and there's not much data for them to train on within any given niche. For example, the IUT "proof" of the abc conjecture used completely novel systems to come to its conclusions, to the point that it took top number theorists a few years to even parse what it was saying, and only then could they find the faults in the proof. I think the IUT proof would be a great adversarial example for any of these systems; if you can find the problem in the proof, you know you've hit on something pretty powerful.
- staunton 2y ago> if you can find the problem in the proof Is it still open whether there is a problem? Last I heard about this, there was one guy saying there's problems and the author dismissing that as "they just didn't understand it" without showing much interest in explaining it better...
- jcla1 2y agoI recon the general cosensus among mathematicians (as that is what counts) is that the ABC conjecture so far has _not_ been proven. Mochizuki (and his school around him) seem to be the majority of people that believe his proof is correct. As you point out, Scholze has identified a supposed flaw in Mochizuki's argument, but anyone not already at the forefront of IUT/NT/ABC conjecture is probably incapable of telling if this flaw is a true flaw or not. As Mochizuki refuses to elaborate (on this supposed flaw) consensus cannot be reached and thus the ABC conjecture remains open.
- namibj 2y agoAre you offering to code that or donate compute for the RL training? The problem is mostly that it's fairly intensive to code an efficient RL trainer for this, and even then it's expensive to run the training.
- thomasahle 2y agoMaybe it could be done distributed, in a similar way to the Leela Zero open source replication of Alpha Zero.
- worldsayshi 2y agoVictor Taelin is doing some semi-related stuff with Claude and their home built proof language Kind2: https://x.com/VictorTaelin/status/1811167900780175423 https://x.com/VictorTaelin/status/1811167900780175423 Can recommend taking a look at their recorded Twitch stream to see it in action.
- butokai 2y agoThat's really cool. Having spent most of my time in (european) academia, I wonder how this kind of research can be carried out outside of academic institutions.
- maxwells-daemon 2y agoSecond author here. Happy to answer any questions about the work!
- gnahtb 2y agothe infographic in the deepmind blog showed the team built a formalizer network. i wonder how you guys build it. last time i tried chatgpt to translate a math problem into lean it sucks
- maxwells-daemon 2y agoLeanDojo (at least as original published) did not use automatically formalized data, but extracted examples from Mathlib, which is already written in Lean.
- altkjg 2y agoGlad to see that major pieces of work like Lean or Wolfram Alpha are getting attention because LLMs utilize them. Still not convinced that LLMs do anything else than rearranging other people's work. Effects can already be seen: The Washington Post used to display articles when found via Google, now you get a paywall. And I can no longer criticize them for it.
- solumunus 2y ago> Still not convinced that LLMs do anything else than rearranging other people's work. It's amazing how useful and powerful that is in certain contexts.
- bjornsing 2y ago> Still not convinced that LLMs do anything else than rearranging other people's work. I’m not convinced that most people do anything else than rearrange other people’s work.
- fsndz 2y agoWhat's a real-life use case of theorem proving ? I really want to learn more about that but it always feel like an abstract thing that people do because they like solving puzzles. Does it help in solving the reliability challenge of current LLMs (https://www.lycee.ai/blog/ai-reliability-challenge https://www.lycee.ai/blog/ai-reliability-challenge) ?
- boroboro4 2y agoIt does, but not necessary with LLMs, see https://news.ycombinator.com/item?id=41069829 https://news.ycombinator.com/item?id=41069829 for example - this is mixing Lean with neural network to automatically proof theorems.
- agentultra 2y agoSel4 microkernel, compcert C compiler, https://bedrocksystems.com/ https://bedrocksystems.com/, AWS and Azure both use model checking, https://hackage.haskell.org/package/containers-verified https://hackage.haskell.org/package/containers-verified ... basically when you need to be sure certain properties of your system hold. You can verify only the critical parts, as in a data structure or algorithm, or you can verify higher-level parts of a system. All you're doing with math is thinking (out loud) and writing a proof is constructing a convincing argument. If you need to be certain that a thread doesn't leak addresses in shared memory to other threads then you ought to take the time to think through how you're going to achieve that and prove that your solution works.
- umutisik 2y agoReal life use cases for theorem proving I am aware of: - Formal verification of implementations for applications that require extreme security and reliability. (banking, aerospace, ...) - Automated theorem proving would increase the pace of theoretical work. In some cases, that helps guide useful work. There are better examples, but a simple one: nobody is looking for faster (worst-case) sorting algorithms because there is a proven theoretical limit. Don't believe in theory, but don't be without theory! It definitely won't hurt if theory-building is cheaper and faster. Also, it's the most complicated pure reasoning task you can build. So working on theorem-proving AI may help in reasoning and reliability.
- wolfspider 2y agoI was recently using Low* with ChatGPT and amazed it could actually explain it to me so I’m looking forward to using this.
- brotchie 2y agoHow good is Lean at assisting the analytical solution to PDEs? 10+ years out from a Finance PhD where I ended up using numerical methods because I really didn't have the math skills to prove closed form solutions. Would love to know if, starting with a stochastic differential equation, how far your can go re: applying Ito's lemma and working through the math to get to a closed form solution (using Lean). It the main advantage of Lean (ignoring LLM assistance) that you build up declarative code that, as you incrementally work on the proof, guarantees that the proof-so-far is correct? So you're still "working through the math" but rather than un-executable math notation written on a pad, you have "by induction" a guaranteed valid argument up to the point you are at in the proof? Just trying to build a mental model of Lean > pen and pad.
- mccoyb 2y agoNot quite a positive (it's ready now!) answer, but there's some interesting work on denoting problems, and constructing numerical methods for systems like the one you're describing -- I believe the design of this library (while not yet mature) would support the workflow you described (including both analytic and numerical solutions): https://github.com/lecopivo/SciLean https://github.com/lecopivo/SciLean To your last point, the idea is that numerical approximations can be introduced (and introduction will ask for proofs of validity! but you can ignore "the proving" via `sorry`) to go from un-executable math notation (in Lean4) to executable! Whether the proof goes through doesn't affect the final executable.