3 ms·
So if Lean was used to find the answers, where exactly is the AI? A thin wrapper around Lean?
by pclmulqdq 2y ago
So if Lean was used to find the answers, where exactly is the AI? A thin wrapper around Lean?
- dooglius 2y agoLean checks that the proof is valid, it didn't find the proof.
- xrisk 2y agoLean is just the language, Presumably to drive the AI towards the program (“the proof”)
- pishpash 2y agoThe AI is the "solver network", which is the (directed) search over solutions generated by Lean. The AI is in doing an efficient search, I suppose. I'm also waiting for my answer on the role of the Gemini formalizer, but reading between the lines, it looks like it was only used during training the "solver network", but not used in solving the IMO problems. If so then the hyping is greatly premature, as the hybrid formalizer/solver is the whole novelty of this, but it's not good enough to use end-to-end? You cannot say AlphaProof learned enough to solve problems if formalization made them easier to solve in the first place! You can say that the "solver network" part learned enough to solve formalized problems better than prior training methods.
- sdenton4 2y agoThink of problems in NP - you can check the answer efficiently, but finding the answer to check is the hard part... This is basically what we're looking at here: The proof checker can quickly evaluate correctness, but we need something to produce the proof, and that's the hard part.