[dead]
AI solves International Math Olympiad problems at silver medal level
551–560 of 564 posts
Re: AI solves International Math Olympiad problems at silver medal level
#552Earlier quoted context omitted.
Could you explain where the 40x speedup comes from, given that literally the biggest problem in semi conductors right now is smaller node size?
Improved parallelization. More cost in less time. This is Nvidia's main area of research now.
Still, very marginal improvements. There is also Amdahl’s Law which limits the speed gains of parallelisation.
Re: AI solves International Math Olympiad problems at silver medal level
#553Earlier quoted context omitted.
What makes solving IMO problems hard is usually the limits of human memory, pattern-matching, and search, not creativity. After all, these are problems that are already solved, and it is expected that many people can solve the problems in about 1 hour's time. That makes it, in principle, similar or even easier than a champsionship-level chess move, which often take more than 1 hour for a professional human (with more…
Ok but if you read the actual solutions they aren't a bizarre mess of brute force. They look like what a human would write if they were trying to come up with a formal proof (albeit it does some steps in a weird order).
They are, though. I spoke to an author just yesterday. They did mostly use brute-force.
Re: AI solves International Math Olympiad problems at silver medal level
#554Earlier quoted context omitted.
Yes, but the problem space means that invalid outputs can be quickly identified - whereas general programming isn’t necessarily amenable to rapid checks.
I mean, aren’t you just describing formal language syntax? Seems like a fundamentally similar situation —- the computer can automatically flag any syntax errors in a millisecond by checking it against the generating grammar for that language. Thats what makes a formal language in the first place, I think! I do think this language is considerably more robust than the typical programming language, which means a sound p…
I don’t mean syntax errors - I mean the difficulty of validating code that contains side effects (like http requests, database access etc).
Validating a math proof either terminates in a reasonable time (in which case it’s useful for training), or does not (in which case the AI should be discouraged from using that approach).
Re: AI solves International Math Olympiad problems at silver medal level
#555how long before it solves the last two problems?
Re: AI solves International Math Olympiad problems at silver medal level
#556Earlier quoted context omitted.
> I am quite confident that this formalisation failure mode is not hard to solve in a system that is, like, actually trained to do this. Why?
This is really not the kind of problem LLMs are bad at! But since you insist, given the LaTeX, Claude 3.5 Sonnet correctly stated the theorem in full while inventing notation for the floor operation (it did correctly note unprompted what the right function was and how to obtain it from mathlib, but it incorrectly attempted to define syntax sugar for it).
The hard part isn't getting the formalisation right sometimes, it's getting it right reliably (and unlike mistakes in the formal part, there's no way for the system to check itself in that part).
IDK, even for translation between languages outside of mathematics, missing small qualifiers that change the whole meaning of the sentence is a worrying failure mode I've seen, and with mathematical problems there are a lot more cases like that.
Re: AI solves International Math Olympiad problems at silver medal level
#557Earlier quoted context omitted.
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.
The useful thing about proofs is that they are written in English (or another language), not formal logic. In general they can be mapped to formal logic, though. This means that people can digest them on an intuitive level. The actual goal of a proof is to create new knowledge (via the proof) which can be distributed across the mathematical community. If proofs exist but are not easily comprehensible, then they don’t…
If a proof is understandable only by a few people in the world, I would say it fails as a proof, according to your definition. There are many such proofs out there right now. It doesn't help that many of them are wrong, albeit usually in a fixable way.
Making a proof formal doesn't mean it is not understandable any more. First, certainly a machine can "understand" it now. I think with AI improving what exactly such an understanding is worth, and what you can do with it, will increase a lot.
Secondly, the inscrutable tactics-based proofs featured in Lean (I have written such proofs in Isabelle in 1996) are actually quite old-fashioned for such a "modern" prover. Isabelle has long featured human-friendly syntax, and these proofs are certainly as understandable as English text, if written with care.
What we will soon get are proof assistants which allow you to write your proofs (and definitions) in English, but which are still fully formal and checkable. That is an immense help if you are producing new knowledge, because usually nobody else looks at your work with sufficient scrutiny in the first place. If you understand it, and in addition the machine "understands" it, I think that will be the gold standard for proofs very soon.
It will also help mathematicians to clean up their act ;-)
Re: AI solves International Math Olympiad problems at silver medal level
#558Earlier quoted context omitted.
What observation, if you saw it, do you think would falsify that hypothesis?
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 milest…
Thursday question seems fine for me… but I have different standard questions that do fail, e.g. non-Euclidian triangles:
https://chatgpt.com/share/b657f0cd-34f9-4f5c-8ac9-c3a06c7101...
Re: AI solves International Math Olympiad problems at silver medal level
#559Earlier quoted context omitted.
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.
Formalization is mechanical work, lets leave it for computers to do :)
I completely agree
Re: AI solves International Math Olympiad problems at silver medal level
#560Earlier quoted context omitted.
The AI took a day on one of the problems so it must have generated and discarded a lot of proofs that didn't work. How could it choose which one to submit as the answer, except the objective fact of the proof passing in Lean.
To some extent, what they do is stronger that the other contestants, who I understand don’t formally prove their answers.
In maths, you are only solving a problem by building a formal solution that is the proof.
Eg. if it asked you to do something computationally hard (when done in a brute force way: calculators not allowed), and you put out the answer without the process using formal math knowledge, you'd get zero points. Even if it was easy to prove the answer was correct.
That's why IMO and many math exams won't take a single answer even if correct.