5 ms·
The problems were first converted into a formal language. So they were partly solved by the AI
by petters 2y ago
The problems were first converted into a formal language. So they were partly solved by the AI
- jeremyjh 2y agoYes 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 agoEven so, having a human formalize the problems and an AI to find machine checkable proofs could be very useful for mathematicians.
- sebzim4500 2y agoIt 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 agoDisagree! Some problems are much harder than others. If you don't believe me please go formalize P5 in this year imo.
- sebzim4500 2y agoYeah, I was just referring to the problems that it actually did.
- SonOfLilit 2y agoI 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 agoI find it incredibly impressive you did this in 15 minutes! You should really help out in formalizing math (completely serious). Personally in the past I tried a few times to formalize some statements and sometimes I found that the mathlib libraries were pretty lacking in these more open-ended problems (I wanted to reason about lists and stuff). But it seems that I am just very bad at formalization lol.
- SonOfLilit 2y agoFormalization is mechanical work, lets leave it for computers to do :)
- Davidzheng 2y agoI completely agree
- rpois 2y agoDoes this formalization process include giving it the answer it should try to prove?
- Smaug123 2y agoNope, per Oliver Nash who worked on the thing: https://news.ycombinator.com/item?id=41070372 https://news.ycombinator.com/item?id=41070372
- deleted 2y ago[deleted]
- clbrmbr 2y agoIIUC, a Gemini-based system could translate the natural language questions into Lean, but in the blog post they don’t really commit to whether this was done just to generate training data or was used in the competition.
- deleted 2y ago[deleted]
- cygaril 2y agoFormalizations for the competition were done by hand.
- golol 2y agoFormalization is in principle just a translation process and should be a much simpler problem than the actual IMO problem. Besides, they also trained a Gemini model which formalizes natural language problems, and this is how they generated training data for AlphaProof. I would therefore expect that they could have also formalized the IMO problems with that model and just did it manually because the point is not to demonstrate formalizing but instead proof capabilities.
- riku_iki 2y ago> Formalization is in principle just a translation process and should be a much simpler problem than the actual IMO problem maybe not, because you need to connect many complicated topics/terms/definitions together, and you don't have a way to reliably verify if formalized statement is correct. They built automatic formalization network in this case, but didn't trust it and formalized it manually.
- pishpash 2y agoYet the facts at hand are the opposite of what you say. Reliable formalizer was the more difficult problem than solving formalized IMO problems, because they have not produced one.
- fngjdflmdflg 2y agoThat does not necessarily follow from the facts at hand. For example they may have prioritized work on the proof solver itself as they may feel that that is the more important result. Alternatively if their goal is to build a proof solver then building the formalizer would be useless if they could not build the actual proof solver.
- pishpash 2y agoA proof solver existed. They were improving the proof solver explicitly by making the formalizer a part of the training. Formalizer reliability is the key novelty. It turns out it was only reliable enough for training. So unless they made the problem statement at the outset that "we'll only make the formalizer strong enough to train but not use", I disagree with that assessment.
- trotro 2y agoBut formalization is the easy part for humans. I'm sure every mathematician would be be happy if the only thing required to prove a result was to formalize it in Lean and feed it to the AI to find the proof.
- Davidzheng 2y agoNot sure every mathematician would be happy to do this... it sounds much less pleasant than thinking. It's like saying mathematicians would rather be programmers lol. It's a significant difficult problem which i believe should be left completely to AI. Human formalization should become dead