True they do technically sell gaming GPUs however I believe Nvidia paid more in taxes than they made from their "gaming" sector. I say "gaming" because I believe they roll it in with other things in their "edge computing" category. All this is off the top of my head so it could be wrong. Here is their Q2 results if you are curious: https://nvidianews.nvidia.com/news/nvidia-announces-financia...
Fascinating read, thanks! The counterpoint to "slaughtering the golden goose" is: If you're all in with AI, this is the rational thing to do, no?
If AI takes over, search becomes irrelevant, so better extract as much value from search as possible while it's decaying and not dead yet.
The thing that I've not fully groked here (might be relevant) is that OAI is generating "paper" proofs first, and only then formalizes them in Lean as a separate step.
They've as far as I'm aware not said anywhere how many write ups failed formalization due to a bug in the proof. If we assume that number is low, models would be quite good at one-shotting math proofs. Then it depends if you can replicate the math RL training for chemistry/biology/medicine. Is there enough data out there for that? No idea.
I'm seeing estimates of a %95-91 failure rate on attempts in generally (or, conversely, a max of ~10% success, but likely lower, since we can only go based on how many attempts they are willing to mention in their statements). E.g., from analysis in https://medium.com/@mehmet.ozel2701/openai-tried-about-4-000...
I wonder how many of those founder at the "paper" to formalization step, or at earlier or later steps (e.g., proof doesn't turn out to prove what the paper said, hits a bug in the kernel, etc.).
based on how bad these models are at one-shotting complex real-world software engineering problems -- it always has to be a conversation -- there is absolutely no way they're one-shotting complex math proofs.
Also, goes without saying, but put Sam Altman in jail, obviously.
Wow. Complexity class separations are really really rare.
Can an expert in sat solving comment if there's any immediate applications of the method from the paper? Or is SAT solving in general pretty far away from worst-case times, and this is a theoretical algorithm which would be hard to apply in practice.
SAT-solving expert here. No immediate applications (the results in the paper are "galactic"). The main question is whether some ideas here will snowball into other ideas, one of which could eventually be very practical.
This is a complete non-sequitur, but I checked out your web page. I love the Curious George image. My daughter has been deeply into the Curious George episodes for the past couple of months, and I don't think I've seen him show up in many other places besides kids' shows :D
Galactic algorithms have such huge constants they figuratively need a galaxy-sized computer and/or galaxy-sized problem, to have any advantage over the normal solutions. Imagine a generic sorting algorithm in O(n) that had a constant of 10^92 **. Technically superior but in practice unusable.
There are realistic situations where galactic O(n) sorting algorithms exist, right? 32-bit integers can be sorted in O(n) using 2^32 words of memory, using bucket sort[1].
If objects have a maximum size of 4 GB (= 2^35 bits), then arbitrary objects can be sorted in O(n) using 2^2^35 bits of memory.
You can use Radix sort https://en.wikipedia.org/wiki/Radix_sort to lower the memory requirement for limited bit-width integers. But there are more practical o(n log n) methods for sorting integers.
Well optimized radix sorts are actually pretty fast (assuming you have the proper fallbacks to quicksort/insertion sort to deal with medium/small sizes)
> A galactic algorithm is an algorithm with state-of-the-art theoretical (asymptotic) performance, but which is not used due to practical constraints.
Yes, I think we can pretty safely say that the algorithm in the paper is not used due to practical constraints. This is a subjective judgment, but pretty clear from the paper that the algorithms aren't practical to apply.
The data you put into a SAT solver has substantial effect on it's performance in practice. Real world inputs tend to be much nicer than pathological ones, so I don't think there's much practical application, but I also haven't read the paper yet.
I'm curious, why would this not turn into an unlimited electricity flatrate? In most parts of the world, consumer electricity is charged by kWh, not as flat payment.
As long as tokens are as energy intense to compute as they are right now, I don't see a flatrate being a viable model.
Something close to how we rent other cloud resources today makes sense. We don't worry about electricity costs, it's built into the hourly prices, use as much of the hardware as you can. Electricity rates vary over the course of the day as well.
People don't like complex pricing. This would be for businesses running larger workloads. For individuals, the unlimited plan seems the most probable to me. This stuff is going to get real cheap in the coming years.
The energy needed per token is in dropping rapidly, even though the energy per-GPU is going up. We are seeing something like 10x improvements per year.
What I think the parent post is missing is that breakthroughs in science don't immediately translate into breakthroughs in engineering and even less so into economically viable products.
The distinction for many people is that math and cs feel like very natural domains for LLMs (and importantly, domains that enable quick iteration and verification). Much less applicable with eg biology and other fields that require lots of physical experimentation.
(in)Conveniently those are also the fields where most ordinary people would experience the most effects from accelerated progress. Dario famously promises potential cures for cancer and dementia.
I think there's a pretty clear distinction between math and science. The former builds theoretical models of what certain axioms and assumptions imply. The latter builds actual models of what we see and measure in the real world.
Advances in math will probably result in advances in science, which in turn will result in advances in engineering (which is probably where the average person sees an actual benefit in their day to day life). But it's not automatic and a lot of the hand wringing by mathematicians about the AI math results include "is this (AI) method of finding proofs actually going to result in as many of those downstream advances as the old fashioned way?"
(I include theoretical CS as a subfield of math - and believe the S in it is a misnomer).
I have a feeling that many more fields are utilizing AI and having some success with it and we just don't know about it in our STEM bubble.
On the other hand, you could downplay the math findings a bit, since it didn't further our understanding of mathematics just yet, only provided proves to things we didn't have proves for.
It's really funny how the server that Jev pushes from the footbridge onto the tracks in one of the later examples falls on a person, yet all 5 are saved :D
Clearly the model coming up with the graphics didn't fully understand the task.
I'd add missing MFA as weakness number three, at minimum.
Problem number 4 is that the "password" was leaked, and the company (Pays ApS) didn't figure that out.
Problem number 5 - the "password" belonged to a _former_ employee. How was that account not disabled?
Problem number 6 - how can a company with two employees get access to this register in the first place? Don't they need to show compliance with some security standard that would be not possible to deliver for such a small company?
If you start thinking more about this, more and more problems pop up.
I thought they're still selling gaming GPUs? What did I miss?
reply