There’s an easy way to turn any mathematical answer-based benchmark into a proof-based benchmark and it doesn’t require coq or lean or any human formalization of the benchmark design: just let the model choose whether or not to submit an answer for each question, and score the model zero for the whole benchmark if it submits any wrong answers.
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.
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.
I don't believe this is true, actually! What do you mean by "resolve the conjecture"? If you mean write up with a proof of it, then of course you can write a turing machine that will write a proof of the conjecture, it's just infinite monkeys. ZFC is best thought of as the "minimal set of axioms to do most math". It's not anything particularly special. You can have various foundations such as ETCS, NF, Type theory, etc. If we have a model that can genuinely reason mathematically, then the set of axioms the model uses should be immaterial to its mathematical ability. In fact, it should certainly be able to handle more or less axioms, like replacing full choice with countable choice etc. Maybe I misunderstood your point here.
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:
But my point was that there are things that should be extremely easy, like proving lemmas about elementary row transformations, that have not been done in Lean yet. That is not due to a lack of people formalizing, but due to fundamental limitations with the proof assistant. The point that I'm failing to make explicit is that this seems like a copout. The ultimate naturalistic benchmark for an LLM's math ability is being able to formalize the undergraduate math curriculum! But it starts with having a proof assistant that is amenable to the formalization project, which seems to be the bottleneck today.
I don't believe this is true, actually! What do you mean by "resolve the conjecture"? If you mean write up with a proof of it, then of course you can write a turing machine that will write a proof of the conjecture, it's just infinite monkeys. ZFC is best thought of as the "minimal set of axioms to do most math". It's not anything particularly special. You can have various foundations such as ETCS, NF, Type theory, etc. If we have a model that can genuinely reason mathematically, then the set of axioms the model uses should be immaterial to its mathematical ability. In fact, it should certainly be able to handle more or less axioms, like replacing full choice with countable choice etc. Maybe I misunderstood your point here.
My point was to gesture at the fact that open conjectures can be so hard that neither humans nor AI can solve them in reasonable time, and that it's too hard to determine whether a conjecture is even provable by an AI or human in reasonable time, so the proving open conjectures benchmark is not a great benchmark, and I was using independence of ZFC as an example of such conjectures.
Also, a Turing Machine in that case (where a statement is independent but not recursively independent) will only prove independence from ZFC, not a proof or disproof of the conjecture.
But my point was that there are things that should be extremely easy, like proving lemmas about elementary row transformations, that have not been done in Lean yet. That is not due to a lack of people formalizing, but due to fundamental limitations with the proof assistant. The point that I'm failing to make explicit is that this seems like a copout. The ultimate naturalistic benchmark for an LLM's math ability is being able to formalize the undergraduate math curriculum! But it starts with having a proof assistant that is amenable to the formalization project, which seems to be the bottleneck today.
I definitely would think that formalizing an entire undergraduate math curriculum would be a great benchmark, but it would have to be designed very carefully to ensure the LLM doesn't break the benchmark's usefulness.
Also, when you state that it's extremely easy to formalize certain lemmas/theorems, are you saying that it's easy to formalize them flat out, including all necessary details, or are you saying that it's easy to give a paper that would be accepted by mathematicians, and if necessary (though the journey may be painful) you could formalize the argument, including all necessary details?
Bonus question: What do you think are the current limitations of proof assistants such as Lean, more specifically?
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.
