Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

AI solves International Math Olympiad problems at silver medal level

deepmind.google

Post reply on HN
Print view View original

521–530 of 564 posts

Re: AI solves International Math Olympiad problems at silver medal level

#521

Post by Thorrez »

_heimdall wrote: post #504
Thorrez wrote: post #428

Earlier quoted context omitted.

This quote from the article sounds like it learns from failed tests: >We trained AlphaProof for the IMO by proving or disproving millions of problems, covering a wide range of difficulties and mathematical topic areas over a period of weeks leading up to the competition. The training loop was also applied during the contest, reinforcing proofs of self-generated variations of the contest problems until a full solution…

Reading between the lines a bit, that does answer the question I had though don't think I I clarified very well. I read that to say the model's token weights are adjusted as it goes, so in an LLM sense it is kind of learning. It isn't reasoning through an answer in the way a human does though. Meaning, the model is still just statistically predicting what an answer may be and checking if it worked. I wouldn't chalk t…

>with a similar number of failed attempts as a human

I'd be hard to know how many failed attempts the human made. Humans are constantly thinking of ideas and eliminating them quickly. Possibly to fast to count.

Re: AI solves International Math Olympiad problems at silver medal level

#522

Post by balls187 »

password54321 wrote: post #497
balls187 wrote: post #248

Earlier quoted context omitted.

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

Many people don't want to live in the world how it is. They would rather see risks taken for accelerated progress. Stop trying to pretend your take is the humanitarian take.

> Many people don't want to live in the world how it is.

Got a source to support your assertion that many people are okay with the effects of climate change?

https://www.scientificamerican.com/article/more-climate-laws...

> Stop trying to pretend your take is the humanitarian take.

That's a straw man. However, I cannot believe many humans are in support of an uninhabitable world.

Re: AI solves International Math Olympiad problems at silver medal level

#523

Post by cynicalpeace »

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.

We just have different definitions of what a proof is. Hence, semantics.

Re: AI solves International Math Olympiad problems at silver medal level

#524

Post by Davidzheng »

SonOfLilit wrote: post #493
Davidzheng wrote: post #342

Earlier quoted context omitted.

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

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…

I 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.

Re: AI solves International Math Olympiad problems at silver medal level

#525

Post by JohnPrine »

imranhou wrote: post #396

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.

it wouldn't surprise me if what we think of as intelligence is nothing more than brute force attempts at prediction with educated guesses

Re: AI solves International Math Olympiad problems at silver medal level

#528

Post by sigbottle »

osti wrote: post #18

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.

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.

Re: AI solves International Math Olympiad problems at silver medal level

#529

Post by sigbottle »

imranhou wrote: post #396

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.

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.

Re: AI solves International Math Olympiad problems at silver medal level

#530

Post by osti »

sigbottle wrote: post #528
osti wrote: post #18

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.

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

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.

Post reply on HN