11–20 of 177 posts
Not to pick on this guy, but this is ridiculous goal post shifting. It's just astounding what people will hand-wave away as not requiring intelligence.
> Note that the performance of GPT-4 performance on IMO problems can also be contaminated by public solutions in its training data.
Doesn't anybody proofread in Nature?
“What the I.M.O. is testing is very different from what creative mathematics looks like for the vast majority of mathematicians,” he said. --- Not to pick on this guy, but this is ridiculous goal post shifting. It's just astounding what people will hand-wave away as not requiring intelligence.
An analogy with software is that math competitions are like (very hard) leetcode.
There was an article posted on HN recently that is related: https://benexdict.io/p/math-team
“What the I.M.O. is testing is very different from what creative mathematics looks like for the vast majority of mathematicians,” he said. --- Not to pick on this guy, but this is ridiculous goal post shifting. It's just astounding what people will hand-wave away as not requiring intelligence.
It isn't untrue, but both are considered metrics by the community. (Whether rightfully or not seems irrelevant to ML).
Interesting that the transformer used is tiny. From the paper: "We use the Meliad library for transformer training with its base settings. The transformer has 12 layers, embedding dimension of 1,024, eight heads of attention and an inter-attention dense layer of dimension 4,096 with ReLU activation. Overall, the transformer has 151 million parameters, excluding embedding layers at its input and output heads. Our cust…
From the Nature article: > Note that the performance of GPT-4 performance on IMO problems can also be contaminated by public solutions in its training data. Doesn't anybody proofread in Nature?
From the Nature article: > Note that the performance of GPT-4 performance on IMO problems can also be contaminated by public solutions in its training data. Doesn't anybody proofread in Nature?
Though this particular model doesn't sound generalizable, the neuro-symbolic approach seems very promising to me: - linking the (increasingly powerful) "system 1" tools that are most of current ML with more structured "system 2" tools, like logical proof generation, which can plan and and check the veracity / value of output. - System 2 chugs along 'till it gets stuck, then system 1 jumps in to provide an intuitive g…
You do not need to solve everything at once. This approach has the potential to revolution both math and programming by moving formal verification from being a niche tool into a regular part of every practitioners toolbox.
It also completely solves (within the domain it applies) one of the most fundamental problems of AI that the current round is calling "hallucinations"; however that solution only works because we have a non AI system to prove correctness.
At a high level, this approach is not really that new. Biochem has been using AI to help find candidate molecules, which are then verified by physical experimentation.
Combinatorical game AI has been using the AI as an input to old fasion monte carlo searches