AI solves International Math Olympiad problems at silver medal level

Post by klyrs » Thu, Jul 25, 2024, 6:16 PM UTC

cs702 wrote: post #177

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

Post by TheDudeMan » Thu, Jul 25, 2024, 6:16 PM UTC

cs702 wrote: post #177

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

Post by adrianN » Thu, Jul 25, 2024, 6:17 PM UTC

klyrs wrote: post #181

cs702 wrote: post #177

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

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.

Post by [deleted] » Thu, Jul 25, 2024, 6:19 PM UTC

nnarek wrote: post #53

ocfnash wrote: post #40

Earlier quoted context omitted.

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.

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

Post by adrianN » Thu, Jul 25, 2024, 6:22 PM UTC

thrdbndndn wrote: post #180

thomasahle wrote: post #145

Earlier quoted context omitted.

You'd think that, but Timothy Gowers (the famous mathematician they worked with) wrote ( 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 auto…

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