11 ms·

The newest models are solving some of the hardest Math Olympiad problems [1]. This is in the top 1% of the top 1% math students out of high school. The math pe

The newest models are solving some of the hardest Math Olympiad problems [1]. This is in the top 1% of the top 1% math students out of high school. The math performance, even for VERY hard problems, is already getting extremely good and progress is still high year-on-year. What OpenAI (and everyone else, less publicly) seem to be doing, is to integrate these kinds of abilities into multi-modal models. https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/ https://deepmind.google/discover/blog/ai-solves-imo-problems...

imtringued 2y ago
Yeah sure, but AlphaProof is "cheating", because they are using an external system to do the hard work and the LLM is just there for translation and semantic information retrieval. As impressive as it is, it makes LLMs look like they are just a fancy UI. Like, you can tell the computer to press the upvote button in English using your voice instead of using your mouse. It's the same with AlphaProof. The LLM is just taking a problem specification in natural language and then acting as the UI of the theorem prover. The moment you talk about using LLMs to solve decidable problems, people whip you with the idea that you should let the LLM generate python code. Aka, the LLM is just a fancy UI for specifying python programs in English. Cool, but also somewhat hollow. It's no different than having a translator from one language to another.
aithrowaway1987 2y ago
It seems misleading to lump AlphaGeometry in with this: that system works by having an LLM generate hundreds of Lean programs and trying to find the one that works. Frankly the project is pointless and borderline dishonest: it is a hideously expensive way to solve useless Olympiad problems, but it won't work at all for actual mathematical research since we wouldn't have nearly enough training data. It does not represent even the slightest advancement at AI performing mathematics, it's pure gimmickry. I suspect the entire point of AlphaGeometry is to generate comments like yours, "AI is now an Olympian-level mathematician." The real AI math advancement will be a computer which is as smart as a pigeon and innately understands what a number is, which means it is able to solve simple counting problems without training. AlphaGeometry or Strawberry aren't even close to that, and I suspect none of us will live to see such a sophisticated AI.

imtringued 2y ago

Yeah sure, but AlphaProof is "cheating", because they are using an external system to do the hard work and the LLM is just there for translation and semantic information retrieval. As impressive as it is, it makes LLMs look like they are just a fancy UI. Like, you can tell the computer to press the upvote button in English using your voice instead of using your mouse. It's the same with AlphaProof. The LLM is just taking a problem specification in natural language and then acting as the UI of the theorem prover. The moment you talk about using LLMs to solve decidable problems, people whip you with the idea that you should let the LLM generate python code. Aka, the LLM is just a fancy UI for specifying python programs in English. Cool, but also somewhat hollow. It's no different than having a translator from one language to another.

aithrowaway1987 2y ago

It seems misleading to lump AlphaGeometry in with this: that system works by having an LLM generate hundreds of Lean programs and trying to find the one that works. Frankly the project is pointless and borderline dishonest: it is a hideously expensive way to solve useless Olympiad problems, but it won't work at all for actual mathematical research since we wouldn't have nearly enough training data. It does not represent even the slightest advancement at AI performing mathematics, it's pure gimmickry. I suspect the entire point of AlphaGeometry is to generate comments like yours, "AI is now an Olympian-level mathematician." The real AI math advancement will be a computer which is as smart as a pigeon and innately understands what a number is, which means it is able to solve simple counting problems without training. AlphaGeometry or Strawberry aren't even close to that, and I suspect none of us will live to see such a sophisticated AI.