AI solves International Math Olympiad problems at silver medal level

Post by adroniser » Fri, Jul 26, 2024, 12:24 PM UTC

sapiogram wrote: post #479

cubefox wrote: post #466

Earlier quoted context omitted.

So finding Lean proofs can be conceptualized as a zero-sum game? Another basic requirement is that valid moves / inference steps and the winning condition can be efficiently verified using some non-AI algorithm. Otherwise there would not be a reward signal for the reinforcement learning algorithm. This is different from answering most natural language questions, where the answer can't be checked trivially.

I don't think AlphaZero is related to this work, apart from both being NN-based. AlphaZero and its training pipeline fundamentally only works for "chess-like" two-player games, where the agent can play against itself and slowly improve through MCTS.

Post by SonOfLilit » Fri, Jul 26, 2024, 12:37 PM UTC

Davidzheng wrote: post #342

sebzim4500 wrote: post #289

Earlier quoted context omitted.

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.

Disagree! Some problems are much harder than others. If you don't believe me please go formalize P5 in this year imo.

  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'  2023 or py'  2025:
                illegal
            (k, F, px', py', m + {((px, py), F)})

Post by HarHarVeryFunny » Fri, Jul 26, 2024, 12:54 PM UTC

camjw wrote: post #235

thrance wrote: post #230

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 wi…

> 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"?

Post by password54321 » Fri, Jul 26, 2024, 1:06 PM UTC

balls187 wrote: post #248

password54321 wrote: post #202

Earlier quoted context omitted.

> need to hold companies accountable by very transparently disclosing those energy costs. And if they do, then what? If it is "too high" do we delay research because we need to keep the world how it is for you? What about all the other problems others face that could be solved by doubling down on compute for AI research?

> And if they do, then what? If it is "too high" do we delay research because we need to keep the world how it is for you? First, it's keeping the world how it is for all of us , not just me. Second, to answer you question, I think that is a decision for all of us to weigh in on, but before we can do that, we must be informed as best as we can. Do sacrifices have to be made for the greater good? Absolutely. Do for-pr…

Post by cweld510 » Fri, Jul 26, 2024, 1:38 PM UTC

auggierose wrote: post #395

cynicalpeace wrote: post #326

Earlier quoted context omitted.

No. Funny how these discussions too often devolve into semantics lol.

Funny how people don't understand basic logic. If it is a proof in a logic, and the machine checked that proof, it is a proof, no matter that no human actually understands it. A human doesn't need to understand the proof, they just have to understand why the proof is a proof.