Would rewriting Linux to seL4 standards cost $16B in the world before or after frontier models are solving Erdos problems?
After. (EDIT: For the incredibly basic reason frontier models are already solving Erdos problems, but the largest LLM-based piece of system software is only borderline functional dumpster fire of a C compiler, but keep reading.)
It’s fantastically impressive that LLMs can solve Erdos problems! But:
Erdos problems are much smaller than the Linux kernel, and much easier to verify. Both these factors play to LLM strengths.
Not all Erdos problems are equally difficult. Some seem to be just difficult enough that a human would need to seriously dig in and grind it out, or bring a nice insight from a distant corner of math. Others are likely more difficult. I believe about 551/1217 are currently solved.
Reimplementing a highly-secure kernel that could replace Linux for most uses cases is an enormous project with many poorly defined subtasks, which is basically hell for LLMs. The biggest LLM project I’m aware of is a C compiler. Which basically works, but which is apparently a remarkably terrible C compiler. And C is far, far better specified than the internal guts of Linux and all the ghastly hardware that Linux supports.
Also, please keep in mind that I’m willing to handwave a couple of zeros either way on the larger estimates.
I expect overall security of newly written code to get clearly worse on average (thanks to the deprofessionalization of software development and companies pushing vibeslop to production) right up until offensive Mythos-class abilities become widespread. Then I expect things to get unpleasantly exciting.
After. (EDIT: For the incredibly basic reason frontier models are already solving Erdos problems, but the largest LLM-based piece of system software is only borderline functional dumpster fire of a C compiler, but keep reading.)
It’s fantastically impressive that LLMs can solve Erdos problems! But:
Erdos problems are much smaller than the Linux kernel, and much easier to verify. Both these factors play to LLM strengths.
Not all Erdos problems are equally difficult. Some seem to be just difficult enough that a human would need to seriously dig in and grind it out, or bring a nice insight from a distant corner of math. Others are likely more difficult. I believe about 551/1217 are currently solved.
Reimplementing a highly-secure kernel that could replace Linux for most uses cases is an enormous project with many poorly defined subtasks, which is basically hell for LLMs. The biggest LLM project I’m aware of is a C compiler. Which basically works, but which is apparently a remarkably terrible C compiler. And C is far, far better specified than the internal guts of Linux and all the ghastly hardware that Linux supports.
Also, please keep in mind that I’m willing to handwave a couple of zeros either way on the larger estimates.
I expect overall security of newly written code to get clearly worse on average (thanks to the deprofessionalization of software development and companies pushing vibeslop to production) right up until offensive Mythos-class abilities become widespread. Then I expect things to get unpleasantly exciting.