As most of you know, openAI has recently showcased o3's SOTA results on various benchmarks. In my opinion FrontierMath was the hardest of the bunch, and it was reflected in model performance as the SOTA was 2% before Friday. It also seems to be the benchmark with the least visibility. To set the scene, Chollet and the ARC-AGI group were very forthcoming with their thoughts on o3's performance, and even published the model training set and the results on github. People have got a chance to engage with the training set, and even argue potential ambiguities. The upshot of this discussion is that there is a lot of data surrounding the ARC-AGI benchmark.
OTOH, there is a dearth of discussion wrt FrontierMath. I think people genuinely don't understand the benchmark, and get oneshotted by the hard math problems it advertises. I understand that people see the jump from 2% -> 25% as impressive, and I do too. I am just not sure at what we're actually measuring, or whether models are actually getting better at math. It's for a very simple reason: coming up with an answer is the easy part, coming up with a solution is the hard part.
I'm not sure if people know, but Elliot Glazer has actually commented on the old 2% SOTA in an AMA on reddit:
I don't find that there is are 3 tiers of problems to be an issue at all, other than openAI has not (to my knowledge) published which tier of problems o3 has solved. Moreover, models are not actually required to "understand" the problem and the solution to come up with an answer. Thus, it's not clear to me that the increased FrontierMath SOTA represents such a large increase in the mathematical capabilities of the models. There is a severe lack of qualitative review of the reasoning traces of o3, and it just seems like people are uncritically accepting the increased performance without questioning what it actually represents.
I of course understand that there is a need for privacy with these models - if the problems get published then the benchmark will be soiled. I think this is a sign that FrontierMath is ultimately not a good benchmark for truly measuring math ability of models. I don't get why there needs to be a middleman in the form of a benchmark. Actually, this has been discussed by Elliot Glazer:
To be blunt, I don't think these are very good reasons for FrontierMath as 1. Why do we need to estimate the difficulty of open problems? There is a common sentiment in math that there are "no low hanging fruit" and there is some truth to this claim. Open problems sit at the cusp of math knowledge these days, so unless you're highly specialized you're probably not finding + solving them. If a model can solve any open problem, regardless of "difficulty", then it has proved its capability. In short, this requirement seems contrived.
2. (Apologies, I get a bit more pie in the sky here.) The reasons for not having FM be proof-based are as follows:
The first point seems weak, as you could argue that doing math is a skill rather than a reflection of "genuine reasoning skills". The second point strikes a pet peeve of mine: the overreliance of Lean in the broad math community. It seems to be the only proof assistant that people know. I don't particularly like it, nor do I like Coq, as these proof assistants feel a little alien compared to how I actually do math. The missing undergraduate math topics in Lean:
seem to reflect a fundamental difference between the proof assistant and doing actual math. All of this should be easy to do in Lean. In all honesty, a motivated highschooler should be able to formalize these concepts. In reality, they can do it for low dimensional matrices but cannot generalize the operations to arbitrary dimensions. I think the only explanation of this is sunk-cost fallacy. There are people working today on better languages for doing math. I am sure many of you roll your eyes at "homotopy type theory". I am extremely bullish on its younger but burgeoning sibling: directed type theory. In particular, something like a directed higher inductive type makes it way more logical to describe categorical structure that exists in matrices. The author of this thesis uses untyped lambda calculus as an example of structure that can be modeled with DHITs. If you understand what he's saying, you can very quickly imagine that it wouldn't be much work to model matrices and other 1-categorical objects. Unfortunately, it doesn't exist yet. Thankfully, people are working on that!
All in all, I really wish that people were a little more critical on FrontierMath for no other reason than an eagerness to push the boundaries on human knowledge to the limit. Part of that, though, requires participation on part of openAI to be completely forthcoming about their performance on benchmarks. A simple bar graph like this: doesn't really cut it for me. It doesn't have to, of course.
1. Why do we need to estimate the difficulty of open problems? There is a common sentiment in math that there are "no low hanging fruit" and there is some truth to this claim. Open problems sit at the cusp of math knowledge these days, so unless you're highly specialized you're probably not finding + solving them. If a model can solve any open problem, regardless of "difficulty", then it has proved its capability. In short, this requirement seems contrived.
Roughly, it's because in order for a benchmark to be useful at identifying practical AI capabilities, then we need the benchmark to neither be too easy nor too hard.
For example, if the statement to be proved is say independent of ZFC, then no computer that can be computed from a Turing Machine (which includes all LLMs) can resolve the conjecture, and due to independent statements, you can make conjectures that are arbitrarily hard to solve, and even the non-independent conjectures may in practice be unsolvable by any human or AI for a long time, which means the benchmark is less useful for real AIs.
The first point seems weak, as you could argue that doing math is a skill rather than a reflection of "genuine reasoning skills".
I actually agree with this, though in a way, you can have both holding at once.
The second point strikes a pet peeve of mine: the overreliance of Lean in the broad math community. It seems to be the only proof assistant that people know. I don't particularly like it, nor do I like Coq, as these proof assistants feel a little alien compared to how I actually do math. The missing undergraduate math topics in Lean:
While I am not experienced at all in formalizing math, and thus am willing to update and be corrected by any expert on mathematics, especially those that formalize mathematics in proof assistants, I'd expect 2 language independent reasons for why formalizing mathematics in proof assistants are difficult:
There just aren't that many people that want to formalize mathematics by default, compared to doing something else.
It's hard to formalize the details, because in a math paper, you can get away with being a little informal (though still pretty rigorous), and in particular you can elide away details that you have to explicitly do if you want to formalize a proof, and the skill of paying attention to details that matter when formalizing a proof aren't usually good enough to make formalizing proofs be natural for a lot of mathematicians.
To be clear, maybe these reasons are wrong, and I'm willing to accept correction, but this would be my view on why formalizing undergraduate mathematics is hard.
I agree there should be something closer to a naturalistic benchmark like proving conjectures, though confounds are going to be a problem if you go that route.
