3 ms·

The linked page says > While the problem statements were formalized into Lean by hand, the answers within the problem statements were generated and formalized

The linked page says > While the problem statements were formalized into Lean by hand, the answers within the problem statements were generated and formalized by the agent. However, it's unclear what initial format was given to the agents that allowed this step

Smaug123 2y ago
FWIW, GPT-4o transcribed a screenshot of problem 1 perfectly into LaTeX, so I don't think "munge the problem into machine-readable form" is per se a difficult part of it these days even if they did somehow take shortcuts (which it sounds like they didn't).
- pclmulqdq 2y ago
  Comparing "turn photo into LaTeX" to "translate theorems into Lean" is like comparing a child's watercolor drawing to the Mona Lisa.
  - Smaug123 2y ago
    … no? After the LaTeX output, I told stock GPT4o that the answer was "all even integers", and asked for the statement in Lean. I had to make two changes to its output (both of which were compile-time errors, not misformalisations), and it gave me the formalisation of the difficult direction of the problem. Both changes were trivial: it had one incorrect (but unnecessary) import, and it used the syntax from Lean 3 instead of Lean 4 in one lambda definition. A system that was trained harder on Lean would not make those mistakes. The one actual error it made was in not proposing that the other direction of the "if and only if" is required. Again, I am quite confident that this formalisation failure mode is not hard to solve in a system that is, like, actually trained to do this. Obviously formalising problems that a working mathematicican solves is dramatically harder than formalising IMO problems, and is presumably way ahead of the state of the art.
    - lmm 2y ago
      > I am quite confident that this formalisation failure mode is not hard to solve in a system that is, like, actually trained to do this. Why?
      - Smaug123 2y ago
        This is really not the kind of problem LLMs are bad at! But since you insist, given the LaTeX, Claude 3.5 Sonnet correctly stated the theorem in full while inventing notation for the floor operation (it did correctly note unprompted what the right function was and how to obtain it from mathlib, but it incorrectly attempted to define syntax sugar for it).
        lmm 2y ago
        The hard part isn't getting the formalisation right sometimes, it's getting it right reliably (and unlike mistakes in the formal part, there's no way for the system to check itself in that part). IDK, even for translation between languages outside of mathematics, missing small qualifiers that change the whole meaning of the sentence is a worrying failure mode I've seen, and with mathematical problems there are a lot more cases like that.
  - sebzim4500 2y ago
    I think that's exagerating a bit. If you are familiar with both Lean and LaTeX then I think transcribing these problems to Lean only takes about twice as long as transcribing them to LaTeX.
pclmulqdq 2y ago
So if Lean was used to find the answers, where exactly is the AI? A thin wrapper around Lean?
- dooglius 2y ago
  Lean checks that the proof is valid, it didn't find the proof.
- xrisk 2y ago
  Lean is just the language, Presumably to drive the AI towards the program (“the proof”)
- pishpash 2y ago
  The 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 ago
  Think 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.

Smaug123 2y ago

FWIW, GPT-4o transcribed a screenshot of problem 1 perfectly into LaTeX, so I don't think "munge the problem into machine-readable form" is per se a difficult part of it these days even if they did somehow take shortcuts (which it sounds like they didn't).

pclmulqdq 2y ago
Comparing "turn photo into LaTeX" to "translate theorems into Lean" is like comparing a child's watercolor drawing to the Mona Lisa.
- Smaug123 2y ago
  … no? After the LaTeX output, I told stock GPT4o that the answer was "all even integers", and asked for the statement in Lean. I had to make two changes to its output (both of which were compile-time errors, not misformalisations), and it gave me the formalisation of the difficult direction of the problem. Both changes were trivial: it had one incorrect (but unnecessary) import, and it used the syntax from Lean 3 instead of Lean 4 in one lambda definition. A system that was trained harder on Lean would not make those mistakes. The one actual error it made was in not proposing that the other direction of the "if and only if" is required. Again, I am quite confident that this formalisation failure mode is not hard to solve in a system that is, like, actually trained to do this. Obviously formalising problems that a working mathematicican solves is dramatically harder than formalising IMO problems, and is presumably way ahead of the state of the art.
  - lmm 2y ago
    > I am quite confident that this formalisation failure mode is not hard to solve in a system that is, like, actually trained to do this. Why?
    - Smaug123 2y ago
      This is really not the kind of problem LLMs are bad at! But since you insist, given the LaTeX, Claude 3.5 Sonnet correctly stated the theorem in full while inventing notation for the floor operation (it did correctly note unprompted what the right function was and how to obtain it from mathlib, but it incorrectly attempted to define syntax sugar for it).
      - lmm 2y ago
        The hard part isn't getting the formalisation right sometimes, it's getting it right reliably (and unlike mistakes in the formal part, there's no way for the system to check itself in that part). IDK, even for translation between languages outside of mathematics, missing small qualifiers that change the whole meaning of the sentence is a worrying failure mode I've seen, and with mathematical problems there are a lot more cases like that.
- sebzim4500 2y ago
  I think that's exagerating a bit. If you are familiar with both Lean and LaTeX then I think transcribing these problems to Lean only takes about twice as long as transcribing them to LaTeX.

pclmulqdq 2y ago

So if Lean was used to find the answers, where exactly is the AI? A thin wrapper around Lean?

dooglius 2y ago
Lean checks that the proof is valid, it didn't find the proof.
xrisk 2y ago
Lean is just the language, Presumably to drive the AI towards the program (“the proof”)
pishpash 2y ago
The 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 ago
Think 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.