8 ms·

So I am extremely hyped about this, but it's not clear to me how much heavy lifting this sentence is doing: > First, the problems were manually translated into

• ocfnash 2y ago
  The computer did find the answers itself. I.e., it found "even integers" for P1, "{1,1}" for P2, and "2" for P6. It then also provided provided a Lean proof in each case.
  • nnarek 2y ago
    formal definition of first theorem already contain answer of the problem "{α : ℝ | ∃ k : ℤ, Even k ∧ α = k}" (which mean set of even real numbers).if they say that they have translated first problem into formal definition then it is very interesting how they initially formalized problem without including answer in it
    • golol 2y ago
      I would expect that in their data which they train AlphaProof on they have some concept of a "vague problem" whoch could just look like {Formal description of the set in question} = ? And then Alphaproof has to find candidate descriptions of this set and prove a theorem that they are equal to the above. I doubt they would claim to solve the problem if they provided half of the answer.
      • puttycat 2y ago
        > I doubt they would claim to solve the problem if they provided half of the answer. Stranger things have happened
      • sebzim4500 2y ago
        To be fair, that isn't half the answer it's like 99% of the answer. They clarified above that it provided the full answer though.
      • JyB 2y ago
        The deepmind team has a history of being misleading. The great StarCraft 2 strategist bot is still in mind.
        • totoglazer 2y ago
          What’s the story with that bot? Always thought it was cool. Was that all smoke and mirrors?
          • topato 2y ago
            I think maybe parent comment is referring to it essentially just employing a zerg rush but with the speed and reaction time of an AI? Not 100% sure... Unrelated, iirc the starcraft functionality was an early example of generalizing a pretrained NN, alphaGO, and showing that it could adapt to learn and defeat games across strategic domains, especially after it learned so much strategy from the most difficult, widely played, and most strategically-varied physical game available.
      • chx 2y ago
        > I doubt they would claim to solve the problem if they provided half of the answer. This falls under extraordinary claims require extraordinary proof and we have seen nothing of the sort.
    • riku_iki 2y ago
      its not clear if theorem is actual input formal definition, or formal definition was in different form.
    • cygaril 2y ago
      Come up with many possible answers, formalize them all, and then try to prove or disprove each of them.
      • Davidzheng 2y ago
        This is probably partially what they did idk why it's downvoted lol
    • Smaug123 2y ago
      (You're talking to one of the people who was part of the project, which is why I took @ocfnash's answer as authoritative: they did not cheat.)
      • Xelynega 2y ago
        If they're talking to the people who are part of the project I'd hope the answer would contain detail and not expect to be taken as authoritative.
        • refulgentis 2y ago
          [flagged]
          • pishpash 2y ago
            [flagged]
            • refulgentis 2y ago
              That wasn't very nice. Are you curious about anything? Happy to help. I'd proactively do it, but I don't want to guess at whats in your mind. My initial guess is you think I think that engaging with the public is an infinite loop. I don't!
              • deleted 2y ago
                [deleted]
    • pishpash 2y ago
      Exactly, a problem and its answer are just different ways of describing the same object. Every step of a proof is a transformation/translation of the same object. It would be disingenuous to say that some heavy lifting isn't done in formalizing a problem but it seems that step is also performed by a machine: "We established a bridge between these two complementary spheres by fine-tuning a Gemini model to automatically translate natural language problem statements into formal statements, creating a large library of formal problems of varying difficulty." I'm confused, is the formalization by Gemini or "manually"? Which is it?
    • deleted 2y ago
      [deleted]
  • Davidzheng 2y ago
    Can you elaborate on how it makes guesses like this? Does it do experiments before? Is it raw LLM? Is it feedback loop based on partial progress?
    • Sharlin 2y ago
      "AlphaProof is a system that trains itself to prove mathematical statements in the formal language Lean. It couples a pre-trained language model with the AlphaZero reinforcement learning algorithm, which previously taught itself how to master the games of chess, shogi and Go."
      • JKCalhoun 2y ago
        Yeah I am not clear the degree to which this system and LLMs are related. Are they related? Or is AlphaProof a complete tangent to CHatGPT and its ilk?
        • gowld 2y ago
          It's not an English LLM (Large Language Model). It's a math Language Model. Not even sure it's a Large Language Model. (Maybe shares a foundational model with an English LLM; I don't know) It learns mathematical statements, and generates new mathematical statements, then uses search techniques to continue. Similar to Alpha Go's neural network, what makes it new and interesting is how the NN/LLM part makes smart guesses that drastically prune the search tree, before the brute-force search part. (This is also what humans do to solve math probrems. But humans are really, really slow at brute-force search, so we really almost entirely on the NN pattern-matching analogy-making part.)
          • sebzim4500 2y ago
            My reading of it is that it uses the same architecture as one of the Gemini models but does not share any weights with it. (i.e it's not just a finetune)
          • nextos 2y ago
  • freehorse 2y ago
    It would make a lot of sense for the lean-code-formalisation of the problems done by the researchers fed to the AI to be provided. Not assuming bad intent in not providing them, but it would help understand better the results.
• dooglius 2y ago
  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?
• deleted 2y ago
  [deleted]
• golol 2y ago
  > When presented with a problem, AlphaProof generates solution candidates and then proves or disproves them by searching over possible proof steps in Lean. To me, this sounds like Alphaproof receives a "problem", whatever that is (how do you formalize "determine all X such that..."? One is asked to show that an abstract set is actually some easily understandable set...). Then it generates candidate Theorems, persumably in Lean. I.e. the set is {n: P(n)} for some formula or something. Then it searches for proofs. I think if Alphaproof did not find {foo} but it was given then it would be very outrageous to claim that it solved the problem. I am also very hyped.
• zerocrates 2y ago
  Interesting that they have a formalizer (used to create the training data) but didn't use it here. Not reliable enough?
• summerlight 2y ago
  To speak generally, that translation part is much easier than the proof part. The problem with automated translation is that the translation result might be incorrect. This happens a lot when even people try formal methods by their hands, so I guess the researchers concluded that they'll have to audit every single translation regardless of using LLM or whatever tools.
  • thomasahle 2y ago
    You'd think that, but Timothy Gowers (the famous mathematician they worked with) wrote (https://x.com/wtgowers/status/1816509817382735986 https://x.com/wtgowers/status/1816509817382735986) > However, LLMs are not able to autoformalize reliably, so they got them to autoformalize each problem many times. Some of the formalizations were correct, but even the incorrect ones were useful as training data, as often they were easier problems. So didn't actually solve autoformalization, which is why they still needed humans to translate the input IMO 2024 problems. The reason why formalization is harder than you think is that there is no way to know if you got it right. You can use Reinforcement Learning with proofs and have a clear signal from the proof checker. We don't have a way to verify formalizations the same way.
    • llwu 2y ago
      > We don't have a way to verify formalizations the same way. While there is no perfect method, it is possible to use the agent to determine if the statement is false, has contradictory hypotheses, or a suspiciously short proof.
    • thrdbndndn 2y ago
      > However, LLMs are not able to autoformalize reliably, so they got them to autoformalize each problem many times. Some of the formalizations were correct, but even the incorrect ones were useful as training data, as often they were easier problems. A small detail wasn't clear to me: for these incorrectly formalized problems, how do they get the correct answer as ground truth for training? Have a human to manually solve them? (In contrast to problems actually from "a huge database of IMO-type problems", they do have answers for these already).
• kurthr 2y ago
  As is often the case, creating a well formed problem statement often takes as much knowledge (if not work) as finding the solution. But seriously, if you can't ask the LLM to solve the right question, you can't really expect it to give you the right answer unless you're really lucky. "I'm sorry, but I think you meant to ask a different question. You might want to check the homework set again to be sure, but here's what I think you really want."
• gowld 2y ago
  The article says > AlphaProof solved two algebra problems and one number theory problem by determining the answer and proving it was correct.
• sebzim4500 2y ago
  I as someone with a maths degree but who hasn't done this kind of thing for half a decade, was able to immediately guess the solution to (1) but actually proving it is much harder.
• hyfgfh 2y ago
  > First, the problems were manually translated into formal mathematical language for our systems to understand. Some people call this programming
• rldjbpin 2y ago
  as a noob, i feel that formalizing is a major part of solving the problem by yourserlf. my assessment is that once you identify certain patterns, you can solve problems by memorizing some patterns. but people might me can struggle with the first stage and solve the wrong problem. still good progress nonetheless. won't call the system sufficient by itself tho.
  • SonOfLilit 2y ago
    My mathematician friend said problem 5 (I think? With the monsters) seems hard to formulate, so I spent 15 minutes formulating it in pseudo-haskell. Then he gave me a huge hint to the solution, after which it only took me a couple of hours to solve. (Formalizing the solution is of course the hardest part, and might serve as a good masters dissertation I think)
    • rldjbpin 2y ago
      please pardon my ignorance, but to me a tower of hanoi question as a middle-schooler was the hardest thing to comprehend. but after learning about it, it is no longer quite as challenging to tackle. i understand that there are very hard questions for the olympiad. but it might be possible to learn about some recurring types of them by looking at past instances. it may not be the meta for IMO but has been for other kinds of exams.
• allxnb 2y ago
  Presenting this just as "translating into formal language" omits important information. Lean isn't just a formal language, it is also a theorem prover, Could the IMO participants use the nlinarith tactic? Could they use other tactics? Of course not, they had to show their work! Could they have mathematicians translate the problem statements into the formal language for them? Of course not, they had to do it themselves. In "How to solve it" Polya stresses multiple times that formalizing the initial question is an important part of the process. Then, the actual computational resources expressed in time are meaningless if one has a massive compute cloud. I'm a bit dissatisfied with the presentation, same as with the AlphaZero comparison to an obsolete Stockfish version that has been debunked multiple times.
• deleted 2y ago
  [deleted]