821–830 of 1001 posts
Earlier quoted context omitted.
Recursive self improvement of their upcoming IPO value maybe. They are fluffy PR pieces otherwise.
How can you possible say this sort of thing in context of what looks like a millenium prize being solved. I swear there's nobody blinder than those who won't see.
I think this is clear evidence that AI models are now at the far frontier of mathematics innovation and discovery and exceed human limits. This specific problem having had a $1 million bounty on its head and still remaining unsolved for 26 years after the bounty was placed is pretty clear evidence that many of the world's best human mathematicians would have solved this problem if they could have, and none were able…
Here you go: When you read the detail the compute they are throwing at it is incredible, tens of thousands of agents with different groups competing. It's not like a single Gauss as you imply, "just" many, many mathematicians working tirelessly in a completely ego-less way, guided by other agents and ultimately humans, built - allegedly - on recent human insights. Stunning, undoubtedly, but this is a "brilliant autis…
I slightly disagree. A single LLM is equally 'mindless' as a herd of them. As anyone will tell you they "simply predict the most likely next token," yet, complex solutions to difficult problems arise from them.
Many people have said that the architecture of LLMs will need to change for true ASI. I think that the herd of tens of thousands of agents can be seen as one such potential architectural extension. Whether or not a herd or a single LLM is used for a result like this is irrelevant.
To be clear, I think the orchestration of thousands of LLMs in their current form, even with ever increasing intelligence, is not the form ASI will take. There is still a major architectural breakthrough to come, in my limited, ignorant opinion.
> We’re sharing a solution to the Navier–Stokes existence and smoothness problem, one of the Millennium Prize Problems. This proof, produced by an internal OpenAI system, shows that the dynamics of the Navier-Stokes equations for fluid motion can develop a singularity in finite time. We’re sharing both a writeup of the proof and a formalization in Lean. WOW?
> WOW This. I do dislike the AI oligarchs as much as the next person, but I do find the thread full of complaining a bit depressing still. If the result holds (and it looks it does), this may be one of the, if not the, biggest things to happen in computing to date. A lot bigger than e.g. Deep Blue beating Kasparov in chess or AlphaGo beating Sedol in Go.
what would have happened if they didn't do this? they could have done things the right way. we could celebrate this achievement.
perhaps they could have taken just a few weeks, even, to work out something with buckmaster and apoge.
i am very concerned that this is a glimpse of things to come. a malign elite with powerful ai, who will turn the sublime of technology into barbarity, violence and human oppression.
if sam altman has destroyed openai's public benefit corp with lesser tools why would he aid humanity with even greater power?
I'm only half joking. Should researchers perhaps put hashes of their attempts on a public blockchain tied to their own public keys, verify their claims asynchronously, and then whoever reveals the first believable attempt gets the credit?
I know some people started doing this years ago but now it might need to become standard practice.
> We’re sharing a solution to the Navier–Stokes existence and smoothness problem, one of the Millennium Prize Problems. This proof, produced by an internal OpenAI system, shows that the dynamics of the Navier-Stokes equations for fluid motion can develop a singularity in finite time. We’re sharing both a writeup of the proof and a formalization in Lean. WOW?
> WOW This. I do dislike the AI oligarchs as much as the next person, but I do find the thread full of complaining a bit depressing still. If the result holds (and it looks it does), this may be one of the, if not the, biggest things to happen in computing to date. A lot bigger than e.g. Deep Blue beating Kasparov in chess or AlphaGo beating Sedol in Go.
People are not complaining about problems being solved or advancement in technology. They are complaining about terrible people doing terrible things.
I think this is clear evidence that AI models are now at the far frontier of mathematics innovation and discovery and exceed human limits. This specific problem having had a $1 million bounty on its head and still remaining unsolved for 26 years after the bounty was placed is pretty clear evidence that many of the world's best human mathematicians would have solved this problem if they could have, and none were able…
>If anyone has counterpoints to this I'd love to hear them! Sure. A proof without an unknown amount of human steering (and/or stolen research) would be an unquestionable achievement. To this day there's zero (0) evidence of any result by an LLM alone (maybe I'm wrong). If I just prompt ChatGPT right now with "give me a proof of the Riemann Hypothesis" and this thing delivers, I'm sold. But anything close to "yeah Cha…
I think the counterpoint here is simply to look at what was being achieved with LLMs one year ago versus today, and extrapolate that trend. Sure, there may not be examples of what you've asked for yet, but Astra is literally a couple of months old, the model that solved Navier-Stokes is less than two weeks old. It appears that we're seeing the hockey stick that only the most bullish thought was possible.
Earlier quoted context omitted.
Yeah I'm surprised they posted a chart, you would think they would keep specifics like that hidden until they're closer to launch
The chart is as non-specific as could be. It improved in some very vague metric by some amount at different (increasing) levels of training.
Earlier quoted context omitted.
>there's still the problem of does this logical result actually prove the initial question that was asked? In math, the question being asked is the validity of a logical statement. That is, there is some rigorous, logical statement which may or may not be true (or even provable, etc.), and the question is whether or not it is actually true or false (or even provable, etc.). Having a proof, fundamentally, means you ha…
I was thinking something along the lines of making a mistake when inputing the initial statement, like you wanted to prove that '2 is even' but what you actually stated was that '3 is odd'. Of course in this simple example it's obvious, but my assumption was that these machine generated lean proofs are millions of lines of code and who knows what they actually say..
[0] https://github.com/openai/NavierStokesAndEuler/blob/main/Com...
Earlier quoted context omitted.
Even under your interpretation, OAI pushed a button and solved NS. Yes, that is very impressive. Are you kidding me? Imagine building an automated system that can solve NS.
That's not my interpretation - that is literally what OpenAI say in that press release.
Earlier quoted context omitted.
With Lean, math has become a really well suited problem for LLMs. We will likely see large gains for many years from here, just doing more and more rlvr, like continuously, non stop. No need to train from scratch. It really doesn't speak to the general intelligence of models though. It does speak to how good these things can become when a problem space has verifiable rewards, especially when you can verify one step a…
It's crazy how deep Microsoft's bench is (Lean was started there, vscode is another), for everything not directly related to the the ai models (hell, even github for data). So interesting how everything played out, I remember in the early days when MS came out with the partnership with OpenAI it seemed like they were playing 5d chess and were poised to win big. And it all just fizzled out. Second biggest fumble after…