Eh. This entire tweet smacks of being AI generated. It has a huge amount of LLM-isms.
I wouldn't be surprised if Sacks just prompted an LLM to just come up with whatever rebuttal to whatever the regulation side comes up (given the big set of regulation tweets) with sounds most convincing, given his usual anti-regulation stance.
Even better, Sacks admitted in response to a Pangram check that he has an LLM line edit his posts (https://x.com/DavidSacks/status/2099040321351106807). (He claims, bizarrely, that this means Pangram is "bogus" rather than accurate.)
The structure of Lean does impose that. The code isn't being run, it's being type checked. And that's it. The overwhelming majority of Lean code is never run. It exists only to be type checked (because type checking is equivalent to verifying the proof).
You could imagine the typechecker has bugs (and indeed another comment mentions examples of bugs!). Crucially though anytime the typechecker has a bug fixed you could rerun the typechecker on the code to see if it still type checks.
This is the whole promise of formal verification. It reduces the problem of verification purely to the typechecker. If the typechecker is correct, then the proof is verified, no matter how many lines of code the proof is. As a sibling comment puts it, the chance of bugs mainly scales with the number of lines of code in the typechecker, not in the amount of lines of Lean code.
Your question is akin to asking, "yes this spellchecker ran fine on your essay, but are you sure it runs fine on War and Peace? That's 1000x more words!" To which the answer is the number of words doesn't matter if the spell checker is correct (which it might not be! And longer passages might reveal more bugs! But you can always rerun it). The main source of bugs is more lines of code in the spell checker, not in number of words in the text.
> Astra’s progress helps clarify which AI capabilities are out of reach and which questions remain open.
Okay. But I don't think this entire article at all explained which AI capabilities remain out of reach. Did I miss something? Other than "oh I guess it could still get even more superhuman on ARC-AGI-3 than it is?"
> It’s highly nontrivial to verify that a 250k loc Lean program actually represents that which it claims.
Generally you only need to look at 10-100 lines (unless you have a highly novel theorem that essentially invents a new field of math or builds on a field that has never been worked on in Lean before) of the 250k to verify what it claims. This is why there is excitement around formal verification. The rest of it is perhaps useful to read to figure out why the proof works, but is not necessary for checking.
That paper has had a pretty turbulent reception and looks pretty conclusively wrong at this point.
It used an incorrect theoretical framing that assumed that data was being replaced rather than accumulated as a result of more training (see https://arxiv.org/abs/2404.01413 which explores this). This is incorrect because this simply isn't how real-world datasets are created via synthetic data generation (which generally accumulate more data over time rather than replace their data). As a result most of the theoretical results were invalid.
Empirical evidence has also cast a considerable amount of doubt on the paper. For example, Microsoft Phi-4 was an empirical test in specifically what happens if the majority of your training data is synthetic rather than human and it turns out that Phi-4 did significantly better than previous models which relied primarily on human data.
There's some nuance to all of this in how exactly you do this, but the original claims of the paper are looking really shaky at this point.
> GPT-4(?) was capable of beating Pokemon 18 months ago but models only became capable of beating it without a harness in the last six months...?
GPT-4 was decidedly not capable of beating Pokemon 18 months ago. I doubt it would be able to complete a single level. I don't think people realize how large the advances in model capabilities have been. GPT-4 in a modern harness is absolutely horrendous compared to modern models.
Yes. Presumably you're referring to my use of the word "level". I mean here basically every "level" as denoted by the order of locations and places on the town map that you get (which is usually +- some other locations how game runners refer to different sections of the game).
There's a deep irony that all of these "anti-doom" pieces are entirely AI generated.
reply