I want to know:
1. How many total problems were given to the model, and what percent were left unsolved at what cost before giving up? 2. How many attempts did you give the model at solving these problems? 3. How expensive was the harness, e.g. did the model have access to a job cluster?
Another question I have is whether or not OpenAI 'simply' hired capable combinatorics researchers to work on problems, and they have, and the use of the model is incidental / secondary to their work.
A couple small ones that I've seen (example here [0]), but not anything of the magnitude that OpenAI and Anthropic have put out. Likely just related to token limits.
> Another question I have is whether or not OpenAI 'simply' hired capable combinatorics researchers to work on problems, and they have, and the use of the model is incidental / secondary to their work.
I think their output has reached a level that precludes this possibility, but I of course don't have any hard proof.
[0]: https://www.reddit.com/r/math/comments/1uxj3cy/after_openais...
My point here is to not snark. But there should be some level of self skepticism that doesn’t warrant an RCT theatre.
AI has no self-awareness. It's a tool. When you assemble a furniture using a screw driver, the torque force interacts with the molecular forces inside the metal and miraculously it transfers the force to the screw though a clever geometry design, communicating the force to the screw to turn it in a certain way.
Do you attribute the build to the tool? The "system's contribution" is helped by many other things all the way down to chips, datacenters and power generation. If the authorship requires attributing to a tool, then it should happen all the way down.
Now I understand that it’s mostly the super stars benefitting from the increased attention. Folks who are less established don’t share in that glory. But on the other hand it seems like an exciting time to go even deeper for in various specialties of math by deciding where to focus these powerful tools. For every conjecture defeated some seven or eight new ideas open up. Our path through that combination will be set by creative and curious human mathematicians.
[edit: deleted a distracting comparison to Chess]
Which is very suggestive - if after everything they are not fully loaded then the next gazillion data centres being built look unlikely to be needed.
> We helped prepare the manuscripts and formalize the proofs in Lean, and we take responsibility for their correctness
Offering to take responsibility for the correctness of a proof written in Lean feels like volunteering to be the fall guy in case someone finds a flaw in basic arithmetic, no?
https://leanprover.zulipchat.com/#narrow/channel/270676-lean...
Edit: Oh, are you suggesting they just use it to privately improve their models? I imagine a few more correct proofs would have a very marginal benefit, if any. Also, they'll probably just get extracted, meaning it still gets out but OpenAI doesn't get to fancily announce it themselves.
This was not a problem that was for sale
A slightly smarter highschooler could write these. I could write these. It's clear as day that the LLM, not the human, did the heavy lift. It'd be ridiculous to give full credit to whoever wrote the prompt.
[0]: Not one of the proofs in the linked article, but from OpenAI too.
I think you're over-estimating what a smarter highschooler could write.
A "finite loopless undirected multigraph" could have been explained to me at that age if we'd taken Discrete rather than Mechanics and Pure (and one module of Stats) in my two A-levels* in maths and further maths; but from what I saw of the Discrete module, neither:
Every finite loopless multigraph with no bridge possesses a cycle double cover, without additional assumptions such as cubicity, planarity, connectivity, or higher edge-connectivity.
repeated-edge closed trails masquerading as cycles
* For those not from the UK: A-levels are between secondary school and university, when aged 16-18. Functionally they are university entrance qualifications: https://en.wikipedia.org/wiki/A-level_(United_Kingdom)
Provability is just going the way of computation. John Napier had to manually compute logarithm tables over decades and was recognised for his work; now that same work could be performed by a 10 year old with a calculator in an evening.
> In particular, proofs for special graph classes, constructions of cycle covers with some edges covered other than twice, bounded-length or prescribed-cycle variants, reductions to another unproved conjecture, computational verification through any fixed graph size, and candidate counterexamples without a complete nonexistence certificate are insufficient.
which is infact a very important part of the prompt.
When the tool is a 3D printer, or any CNC system really, you bet I attribute a build to it.
I could also attribute the operator; there is no contradiction, it's a free choice, just like saying "I am in Berlin" does not contradict "I am in Germany".
What is your mechanistic model of self awareness that yields this conclusion?
> It's a tool
Does your model suggest that tools can't have self awareness?
A language model (or an image model or whatever) cannot even be sentient, and I think sentience is a prerequisite for awareness.
Even if we express a lot of our subjective experience with words, the language is just a symbolic representation of those experiences. The qualia themselves, even those that are quite abstract, are rooted in our physical presence and evolution.
You can't have an understanding of what hunger or physical pain feel like if you have no need for food or a sensory capacity for feeling pain. You can't understand what loneliness or pride at an achievement mean if you don't have a neural network wired to value social connection or status. We value connection because we're social animals that have needed each other for survival.
Even the more abstract of our subjective experiences are in some way rooted in our physical evolution.
I see no reason to believe that a neural network built entirely based on the symbolic level of language could have the features needed for the subjective experience itself.
AI awareness might actually be more believable if that awareness manifested itself in an entirely different way than in humans. But if we assume awareness because outputs resemble what we consider meaningful as humans, yet the neural network has had no inputs or evolution that could form the actual basis of human-like experience, I think we're seeing something that isn't actually there.
(*) Even if we hack around this and just do the usual trick of simply laundering statefulness to a higher level, in this case the context window being fed in, I fail to identify (**) a representation of its own state in these bodies of text that it'd be meticulously maintaining. I further fail to identify how it could be hidden or maintained, considering I control like half of it. The best you could ascribe it is a meticulous maintenance of a persona the user is talking to, but then that doesn't necessarily represent the model's internal state, the same way my own words here aren't doing so either. Difference being, I actually have one (I'm "on-line").
You'll sometimes catch models mixing up who's who and how many who-s there even are for example.
(**) I did wish for something hidden though, so maybe it's just concealed? The same way people can encode a lot more of their emotional and mental state than normal into text if they read and write a lot of it, I'm aware of research that suggested the same for LLMs, albeit I cannot cite it. Maybe those phrasing signatures are just alien to me and will never pop out. Either way, I'd expect researchers to stumble upon this during interpretability studies, and either they haven't, they have but it wasn't popsci adopted, or they're keeping awfully tight lipped about it. If you know of anything like this, your turn now, would be happy to learn.
I do wonder how reasonable it is to expect e.g. a single maintained identity though. Maybe it isn't?
(*) Another way to hack around this of course is to just precompute some internal "self-awareness states" and hop around between them. Probably the closest to what the models are actually "doing".
The most disappointed folks will simply drop out, but the enthusiastic ones will keep going and with luck make up for the ones who decided to quit. Chess and go certainly went this way.
If you translate that to math, then all you get is math competitions, not math as a career. Of course the translation isn't nearly exact ... there's a lot more room for professional mathematicians because the math space is far more vast than the chess space and can't generally be cranked out mechanically (we have proof).
P.S. The response is nonsense ... I explained exactly why it's awful (others have too) and the response doesn't in any way refute the explanation ... rather it offers up a ridiculous strawman.
[0]: e.g. "go through wikipedia's unsolved math problem list and solve them".
> a hidden representation of self that is continually tended to
This sounds like a personality? They act like they have one of those. It may be an illusion, and even if it isn't an illusion it is unlikely to be anything like the source (us), but they act like it.
> I further fail to identify how it could be hidden or maintained, considering I control like half of it.
Indeed you control everything about a local model, and much of the context of even a remote model. But the state of activations and circuits in SotA AI is hidden in similar ways to those of synapses in your head: difficult to decipher even with probes monitoring the signals directly, and often not emitted at the normal output.
> The best you could ascribe it is a meticulous maintenance of a persona the user is talking to, but then that doesn't necessarily represent the model's internal state, the same way my own words here aren't doing so either. Difference being, I actually have one (I'm "on-line").
While we can be confident that LLMs make up personas etc., it is insufficient to go from "that doesn't necessarily represent the model's internal state" to "therefore it doesn't have one".
> You'll sometimes catch models mixing up who's who and how many who-s there even are for example.
I've, unfortunately, also experienced this with humans. Perhaps they were losing their self-awareness at the time? I do wonder if old-age dementia does that by the end, though the person in question didn't ever get diagnosed with that.
> If you know of anything like this, your turn now, would be happy to learn.
Do you mean like these, or something else?
• https://researchportal.hkust.edu.hk/en/publications/decoding...
As I currently understand it, all we know is that:
- a mathematician produced a Lean-verified counterexample to the Collatz conjecture, demonstrating a bug in the kernel
- he claims that LLMs were involved somehow but pointedly refuses to specify how
- he admits that he knew about the bug before publishing the counterexample to his repository.
Perhaps not a joke (although it sure seems to me like they discovered a bug and thought falsely disproving the Collatz conjecture would be a flashy way to announce it), but at best extremely sensationalized by the above description. If you have additional context I would be happy to hear it!
It's a marketing post from a huge company. Only the naive would view it uncritically without assuming it's been written carefully to present the results in the best possible light while skirting the boundaries of outright lying.