20 ms·

AI solves International Math Olympiad problems at silver medal level

• adverbly 2y ago
  > First, the problems were manually translated into formal mathematical language for our systems to understand. In the official competition, students submit answers in two sessions of 4.5 hours each. Our systems solved one problem within minutes and took up to three days to solve the others. Three days is interesting... Not technically silver medal performance I guess, but let's be real I'd be okay waiting a month for the cure to cancer.
  • ZenMikey 2y ago
    I haven't read TFA as I'm at work, but I would be very interested to know what the system was doing in those three days. Were there failed branches it explored? Was it just fumbling its way around until it guessed correctly? What did the feedback loop look like?
    • qsort 2y ago
      I can't find a link to an actual paper, that just seems to be a blog post. But from what I gather the problems were manually translated to Lean 4, and then the program is doing some kind of tree search. I'm assuming they are leveraging the proof checker to provide feedback to the model.
    • tsoj 2y ago
      This is NOT the paper, but probably a very similar solution: https://arxiv.org/abs/2009.03393 https://arxiv.org/abs/2009.03393
    • visarga 2y ago
      > just fumbling its way around until it guessed correctly As opposed to 0.999999% of the human population who can't do it even if their life depends on it?
      • dsign 2y ago
        I was going to come here to say that. I remember being a teenager and giving up in frustration at IMO problems. And I was competing at IPhO.
        • kevinventullo 2y ago
          Yeah, as a former research mathematician, I think “fumbling around blindly” is not an entirely unfair description of the research process. I believe even Wiles in a documentary described his search for the proof of Fermat’s last theorem as groping around in a pitch black room, but once the proof was discovered it was like someone turned the lights on.
      • logicchains 2y ago
        I guess you mean 99.9999%?
    • lacker 2y ago
      The training loop was also applied during the contest, reinforcing proofs of self-generated variations of the contest problems until a full solution could be found. So they had three days to keep training the model, on synthetic variations of each IMO problem.
    • thomasahle 2y ago
      They just write "it's like alpha zero". So presumably they used a version of MCTS where each terminal node is scored by LEAN as either correct or incorrect. Then they can train a network to evaluate intermediate positions (score network) and one to suggest things to try next (policy network).
    • utopcell 2y ago
      I'm at work and reading this article is the first thing I did this morning. What's your point ?
  • ComplexSystems 2y ago
    Or the simultaneous discovery of thousands of cryptographic exploits...
    • poincaredisk 2y ago
      Still waiting for the first one. I'm not holding my breath - just like fuzzing found a lot of vulnerabilities in low-level software, I expect novel automated analysis approaches will yield some vulnerabilities - but that won't be a catastrophic event just like fuzzing wasn't.
      • sqeaky 2y ago
        I hope it doesn't find a new class of bug. Find another thing like Spectre could be problematic. EDIT - I hope if that new class of bug exists that it is found. I hope that new class of bug doesn't exist.
      • throwaway240403 2y ago
        Hope that's true. Really mucks up the world a bit if not.
      • criddell 2y ago
        It's rumored that the NSA has 600 mathematicians working for them. If they are the ones finding the exploits you will probably never hear about them until they are independently discovered by someone who can publish.
      • ComplexSystems 2y ago
        Why don't you think that AI models will, perhaps rather soon, surpass human capabilities in finding security vulnerabilities? Because an AI that's even equally competent would be a fairly catastrophic event.
  • nnarek 2y ago
    "three days" does not say anything about how much computational power is used to solve problems, maybe they have used 10% of all GCP :)
    • vlovich123 2y ago
      The thing is though, once we have a benchmark that we pass, it’s pretty typical to be able to bring down time required in short order through performance improvements and iterating on ideas. So if you knew you had GAI but it took 100% of all GCP for 3 years to give a result, within the next 5 years that would come down significantly (not least of which you’d build HW dedicated to accelerating the slow parts).
      • tsimionescu 2y ago
        That's patently false for many classes of problems. We know exactly how to solve the traveling salesman problem, and have for decades, but we're nowhere close to solving a random 1000 city case (note: there are approximate methods that can find good, but not optimal, results on millions of cities). Edit: I should say 1,000,000 city problem, as there are some solutions for 30-60k cities from the 2000s. And there are good reasons to believe that theorem finding and proof generation are at least NP-hard problems.
        • rowanG077 2y ago
          The person said typical not always the case. Just because there are obviously cases where it didn't happen does mean it it's still not typically the case.
        • vlovich123 2y ago
          We're not talking about mathematical optimality here, both from the solution found and for the time taken. The point is whether this finds results more cheaply than a human can and right now it's better on some problems while others it's worse. Clearly if a human can do it, there is a way to solve it in a cheaper amount of time and it would be flawed reasoning to think that improving the amount of time would be asymptotically optimal already. While I agree that not all problems show this kind of acceleration in performance, that's typically only true if you've already spent so much time trying to solve it that you've asymptoted to the optimal solution. Right now we're nowhere near the asymptote for AI improvements. Additionally, there's so many research dollars flowing into AI precisely because the potential upside here is nowhere near realized and there's lots of research lines still left to be explored. George Hinton ended the AI winter.
  • wongarsu 2y ago
    The problem solved "within minutes" is also interesting. I'd interpret that as somewhere between 2 and 59 minutes. Given the vagueness probably on the higher end, otherwise they'd celebrate it more. The students had 6 tasks in 9 hours, so on average 1.5h per task. If you add the time a student would take to (correctly!) translate the problems to their input format, their best-case runtime is probably about as fast as a silver-medalist would take to solve the problem on their own. But even if they aren't as fast as humans yet this is very valuable. Both as a stepping stone, and because at a certain scale compute is much easier to scale than skilled mathematicians.
    • gjm11 2y ago
      They say "our systems" (presumably meaning AlphaProof and AlphaGeometry 2) solved one problem "within minutes", and later on the page they say that the geometry question (#4) was solved by AlphaGeometry in 19 seconds. So either (1) "within minutes" was underselling the abilities of the system, or (2) what they actually meant was that the geometry problem was solved in 19 seconds, one of the others "within minutes" (I'd guess #1 which is definitely easier than the other two they solved), and the others in unspecified times of which the longer was ~3 days. I'd guess it's the first of those. (Euclidean geometry has been a kinda-solved domain for some time; it's not super-surprising that they were able to solve that problem quickly.) As for the long solve times, I would guess they're related to this fascinating remark: > The training loop was also applied during the contest, reinforcing proofs of self-generated variations of the contest problems until a full solution could be found.
      • visarga 2y ago
        Euclidian Geometry still requires constructions to solve, and those are based in intuition.
        • gjm11 2y ago
          There are known algorithms that can solve _all_ problems in euclidean (ruler-and-compasses) geometry, no intuition required. The most effective algorithms of this type are quite inefficient, though, and (at least according to DeepMind) don't do as well as AlphaGeometry does at e.g. IMO geometry problems.
  • lolinder 2y ago
    It feels pretty disingenuous to claim silver-medal status when your machine played by significantly different rules. The article is light on details, but it says they wired it up to a theorem prover, presumably with feedback sent back to the AI model for re-evaluation. How many cycles of guess-and-check did it take over the course of three days to get the right answer? If the IMO contestants were allowed to use theorem provers and were given 3 days (even factoring in sleep) would AlphaProof still have gotten silver? > let's be real I'd be okay waiting a month for the cure to cancer. I don't think these results suggest that we're on the brink of knowledge coming at a substantially faster rate than before. Humans have been using theorem provers to advance our understanding for decades. Now an LLM has been wired up to one too, but it still took 8x as long to solve the problems as our best humans did without any computer assistance.
    • ToucanLoucan 2y ago
      I am so exhausted of the AI hype nonsense. LLMs are not fucking curing cancer. Not now, not in five years, not in a hundred years. That's not what they do. LLM/ML is fascinating tech that has a lot of legitimate applications, but it is not fucking intelligent, artificial or otherwise, and I am sick to death of people treating it like it is.
      • apsec112 2y ago
        What observation, if you saw it, do you think would falsify that hypothesis?
        • necovek 2y ago
          It seems unlikely people will employ only ML models, especially LLM, to achieve great results: they will combine it with human insights (through direction and concrete algorithms). It's obvious that's happening with LLMs even today to ensure they don't spew out too much bullshit or harmful content. So let's get to a point where we can trust AI as-is first, and let's talk about what's needed to achieve the next milestone after and if we get there. And I love asking every new iteration of ChatGPT/Gemini something along the lines of "What day was yesterday if yesterday was a Thursday?" It just makes me giggle.
  • 10100110 2y ago
    Don't confuse interpolation with extrapolation. Curing cancer will require new ideas. IMO requires skill proficiency in tasks where the methods of solving are known.
    • trueismywork 2y ago
      They are the same things
    • golol 2y ago
      Mathematicians spend most of their time interpolating between known ideas and it would be extremely helpful to have computer assistance with that.
    • visarga 2y ago
      Search is extrapolation. Learning is interpolation. Search+Learn is the formula used by AZ. Don't forget AZ taught us humans a thing or two about a game we had 2000 years head start in, and starting from scratch not from human supervision.
      • xdavidliu 2y ago
        no, search is not extrapolation. Extrapolation means taking some data and projecting out beyond the limits of that data. For example, if my bank account had $10 today and $20 tomorrow, then I can extrapolate and say it might have $30 the day after tomorrow. Interpolation means taking some data and inferring the gaps of that data. For example, if I had $10 today and $30 the day after tomorrow, I can interpolate and say I probably had $20 tomorrow. Search is different from either of those things, it's when you have a target and a collection of other things, and are trying to find the target in that collection.
        • visarga 2y ago
          Search can go from a random init model to beating humans at Go. That is not interpolation. - Search allows exploration of the game tree, potentially finding novel strategies. - Learning compresses the insights gained from search into a more efficient policy. - This compressed policy then guides future searches more effectively. Evolution is also a form of search, and it is open-ended. AlphaProof solved IMO problems, those are chosen to be out of distribution, simple imitation can't solve them. Scientists do (re)search, they find novel insights nobody else discovered before. What I want to say is that search is on a whole different level than what neural nets do, they can only interpolate their training data, search pushes outside of the known data distribution. It's actually a combo of search+learning that is necessary, learning is just the little brother of search, it compresses novel insights into the model. You can think of training a neural net also as search - the best parameters that would fit the training set.
• iamronaldo 2y ago
  No benchmarks of any kind?
• arnabgho 2y ago
  https://x.com/GoogleDeepMind/status/1816498082860667086 https://x.com/GoogleDeepMind/status/1816498082860667086
• piombisallow 2y ago
  IMO problems aren't fundamentally different from chess or other games, in that the answer is already known.
  • Smaug123 2y ago
    I really don't understand what you mean by this. 1) it's not known whether chess is a win for White or not. 2) IMO problems, such as 2024 problem 1 which the system solved, are often phrased as "Determine all X such that…".
    • diffeomorphism 2y ago
      You are attacking a straw man and the point made is pretty good. Competition problems are designed to be actually solvable by contestants. In particular, the problems should be solvable using a reasonable collection of techniques and many "prep courses" will teach you many techniques, tools and algorithms and a good starting point is to throw that stuff at any given problem. So just like chess openings putting in lots of leg work will give you some good results for that part. You might very well lose in mid and late game, just like this AI might struggle with "actual problems" It is of course still very impressive, but that is an important point.
      • Smaug123 2y ago
        I'm attacking nobody! I literally couldn't understand the point, so I said so: as stated, its premises are simply clearly false! Your point, however, is certainly a good one: IMO problems are an extremely narrow subset of the space of mathematical problems, which is itself not necessarily even 50% of the space of the work of a mathematician.
  • wufufufu 2y ago
    Kinda? Chess isn't solved. Complex problems can have better solutions discovered in the future.
    • jeremyjh 2y ago
• c0l0 2y ago
  That's great, but does that particular model also know if/when/that it does not know?
  • foota 2y ago
    Never? Edit: To defend my response, the model definitely knows when it hasn't yet found a correct response, but this is categorically different from knowing that it does not know (and of course monkeys and typewriters etc., can always find a proof eventually if one exists).
  • ibash 2y ago
    Yes > AlphaProof is a system that trains itself to prove mathematical statements in the formal language Lean. … Formal languages offer the critical advantage that proofs involving mathematical reasoning can be formally verified for correctness.
  • diffeomorphism 2y ago
    While that was probably meant to be rhetorical, the answer surprisingly seems to be an extremely strong "Yes, it does". Exciting times.
• PaulHoule 2y ago
  See https://en.wikipedia.org/wiki/Automated_Mathematician https://en.wikipedia.org/wiki/Automated_Mathematician for an early system that seems similar in some way.
  • golol 2y ago
    This Wikipedia page makes AM kind of comes across as a nonsense project whose outputs no one (besides the author) bothered to decipher.
• petters 2y ago
  The problems were first converted into a formal language. So they were partly solved by the AI
  • jeremyjh 2y ago
    Yes and it is difficult for me to believe that there is not useful human analysis and understanding involved in this translation that the AI is helpless without. But that I suppose is a problem that could be tackled with a different model...
    • adrianN 2y ago
      Even so, having a human formalize the problems and an AI to find machine checkable proofs could be very useful for mathematicians.
    • sebzim4500 2y ago
      It is vastly easier to do the formalization than to actually solve the problem. Any undergraduate with some lean familiarity could do it in minutes.
      • Davidzheng 2y ago
        Disagree! Some problems are much harder than others. If you don't believe me please go formalize P5 in this year imo.
        • sebzim4500 2y ago
          Yeah, I was just referring to the problems that it actually did.
        • SonOfLilit 2y ago
          I formalized it last night, to a level that an IMO trainer agreed was adequate. Took maybe 15 minutes. Find n such that p(n) and not p(n-1). p(n): exists(f: state -> move) such that solves(f, n) state: solved | illegal | (k, is_first_move in {T,F}, px in (1,2023), py in (1,2024+1), mapping from x,y to {T,F, ?}) initial_state(n): (n, T, 1, 1, {(x,y) -> ?}) move: U|D|L|R|(x in (1,2023)) power: ((a -> a), integer) -> (a->a) power(h, 0)(x) = h(x) power(h, k)(x) = h(power(k-1))(x) solves(f, n): exists l such that for every board, power(make_move(board, f), l)(initial_state(n)) = solved board: permutation of (1, 2, 3, ..., 2022+1) make_move: (board, (state -> move)) -> (state -> state) make_move(board, f)(solved): solved make_move(board, f)(illegal): illegal make_move(board, f)(s = (k, is_first_move, px, py, m)) if is_first_move = T: if k = 0: illegal else if f(s) is a number: (k, F, f(s), 1, m) else: illegal else: if f(s) is a number: illegal else if py = 2025: solved else if board(px) = py and py != 1: (k - 1, T, px, py, m + {((px, py), T)}) else: dy = {U:-1,D:1,L:0,R:0}(f(s)) dx = {U:0,D:0,L:-1,R:1}(f(s)) px' = px+dx py' = py+dy if px' < 1 or px' > 2023 or py' < 1 or py' > 2025: illegal (k, F, px', py', m + {((px, py), F)})
• Davidzheng 2y ago
  HOLY SHIT. It's amazing
• deleted 2y ago
  [deleted]
• deleted 2y ago
  [deleted]
• osti 2y ago
  So they weren't able to solve the combinatorics problem. I'm not super well versed in competition math, but combinatorics always seem to be the most interesting problems to me.
  • sigbottle 2y ago
    I mean, IMO algebra problems can require very clever insights as well, and number theory especially has some really nice proof arguments you can make. It's easier to make a bad problem of this category though because it's much easier to hide the difficulty in a bunch of computations / rote deduction, and not creative insights. Combinatorics problems are usually simple enough that anyone can understand and try tackling it though, and the solutions in IMO are usually designed to be elegant. I don't think I've ever seen a bad combo problem before.
    • osti 2y ago
      Oh I'm sure the other topics all do have interesting problems, but I don't have the background necessary to even tackle them. Your second paragraph conveyed exactly how I feel about combinatorics. Elegant and clever, on top of being understandable to even non math people.
• mupuff1234 2y ago
  Can it / did it solve problems that weren't solved yet?
  • raincole 2y ago
    Techinically yes. And it's easy. You can probably do it with your PC's computational power. The thing is that most math "problems" are not solved not becasue they're hard, but because they're not interesting enough to even be discovered by humans.
    • mupuff1234 2y ago
      Yeah, I mean "interesting" problems (perhaps not fields medal interesting, but interesting enough)
• Ericson2314 2y ago
  The lede is a bit buried: they're using Lean! This is important for more than Math problems. Making ML models wrestle with proof systems is a good way to avoid bullshit in general. Hopefully more humans write types in Lean and similar systems as a much way of writing prompts.
  • Ericson2314 2y ago
    They're def gonna go after the Riemann hypothesis with this, hehe.
    • nwoli 2y ago
      Guessing the context here is that the RH was recently translated into Lean. Would be very cool if they threw their compute on that
      • Smaug123 2y ago
        I think you might be thinking of the recent project to start Fermat's Last Theorem? The Riemann hypothesis has been easy to state (given what's in Mathlib) for years.
        • Davidzheng 2y ago
          Yeah lol i don't think either is hard to formalize in lean
          • raincole 2y ago
            They're not just formalizing Fermant's Last Theorem's statement itself. They're formalizing the proof.
  • Smaug123 2y ago
    And while AlphaProof is clearly extremely impressive, it does give the computer an advantage that a human doesn't have in the IMO: nobody's going to be constructing Gröbner bases in their head, but `polyrith` is just eight characters away. I saw AlphaProof used `nlinarith`.
• riku_iki 2y ago
  Example of proof from AlphaProof system: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P6/index.html https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
• highcountess 2y ago
  [flagged]
  • ykonstant 2y ago
    Programming in Lean?
  • dpbriggs 2y ago
    This is more analogous to programmers working with copilot. There's an exciting possibility here of mathematicians feeding these systems subproblems to assist in proving larger theorums.
    • highcountess 2y ago
      It was not meant to be a serious comment even though it seems it may have touched a nerve.
  • Davidzheng 2y ago
    lol
    • Davidzheng 2y ago
      Of course i agree they will be better--I'm happy to be like chess players and just admire the machines and entertains humans
• golol 2y ago
  This is the real deal. AlphaGeometry solved a very limited set of problems with a lot of brute force search. This is a much broader method that I believe will have a great impact on the way we do mathematics. They are really implementing a self-feeding pipeling from natural language mathematics to formalized mathematics where they can train both formalization and proving. In principle this pipeline can also learn basic theory building like creating auxilliary definitions and Lemmas. I really think this is the holy grail of proof-assistance and will allow us to formalize most mathematics that we create very naturally. Humans will work podt-rigorously and let the machine asisst with filling in the details.
  • visarga 2y ago
    > a lot of brute force search Don't dismiss search, it might be brute force but it goes beyond human level in Go and silver at IMO. Search is also what powers evolution which created us, also by a lot of brute forcing, and is at the core of scientific method (re)search.
    • Eridrus 2y ago
      Search is great, search works, but there was not a tonne to learn from the AlphaGeometry paper unless you were specifically interested in solving geometry problems.
    • kypro 2y ago
      My old AI professor used to say that every problem is a search problem. The issue is that to find solutions for useful problems you're often searching through highly complex and often infinite solution spaces.
      • visarga 2y ago
        For some problems validation is expensive. Like the particle collider or space telescope, or testing the COVID vaccine. It's actually validation that is the bottleneck in search not ideation.
      • pishpash 2y ago
• Smaug123 2y ago
  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 formal mathematical language for our systems to understand. The non-geometry problems which were solved were all of the form "Determine all X such that…", and the resulting theorem statements are all of the form "We show that the set of all X is {foo}". The downloadable solutions from https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html https://storage.googleapis.com/deepmind-media/DeepMind.com/B... don't make it clear whether the set {foo} was decided by a human during this translation step, or whether the computer found it. I want to believe that the computer found it, but I can't find anything to confirm. Anyone know?
  • 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
• AyyEye 2y ago
  Parlor tricks. Wake me up AI can reliably identify which number is circled at the level of my two year old.
• balls187 2y ago
  What was the total energy consumption required to acheive this result (both training and running) And, how much CO2 was released into earths atmosphere?
  • ozten 2y ago
    Compared to all of the humans who compete at this level and their inputs and outputs for the trailing 5 years.
    • balls187 2y ago
      And? The result is (likely) net energy consumption, resulting in (likely) net CO2 emissions. So, what was did it cost us for this achievement in AI? EDIT TO ADD: It's fair to think that such a presser should not include answers to my questions. But, it's also fair to want that level of transparency given we are dealing with climate change.
      • regularfry 2y ago
        You're not wrong and in general the conclusion is that AI emits less CO2 than a human performing the same task. Whether that's true for this specific task is worth asking, as is the question of how efficient such a process can be made.
  • amelius 2y ago
    There's no energy limit in the IMO rules.
    • balls187 2y ago
      The point isn't IMO rules. It's that we are living in a period of time where there are very real consequences of nearly a century of unchecked CO2 due to human industry. And AI (like crypto before it) requires considerable energy consumption. Because of which, I believe we (people who believe in AI) need to hold companies accountable by very transparently disclosing those energy costs.
• majikaja 2y ago
  It would be nice if on the page they included detailed descriptions of the proofs it came up with, more information about the capabilities of the system and insights into the training process... If the data is synthetic and covers a limited class of problems I would imagine what it's doing mostly reduces to some basic search pattern heuristics which would be of more value to understand than just being told it can solve a few problems in three days.
  • cygaril 2y ago
    Proofs are here: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
    • majikaja 2y ago
      I found those, I just would have appreciated if the content of the mathematics wasn't sidelined to a separate download as if it's not important. I felt the explanation on the page was shallow, as if they just want people to accept it's a black box. All I've learnt from this is that they used an unstated amount of computational resources just to basically brute force what a human already is capable of doing in far less time.
      • Davidzheng 2y ago
        Very few humans can after years of training. Please don't trivialize.
        • necovek 2y ago
          Very few humans go after this type of the training. In my "math talent" school (most of the Serbian/Yugoslavian medal winners came from it), at most a dozen students "trained" for this over 4 high school generations (500 students). Problems are certainly not trivial, but humans are not really putting all their effort into it either, and the few that do train for it, on average medal 50% of the time and get a silver or better 25% of the time (by design) with much less time available to do the problems.
• fancyfredbot 2y ago
  I'm seriously jealous of the people getting paid to work on this. Sounds great fun and must be incredibly satisfying to move the state of the art forward like that.
  • Mithriil 2y ago
    Best we can do then is keep ourselves up to date and give our support!
  • bearjaws 2y ago
    C'mon you're meant to be re-configuring 3,292,329 line of YML for K8s. (/s)
    • psbp 2y ago
      It's funny that if I could describe my entire career, it would probably be something similar to software janitor/maintenance worker. I guess I should have pursued a PhD when I was younger.
      • geodel 2y ago
        In another universe, this comment would be "With low pay and few academic jobs going for PhD was the worst decision of my life"
  • onemoresoop 2y ago
    You probably mean envious not jealous.
    • yalok 2y ago
      I'm learning something new today. In some other languages these 2 are usually the same 1 word.
      • Vinnl 2y ago
        Huh. So I tried to look it up just now and I'm not sure if I understand the difference. (To the extent that there is one - apparently one can mean the other, but I imagine they're usually used as follows.) It looks like "jealous" is more being afraid of losing something you have (most commonly e.g. a spouse's affection) to someone else, whereas "envious" is wanting what someone else has?
• lolinder 2y ago
  This is a fun result for AI, but a very disingenuous way to market it. IMO contestants aren't allowed to bring in paper tables, much less a whole theorem prover. They're given two 4.5 hour sessions (9 hours total) to solve all the problems with nothing but pencils, rulers, and compasses [0]. This model, meanwhile, was wired up to a theorem proover and took three solid days to solve the problems. The article is extremely light on details, but I'm assuming that most of that time was guess-and-check: feed the theorem prover a possible answer, get feedback, adjust accordingly. If the IMO contestants were given a theorem prover and three days (even counting breaks for sleeping and eating!), how would AlphaProof have ranked? Don't get me wrong, this is a fun project and an exciting result, but their comparison to silver medalists at the IMO is just feeding into the excessive hype around AI, not accurately representing its current state relative to humanity. [0] 5.1 and 5.4 in the regulations: https://www.imo-official.org/documents/RegulationsIMO.pdf https://www.imo-official.org/documents/RegulationsIMO.pdf
  • gjm11 2y ago
    Working mathematicians mostly don't use theorem provers in their work, and find that when they do they go significantly more slowly (with of course the compensating advantage of guaranteeing no mistakes in the final result). A theorem prover is probably more useful for the typical IMO problem than for the typical real research problem, but even so I'd guess that even with a reasonable amount of training most IMO contestants would not do much better for having access to a theorem prover. Having three days would be a bigger deal, for sure. (But from "computers can't do this" to "computers can do this, but it takes days" is generally a much bigger step than from "computers can do this, but it takes days" to "computers can do this in seconds".)
  • golol 2y ago
    The point is not to compare AI and humans, it is to compare AI and IMO-level math problems. It's not for sport.
    • lolinder 2y ago
      They're literally comparing AI to human IMO contestants. "DeepProof solves 4/6 IMO problems correctly" would be the non-comparison version of this press release and would give a better sense for how it's actually doing.
• StefanBatory 2y ago
  Wow, that's absolutely impressive to hear! Also it's making me think that in 5-10 years almost all tasks involving computer scientists or mathematicians will be done in AI. Perhaps people going into trades had a point.
  • visarga 2y ago
    Everything that allows for cheap validation is going that way. Math, code, or things we can simulate precisely. LLM ideation + Validation is a powerful combination.
    • machiaweliczny 2y ago
      This, I've said it many years ago. Math => Code => Simulation => Robots => GG
• quirino 2y ago
  I honestly expected the IOI (International Olympiad of Informatics) to be "beaten" much earlier than the IMO. There's AlphaCode, of course, but on the latest update I don't think it was quite on "silver medal" level. And available LLM's are probably not even on "honourable mention" level. I wonder if some class of problems will emerge that human competitors are able to solve but are particularly tricky for machines. And which characteristics these problems will have (e.g. they'll require some sort of intuition or visualization that is not easily formalized). Given how much of a dent LLM's are already making on beginner competitions (AtCoder recently banned using them on ABC rounds [1]), I can't help but think that soon these competitions will be very different. [1] https://info.atcoder.jp/entry/llm-abc-rules-en https://info.atcoder.jp/entry/llm-abc-rules-en
  • oXman038 2y ago
    IOI problems are more close to IMO combinatoric problems than other IMO problem types. That might be the reason for that delay. I personally like only combinatoric problems in IMO. Thats why I drop math track and went IOI instead. I feel why combinatoric is harder for AI models is the same reason why LLM's are not great at reasoning anything out of distribution. LLM's are good pattern recognizers and fascinating at this point. But simple tasks like counting intersections at the Venn diagrams requires more strategy and less pattern recognition. Pure NN based models seem won't be enough to solve these problems. AI agents and RL are promising. I don't know anything about lean but I am curious that proof of combinatorial problems can be as well represented as number theory or algebra. If combinatorial problem solutions are always closer to natural language, the failure of LLMs are expected. Or, at least we can assume it might take more time to make it better. I am making assumption in here that solutions of combinatorial problems in IMO are more human language oriented and relies on more common sense/informal logic when it compared to geometry or number theory problems.
    • Davidzheng 2y ago
      Are you convinced there's a "reason " AI today is worse at combo? Like i don't see enough evidence that it's not an accident.
• robinhouston 2y ago
  Some more context is provided by Tim Gowers on Twitter [1]. Since I think you need an account to read threads now, here's a transcript: Google DeepMind have produced a program that in a certain sense has achieved a silver-medal peformance at this year's International Mathematical Olympiad. It did this by solving four of the six problems completely, which got it 28 points out of a possible total of 42. I'm not quite sure, but I think that put it ahead of all but around 60 competitors. However, that statement needs a bit of qualifying. The main qualification is that the program needed a lot longer than the human competitors -- for some of the problems over 60 hours -- and of course much faster processing speed than the poor old human brain. If the human competitors had been allowed that sort of time per problem they would undoubtedly have scored higher. Nevertheless, (i) this is well beyond what automatic theorem provers could do before, and (ii) these times are likely to come down as efficiency gains are made. Another qualification is that the problems were manually translated into the proof assistant Lean, and only then did the program get to work. But the essential mathematics was done by the program: just the autoformalization part was done by humans. As with AlphaGo, the program learnt to do what it did by teaching itself. But for that it needed a big collection of problems to work on. They achieved that in an interesting way: they took a huge database of IMO-type problems and got a large language model to formalize them. 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. It's not clear what the implications of this are for mathematical research. Since the method used was very general, there would seem to be no obvious obstacle to adapting it to other mathematical domains, apart perhaps from insufficient data. So we might be close to having a program that would enable mathematicians to get answers to a wide range of questions, provided those questions weren't too difficult -- the kind of thing one can do in a couple of hours. That would be massively useful as a research tool, even if it wasn't itself capable of solving open problems. Are we close to the point where mathematicians are redundant? It's hard to say. I would guess that we're still a breakthrough or two short of that. It will be interesting to see how the time the program takes scales as the difficulty of the problems it solves increases. If it scales with a similar ratio to that of a human mathematician, then we might have to get worried. But if the function human time taken --> computer time taken grows a lot faster than linearly, then more AI work will be needed. The fact that the program takes as long as it does suggests that it hasn't "solved mathematics". However, what it does is way beyond what a pure brute-force search would be capable of, so there is clearly something interesting going on when it operates. We'll all have to watch this space. 1. https://x.com/wtgowers/status/1816509803407040909?s=46 https://x.com/wtgowers/status/1816509803407040909?s=46
• deleted 2y ago
  [deleted]
• mathinaly 2y ago
  How do they know their formalization of the informal problems into formal ones was correct?
• skywhopper 2y ago
  Except it didn’t. The problem statements were hand-encoded into a formal language by human experts, and even then only one problem was actually solved within the time limit. So, claiming the work was “silver medal” quality is outright fraudulent.
  • noud 2y ago
    I had exactly the same feeling when reading this blog. Sure, the techniques used to find the solutions are really interesting. But the claim more than they achieve. The problem statements are not available in Lean, and the time limit is 2 x 4.5 hours. Not 3 days. The article claims they have another model that can work without formal languages, and that it looks very promising. But they don't mention how well that model performed. Would that model also perform at silver medal level? Also note, that if the problems are provided in a formal language, you can always find the solution in finite amount of time (provided the solution exists). You can brute-force over all possible solutions until you find the solution that proofs the statement. This may take a very long time, but it will find the solutions eventually. You will always solve all the problems and win the IMO at gold medal level. Alphaproof seems to do something similar, but takes smarter decisions which possible solutions to try and which once to skip. What would be the reason they don't achieve gold?
• t3estabc 2y ago
  [dead]
• refulgentis 2y ago
  Goalposts at the moon, FUD at "but what if its obviously fake?". Real, exact, quotes from the top comments at 1 PM EST. "I want to believe that the computer found it, but I can't find anything to confirm." "Curing cancer will require new ideas" "Maybe they used 10% of all of GCP [Google compute]"
• brap 2y ago
  Are all of these specialized models available for use? Like, does it have an API? I wonder because on one hand they seem very impressive and groundbreaking, on the other it’s hard to imagine why more than a handful of researchers would use them
  • creata 2y ago
    > it’s hard to imagine why more than a handful of researchers would use them If you could automatically prove that your concurrency protocol is safe, or that your C program has no memory management mistakes, or that your algorithm always produces the same results as a simpler, more obviously correct but less optimized algorithm, I think that would be a huge benefit for many programmers.
• gallerdude 2y ago
  Sometimes I wonder if in 100 years, it's going to be surprising to people that computers had a use before AI...
  • onemoresoop 2y ago
    If AI stays in the computer form though..
  • necovek 2y ago
    AI is simply another form of what we've been doing since the dawn of computers: expressing real world problems in the form of computations. While there are certainly some huge jumps in compute power, theory of data transformation and availability of data to transform, it would surprise me if computers in a 100 years do not still rely on a combination of well-defined and well-understood algorithms and AI-inspired tools that do the same thing but on a much bigger scale. If not for any other reason, then because there are so many things where you can easily produce a great, always correct result simply by doing very precise, obvious and simple computation. We've had computers and digital devices for a long while now, yet we still rely heavily on mechanical contraptions. Sure, we improve them with computers (eg. think brushless motors), but I don't think anyone would be surprised today about how did anyone design these same devices (hair dryers, lawn mowers, internal combustion engines...) before computers?
• Jun8 2y ago
  Tangentially: I found it fascinating to follow along the solution to Problem 6: https://youtu.be/7h3gJfWnDoc https://youtu.be/7h3gJfWnDoc (aquaesulian is a node to ancient name of Bath). There’s no advanced math and each step is quite simple, I’d guess on a medium 8th grader level. Note that the 6th question is generally the hardest (“final boss”) and many top performers couldn’t solve it. I don’t know what Lean is or how see AI’s proofs but an AI system that can explain such a question on par with the YouTuber above would be fantastic!
• pmcf 2y ago
  I read this as “In My Opinion” and really thought this about AI dealing with opinionated people. Nope. HN is still safe. For now…
• lo_fye 2y ago
  Remember when people thought computers would never be able to beat a human Grand Master at chess? Ohhh, pre-2000 life, how I miss thee.
  • utopcell 2y ago
    not to be pedantic, but Deep Blue beat Kasparov in 1997.
• michael_nielsen 2y ago
  A good brief overview here from Tim Gowers (a Fields Medallist, who participated in the effort), explaining and contextualizing some of the main caveats: https://x.com/wtgowers/status/1816509803407040909 https://x.com/wtgowers/status/1816509803407040909
• HL33tibCe7 2y ago
  This is kind of an ideal use-case for AI, because we can say with absolute certainty whether their solution is correct, completely eliminating the problem of hallucination.
• cs702 2y ago
  In 1997, machines defeated a World Chess Champion for the first time, using brute-force "dumb search." Critics noted that while "dumb search" worked for chess, it might not necessarily be a general strategy applicable to other cognitive tasks.[a] In 2016, machines defeated a World Go Champion for the first time, using a clever form of "dumb search" that leverages compute, DNNs, reinforcement learning (RL), and self-play. Critics noted that while this fancy form of "dumb search" worked for Go, it might not necessarily be a general strategy applicable to other cognitive tasks.[a] In 2024, machines solved insanely hard math problems at the Silver Medal level in an International Math Olympiad for the first time, using a clever form of "dumb search" that leverages compute, DNNs, RL, and a formal language. Perhaps "dumb search" over cleverly pruned spaces isn't as dumb as the critics would like it to be? --- [a] http://www.incompleteideas.net/IncIdeas/BitterLesson.html http://www.incompleteideas.net/IncIdeas/BitterLesson.html
  • klyrs 2y ago
    A brute force search has perfect knowledge. Calling it "dumb" encourages bad analogies -- it's "dumb" because it doesn't require advanced reasoning. It's also "genius" because it always gets the right answer eventually. It's hugely expensive to run. And you keep shifting the goalpost on what's called "dumb" here.
    • adrianN 2y ago
      You might have missed the point.
      • bdjsiqoocwk 2y ago
        Tell us what the point was, I think a lot of us are missing it.
        • BiteCode_dev 2y ago
          Moving the goal post of dumb search.
    • 2y ago
• dmitrygr 2y ago
  > First, the problems were manually translated into formal mathematical language That is more than half the work of solving them. Headline should read "AI solves the simple part of each IMA problem at silver medal level"
• ksoajl 2y ago
  [flagged]
• jerb 2y ago
  Is the score of 28 comparable to the score of 29 here? https://www.kaggle.com/competitions/ai-mathematical-olympiad-prize/leaderboard https://www.kaggle.com/competitions/ai-mathematical-olympiad...
  • Davidzheng 2y ago
    No. I would say it is more impressive than 50/50 there. (Source: I used to do math comps back in the day sorry it's not a great source)
  • gus_massa 2y ago
    IIUC the American Math Olympiad has 3 rounds. Wining the last one is almost a guaranty gold medal. The link you posted has problems with a dificulty between the first and second round that are much easier. I took a quik look at the recent list of problems in the first and second round. I expect this new AI to get a solid 50/50 points in this test.
• machiaweliczny 2y ago
  Good, now use DiffusER on algebra somehow please
• gowld 2y ago
  Why is it so hard to make an AI that can translate an informally specified math problem (and Geometry isn't even so informal) into a formal representation?
• nybsjytm 2y ago
  To what extent is the training and structure of AlphaProof tailored specifically to IMO-type problems, which typically have short solutions using combinations of a small handful of specific techniques? (It's not my main point, but it's always worth remembering - even aside from any AI context - that many top mathematicians can't do IMO-type problems, and many top IMO medalists turn out to be unable to solve actual problems in research mathematics. IMO problems are generally regarded as somewhat niche.)
  • Davidzheng 2y ago
    The last statement is largely correct (though idk what the imo medalists that are unable to solve actual problems most mathematicians can't solve most open problems). But i kind of disagree with the assessment of imo problems--the search space is huge if it were as you say it would be easy to search.
    • nybsjytm 2y ago
      No, I don't mean that the search space is small. I just mean that there are special techniques which are highly relevant for IMO-type problems. It'd be interesting to know how important that knowledge was for the design and training of AlphaProof. In other words, how does AlphaProof fare on mathematical problems which aren't in the IMO style? (As such exceptions comprise most mathematical problems)
      • Davidzheng 2y ago
        Probably less well? They rely heavily on the dataset of existing problems
• gowld 2y ago
  This shows a major gap in AI. The proofs of these problems aren't interesting. They were already known before the AI started work. What's interesting is how the AI found the proof. The only answer we have is "slurped data into a neural network, matched patterns, and did some brute search". What were the ideas it brainstormed? What were the dead-end paths? What were the "activations" where the problem seemed similar to a certain piece of input, which led to a guess of a step in the solution?
• atum47 2y ago
  Oh, the title was changed to international math Olympiad. I was reading IMO as in my opinion, haha
• thrance 2y ago
  Theorem proving is a single-player game with an insanely big search space, I always thouht it would be solved long before AGI. IMHO, the largest contributors to AlphaProof were the people behind Lean and Mathlib, who took the daunting task of formalizing the entirety of mathematics to themselves. This lack of formalizing in math papers was what killed any attempt at automation, because AI researcher had to wrestle with the human element of figuring out the author's own notations, implicit knowledge, skipped proof steps...
  • camjw 2y ago
    > Theorem proving is a single-player game with an insanely big search space, I always thouht it would be solved long before AGI. This seems so weird to me - AGI is undefined as a term imo but why would you expect "producing something generally intelligent" (i.e. median human level intelligence) to be significantly harder than "this thing is better than Terrence Tao at maths"?
    • thrance 2y ago
      My intuition tells me we humans are generally very bad at math. Proving a theorem, in an ideal way, mostly involves going from point A to point B in the space of all proofs, using previous results as stepping stones. This isn't particularly a "hard" problem for computers which are able to navigate search spaces for various games much more efficiently than us (chess, go...). On the other hand, navigating the real world mostly consists in employing a ton of heuristics we are still kind of clueless about. At the end of the day, we won't know before we get there, but I think my reasons are compelling enough to think what I think.
      • tim-kt 2y ago
        I don't think that computers have an advantage because they can navigate search spaces efficiently. The search space for difficult theorems is gigantic. Proving them often relies on a combination of experience with rigorous mathematics and very good intuition [1] as well as many, many steps. One example is the classification of all finite simple groups [2], which took about 200 years and a lot of small steps. I guess maybe brute forcing for 200 years with the technology available today might work. But I'm sceptical and sort of hope that I won't be out of a job in 10 years. I'm certainly curious about the current development. [1] https://terrytao.wordpress.com/career-advice/theres-more-to-mathematics-than-rigour-and-proofs/ https://terrytao.wordpress.com/career-advice/theres-more-to-... [2] https://en.m.wikipedia.org/wiki/Classification_of_finite_simple_groups https://en.m.wikipedia.org/wiki/Classification_of_finite_sim...
• cynicalpeace 2y ago
  Machines have been better than humans at chess for decades. Yet no one cares. Everyone's busy watching Magnus Carlsen. We are human. This means we care about what other humans do. We only care about machines insofar as it serves us. This principle is broadly extensible to work and art. Humans will always have a place in these realms as long as humans are around.
  • awahab92 2y ago
    magnus carlsen basically quit because computers ruined chess. As did kasparov. Fischer was probably the last great player who was unassisted by tools.
    • hyperbovine 2y ago
      ?? Carlsen is very much active -- look up the YouTube channel EpicChess for an extremely entertaining recap of what he's up to recently.
    • karmakurtisaani 2y ago
      Carlsen plays still at the highest level. He just didn't want to do the world championship anymore, wasn't worth the effort after winning it so many times.
  • camjw 2y ago
    Sure but if an AI can prove e.g the Goldbach conjecture then that is a bfd.
    • hyperbovine 2y ago
      What if the proof were incomprehensible to humans?
      • camjw 2y ago
        I think that is unlikely to be the case - the classic example of a proof that human's "can't understand" is the Four Colour Theorem, but thats because the proof is a reduction to like 100000 special cases which are checked by computer. To what extent is the proof of Fermat's Last Theorem "incomprehensible to humans" because only like a dozen people on the planet could truly understand it - I don't know. The point of new proofs is really to learn new things about mathematics, and I'm sure we would learn something from a proof of Goldbach's conjecture. Finally if it's not peer reviewed then its not a real proof eh.
• dan_mctree 2y ago
  I'm curious if we'll see a world where computers could solve math problems so easily, that we'll be overwhelmed by all the results and stop caring. The role of humans might change to asking the computer interesting questions that we care about.
  • klysm 2y ago
    I'm not sure what stop caring really means - like stop caring about the result, or the implications?
  • Davidzheng 2y ago
    I think mathematicians will still care
  • mr_toad 2y ago
    The next step will be having an AI come up with the problems.
• xyst 2y ago
  Billions of dollars spent building this, gW of energy used to train it. And the best it could do is “silver”? Got to be kidding me. We are fucked
• NoblePublius 2y ago
  A lot of words to say second place
• stonethrowaway 2y ago
  It’s like bringing a rocket launcher to a fist fight but I’d like to use these math language models to find gaps in logic when people are making online arguments. It would be an excellent way to verify who has done their homework.
• ezugwuernesttoc 2y ago
  [dead]
• ezugwuernesttoc 2y ago
  [dead]
• zhiQ 2y ago
  Coincidentally, I just posted about how well LLMs handle adding long strings of numbers: https://userfriendly.substack.com/p/discover-how-mistral-large-2-claude https://userfriendly.substack.com/p/discover-how-mistral-lar...
• hulitu 2y ago
  > AI solves International Math Olympiad problems at silver medal level > In the official competition, students submit answers in two sessions of 4.5 hours each. Our systems solved one problem within minutes and took up to three days to solve the others. Why not compare with students who are given 3 days to submit an answer ? /s
• lumb63 2y ago
  Can someone explain why proving and math problem solving is not a far easier problem for computers? Why does it require any “artificial intelligence” at all? For example, suppose a computer is asked to prove the sum of two even numbers is an even number. It could pull up its list of “things it knows about even numbers”, namely that an even number modulo 2 is 0. Assuming the first number is “a” and the second is “b”, then it knows a=2x and b=2y for some x and y. It then knows via the distributive property that the sum is 2(x+y), which satisfies the definition of an even number. What am I missing that makes this problem so much harder than applying a finite and known set of axioms and manipulations?
  • zone411 2y ago
    The problems in question require much, much more complex proofs. Try example IMO problems yourself and see if they don't require much intelligence: https://artofproblemsolving.com/wiki/index.php/IMO_Problems_and_Solutions https://artofproblemsolving.com/wiki/index.php/IMO_Problems_.... And then keep in mind that research math is orders of magnitude more complex still.
  • runeblaze 2y ago
    Another answer is that 3SAT and co can be seen as distilled variants of proving statements. Well, 3SAT is famously hard.
  • psb217 2y ago
    In a sense, the model _is_ simply applying a finite and known set of axioms and manipulations. What makes this hard in practice is that the number of possible ways in which to perform multiple steps of this sort of axiomatic reasoning grows exponentially with the length of the shortest possible solution for a given problem. This is similar to the way in which the tree of possible futures in games like go/chess grows exponentially as one tries to plan further into the future. This makes it natural address these problems using similar techniques, which is what this research team did. The "magic" in their solution is the use of neural nets to make good guesses about which branches of these massive search trees to explore, and make good guesses about how good any particular branch is even before they reach the end of the branch. These tricks let them (massively) reduce the effective branching factor and depth of the search trees required to produce solutions to math problems or win board games.
• zone411 2y ago
  The best discussion is here: https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning-for-Theorem-Proving https://leanprover.zulipchat.com/#narrow/stream/219941-Machi...
• data_maan 2y ago
  It's bullshit. AlphaGeometry can't even solve Pythagoras theorem. Not opensourcing anything. This is a dead end on which no further research can be built. It violates pretty much every principle of incremental improvement on which science is based. It's here just for hype, and the 300+ comments prove it.
• necovek 2y ago
  This is certainly impressive, but whenever IMO is brought up, a caveat should be put out: medals are awarded to 50% of the participants (high school students), with 1:2:3 ratio between gold, silver and bronze. That puts all gold and silver medalists among the top 25% of the participants. That means that "AI solves IMO problems better than 75% of the students", which is probably even more impressive. But, "minutes for one problem and up to 3 days for each remaining problem" means that this is unfortunately not a true representation either. If these students were given up to 15 days (5 problems at "up to 3 days each") instead of 9h, there would probably be more of them that match or beat this score too. It really sounds like AI solved only a single problem in the 9h students get, so it certainly would not be even close to the medals. What's the need to taint the impressive result with apples-to-oranges comparison? Why not be more objective and report that it took longer but was able to solve X% of problems (or scored X out of N points)?
  • muglug 2y ago
    > What's the need to taint the impressive result with apples-to-oranges comparison? Most of DeepMind’s research is a cost-centre for the company. These press releases help justify the continued investment both to investors and to the wider public.
    • utopcell 2y ago
      > Most of DeepMind’s research is a cost-centre for the company. The effect of establishing oneself as the thought leader in a field is enormous. For example, IBM's stock went up 15% the month after they beat Kasparov.
    • mensetmanusman 2y ago
      Cost centers are profit centers when R&D is successful.
  • Davidzheng 2y ago
    In my opinion (not Google s) the only reason they didn't get gold this year (apart from being unlucky on problem selection) is that they didn't want to try for any partial credit in P3 and P5. They are so close to the cut off and usually contestants with a little bit of progress can get 1 point. But i guess they didn't want to get a gold on a technicality--it would be bad press. So they settled in a indisputable silver
• dinobones 2y ago
  I see DeepMind is still playing around with RL + search algorithms, except now it looks like they're using an LLM to generate state candidates. I don't really find that this impressive. With enough compute you could just do n-of-10,000 LLM generations to "brute force" a difficult problem and you'll get there eventually.
  • richard___ 2y ago
    Sigh. Just wrong
    • dinobones 2y ago
      I'm hoping someone takes my bait and explains why MCTS + LLM is more impressive than what it sounds like.
      • utopcell 2y ago
        good luck with that.
• rich_sasha 2y ago
  I'm actually not that surprised. Maths Olympiads IME have always been 80% preparation, 20% skill - if not more heavily tuned to preparation. It was all about solving as many problems as possible ahead of the papers, and having a good short term memory. Since Olympiads are for kids, the amount of actual fundamental mathematical theorems required is actually not that great. Sounds perfect for a GPT model, with lots of input training data (problem books and solutions).
• fovc 2y ago
  6 months ago I predicted Algebra would be next after geometry. Nice to see that was right. I thought number theory would come before combinatorics, but this seems to have solved one of those. Excited to dig into how it was done https://news.ycombinator.com/item?id=39037512 https://news.ycombinator.com/item?id=39037512
• teresasovinski 2y ago
  [dead]
• gyudin 2y ago
  Haha, what a dumb tincan (c) somebody on Twitter right now :D
• imranhou 2y ago
  If the system took 3 days to solve a problem, how different is this approach than a bruteforce attempt at the problem with educated guesses? Thats not reasoning in my mind.
  • JohnPrine 2y ago
    it wouldn't surprise me if what we think of as intelligence is nothing more than brute force attempts at prediction with educated guesses
  • sigbottle 2y ago
    Because with AlphaGeometry it literally was just a feedback loop brute forcing over a known database of geometry axioms with an LLM to guide the guesses. Here, from what I understand, it's instead a theorem prover + LLM backing it. General proofs have a much larger search space than the 2d geometry problems you see on IMO; many former competitors disparage geometry for that reason.
• gerdesj 2y ago
  Why on earth did the "beastie" need the questions translating? So it failed at the first step (comprehension) and hence I think we can request a better effort next time.
• thoiwer23423 2y ago
  And yet it thinks 3.11 is greater than 3.9 (probably confused by version numbers)
• sssummer 2y ago
  Why frontier models can both achieve silver medal in Math Olympiad but also fail to answer "which number is bigger, 9.11 or 9.9"?
  • utopcell 2y ago
    ..because not all systems are of the same quality.
• lngnmn2 2y ago
  [dead]
• 1024core 2y ago
  > The system was allowed unlimited time; for some problems it took up to three days. The students were allotted only 4.5 hours per exam. I know speed is just a matter of engineering, but looks like we still have a ways to go. Hold the gong...
• _heimdall 2y ago
  I'm still unclear whether the system used here is actually reasoning through the process of solving the problem, or brute forcing solutions with reasoning coming in during the mathematical proof of each potential proof. Is it clear whether the algorithm is actually learning from why previously attempted solutions failed to prove out, or is it statistically generating potential answers similar to an LLM and then trying to apply reasoning to prove out the potential solution?
• m3kw9 2y ago
  Is it one of those slowly slowly then suddenly things? I hope so
• szundi 2y ago
  Like it understands any of it
  • johnfn 2y ago
    Do you understand any of it?
    • utopcell 2y ago
      :-) Let us support the fellow human who seems to be just at the first of the five stages of grief: denial.
• __0x01 2y ago
  Please could someone explain, very simply, what the training data was composed of?
• 0xd1r 2y ago
  > As part of our IMO work, we also experimented with a natural language reasoning system, built upon Gemini and our latest research to enable advanced problem-solving skills. This system doesn’t require the problems to be translated into a formal language and could be combined with other AI systems. We also tested this approach on this year’s IMO problems and the results showed great promise. Wonder what "great promise" entails. Because it's hard to imagine Gemini and other transformer-based models solving these problems with reasonable accuracy, as there is no elimination of hallucination. At least in the generally available products.
  • azeirah 2y ago
    I don't think that's what they mean. They explicitly stated that to achieve the current results, they had to manually translate the problem statements into formal mathematical statements: > First, the problems were manually translated into formal mathematical language for our systems to understand. How I understand what they're saying is that they used gemini to translate the problem statement into formal mathematical language and let DeepMath do it's magic after that initial step.
• Sparkyte 2y ago
  In other news today calculator solves math problem.
• djaouen 2y ago
  Is it really such a smart thing to train a non-human "entity" to beat humans at math?
• amarant 2y ago
  This is quite cool! I've found logical reasoning to be one of the biggest weak points of LLMs, nice to see that an alternative approach works better! I've tried to enlist gpt to help me play a android game called 4=10, where you solve simple math problems, and gpt was hilariously terrible at it. It would both break the rules I described, and make math mistakes, such as claiming 6*5-5+8=10 I wonder if this new model could be integrated with an LLM somehow? I get the feeling that combining those two powers would result in a fairly capable programmer. Also perhaps a LLM could do the translation step that is currently manual?
• bigbacaloa 2y ago
  [dead]
• khana 2y ago
  [dead]
• nitrobeast 2y ago
  Reading into the details, the system is more impressive than the title. 100% of the algebra and geometry problems were solved. The remaining problems are of combinatorial types, which ironically more closely resembles software engineering work.
• signa11 2y ago
  > ... but whenever IMO is brought up, a caveat should be put out: medals are awarded to 50% of the participants (high school students), with 1:2:3 ratio between gold, silver and bronze. That puts all gold and silver medalists among the top 25% of the participants. yes, it is true, but getting to the country specific team is itself an arduous journey, and involves brutal winnowing every step of the way f.e. regional math-olympiad, and then national math-olympiad etc. this is then followed by further trainings specifically meant for this elite bunch, and maybe further eliminations etc. suffice it to say, that qualifying to be in a country specific team is imho a big deal. getting a gold/silver from amongst them is just plain awesome !
  • nb_quant 2y ago
    Some countries pull these kids out of school for an entire year to focus on training for it, while guaranteeing them entry into their nation's top university. Source: a friend who got silver on the IMO
• myspeed 2y ago
  This means we may need to remove or replace the Olympiad..It has no practical significance..Winners never contributed to any major scientific breakthroughs.
  • anon2345252 2y ago
    "A number of IMO participants have gone on to become notable mathematicians. The following IMO participants have either received a Fields Medal, an Abel Prize, a Wolf Prize or a Clay Research Award, awards which recognise groundbreaking research in mathematics; a European Mathematical Society Prize, an award which recognizes young researchers; or one of the American Mathematical Society's awards (a Blumenthal Award in Pure Mathematics, Bôcher Memorial Prize in Analysis, Cole Prize in Algebra, Cole Prize in Number Theory, Fulkerson Prize in Discrete Mathematics, Steele Prize in Mathematics, or Veblen Prize in Geometry and Topology) recognizing research in specific mathematical fields. Grigori Perelman proved the Poincaré conjecture (one of the seven Millennium Prize Problems), and Yuri Matiyasevich gave a negative solution of Hilbert's tenth problem." [...] "IMO medalists have also gone on to become notable computer scientists. The following IMO medalists have received a Nevanlinna Prize, a Knuth Prize, or a Gödel Prize; these awards recognise research in theoretical computer science." https://en.wikipedia.org/wiki/List_of_International_Mathematical_Olympiad_participants#Notable_participants https://en.wikipedia.org/wiki/List_of_International_Mathemat...
  • hnfong 2y ago
    (And with this comment, the 2024 Olympics commences.) There are so many competitions that don't have any obvious practical significance. And people are still enjoying competitions where AI completely pwns humans. Also, this is probably a good time to ask whether you won the Putnam... https://news.ycombinator.com/item?id=35079 https://news.ycombinator.com/item?id=35079
  • nb_quant 2y ago
    A lot of them become Fields medallists. From [1] "The conditional probability that an IMO gold medalist will become a Fields medalist is fifty times larger than the corresponding probability for a PhD graduate from a top 10 mathematics program." [1]: https://www.aeaweb.org/articles?id=10.1257/aeri.20190457 https://www.aeaweb.org/articles?id=10.1257/aeri.20190457
• pnjunction 2y ago
  Brilliant and so encouraging! >because of limitations in reasoning skills and training data One would assume that mathematical literature and training data would be abundant. Is there a simple example that could help appreciate the Gemini bridge layer mentioned in the blog which produces the input for RL in Lean?
• quantum_state 2y ago
  It’s as impressive as if not more than AI beating a chess master. But are we or should we be really impressed?
• kerbaupapua 2y ago
  [flagged]
• hendler 2y ago
  see also https://leandojo.org/ https://leandojo.org/
• badrunaway 2y ago
  This will in a few months change everything forever. Exponential growth incoming soon from Deepmind systems.
• seydor 2y ago
  We need to up the ante: Getting human-like performance on any task is not impressive in itself, what matters is superhuman, orders of magnitude above. These comparisons with humans in order create impressive sounding titles are disguising the fact that we are still at the stone age of intelligence.
• nopinsight 2y ago
  Once Gemini, the LLM, integrates with AlphaProof and AlphaGeometry 2, it might be able to reliably perform logical reasoning. If that's the case, software development might be revolutionized. "... We'll be bringing all the goodness of AlphaProof and AlphaGeometry 2 to our mainstream #Gemini models very soon. Watch this space!" -- Demis Hassabis, CEO of Google DeepMind. https://x.com/demishassabis/status/1816499055880437909 https://x.com/demishassabis/status/1816499055880437909
• rowanG077 2y ago
  Is this just google blowing up their own asses or is this actually useable with some sane license?
• 11101010001100 2y ago
  Can anyone comment on how different the AI generated proofs are when compared to those of humans? Recent chess engines have had some 'different' ideas.
• amelius 2y ago
  How long until this tech is integrated into compilers?
• SJC_Hacker 2y ago
  The kicker with some of those math competition problems, there will be problems that reduce to finding all natural numbers for which some statement is true. These are almost always small numbers, less than 100 in most circumstances. Which means these problems are trivial to solve if you have a computer - you can simply check all possibilities. And is precisely the reason why calculators aren't allowed. But exhaustive searches are not feasible by hand in the time span the problems are supposed to be solved - roughly 30 minutes per problem. You are not supposed to use brute force, but recognize a key insight which simplifies the problem. And I believe even if you did do an exhaustive search, simply giving the answer is not enough for full points. You would have to give adequate justification.
• nsjoz 2y ago
  [dead]
• mik09 2y ago
  how long before it solves the last two problems?
• ckcheng 2y ago
  There doesn’t seem to be much information on how they attempted and failed to solve the combinatorial type problems. Anyone know any details?
  • ckcheng 2y ago
    I asked around and all I got was this: https://news.ycombinator.com/item?id=41150581 https://news.ycombinator.com/item?id=41150581