So, a proposal: Whenever someone claims that LLMs will d/acc us out of AI takeover by fixing our infrastructure, they will also have to specify who will pay the costs of setting up this project and running it.
I’m almost centrally the guy claiming LLMs will d/acc us out of AI takeover by fixing infrastructure, technically I’m usually hedging more than that but it’s accurate in spirit.
If transformative AI is developed soon, most open source projects (especially old ones relevant to internet infrastructure) are going to be maintained by humans with human response times. That will significantly increase the time for relevant security patches to be reviewed and merged into existing codebases, especially if at the time attackers will submit AI-generated or co-developed subtle exploits using AI systems six to nine months behind the leading capabilities, keeping maintainers especially vigilant.
I usually say we prove the patches correct! But Niplav is correct: it’s a hard social problem, many critical systems maintainers are particularly slop-phobic and won’t want synthetic code checked in. That’s why I try to emphasize that the two trust points are the spec and the checker, and the rest is relinquished to a shoggoth. That’s the vision anyway– we solve this social problem by involving the slop-phobic maintainers in writing the spec and conveying to them how trustworthy the deductive process is.
Niplav’s squiggle model: Median $~1b worth of tokens, plus all the “setting up the project, paying human supervisors and reviewers, costs for testing infrastructure & compute, finding complicated vulnerabilities that arise from the interaction of different programs…” etc costs. I think a lot’s in our action space to reduce those latter costs, but the token cost imposes a firm lower bound.
But this is an EA Forum post, meaning the project is being evaluated as an EA cause area: is it cost effective? To be cost effective, the savings from alleviating some disvalue have to be worth the money you’ll spend. As a programming best practices chauvinist, one of my pastimes is picking on CrowdStrike, so let’s not pass up the opportunity. The 2024 outage is estimated to have cost about $5b across the top 500 companies excluding microsoft. A public goods project may not have been able to avert CrowdStrike, but it’s instructive for getting a flavor of the damage, and this number suggests it could be easily worth spending around Niplav’s estimate. On cost effectiveness though, even I (who works on this “LLMs driving Hot FV Summer” thing full time) am skeptical, only because open source software is pretty hardened already. Curl/libcurl saw 23 CVEs in 2023 and 18 in 2024, which it’d be nice to prevent but really isn’t a catastrophic amount. Other projects are similar. I think a lot about the Tony Hoare quote “It has turned out that the world just does not suffer significantly from the kind of problem that our research was originally intended to solve.” Not every bug is even an exploit.
I’m almost centrally the guy claiming LLMs will d/acc us out of AI takeover by fixing infrastructure, technically I’m usually hedging more than that but it’s accurate in spirit.
I’m happy this is reaching exactly the right people :-D
As for proving invariances, that makes sense as a goal, and I like it. If I perform any follow-up I’ll try to estimate how much more tokens that’ll produce, since IIRC seL4 or CakeML had proofs that exceeded 10× the length of their source code.
A recent experience I’ve had is to try and use LLMs to generate Lean definitions and proofs for a novel mathematical structure I’m toying with, they do well with anything below 10 lines but start to falter with more complicated proofs, and sorry their way out of anything I’d call non-trivial. My understanding is that a lot of software formal verification is gruntwork but there also needs to be interwoven moments of brilliance.
I’m always unsure what to think of claims that markets will incentivize the correct level of investment in software security. Like, initial computer security in the aughts seems to me like it was actually pretty bad, and while it became better over time it did take at least a decade. From afar, markets look efficient, from close up you can see efficiency establish itself. And then it’s the question how much of the cost is internalized, which I feel for private companies should be close to 100%? For open source projects of course that number then goes close to zero.
It’d be cool to see a time series of the number of found exploits in open source software, thanks for the curl numbers. You picked a fairly old/established codebase with an especially dedicated developer, I wonder what it’s like with newer ones, and whether one discovers more exploits in the early, middle, or late stage of development. The adoption of better programming languages than C/C++ of course helps.
Lean synthesis capabilities aren’t maximally elicited right now, because a lot of people view it as a text-to-text problem which leads to a bunch of stress about low amount of syntax in the pretraining data and the high code velocity (until about a year ago, language models still hadn’t fully internalized migrations from Lean3 to Lean4). Techniques like Cobblestone or the stuff that Higher Order Company talks about (logic programming / language model API call hybrid architecture) seem really promising to me (and, especially as HOC points out, so much cheaper!).
Thanks for your comment. I had broken my ankle in three places and was on too much oxycodone to engage the first time I read it. I continue to recommend your essay a lot.
Remark in guaranteed safe AI newsletter:
Niplav writes
I’m almost centrally the guy claiming LLMs will d/acc us out of AI takeover by fixing infrastructure, technically I’m usually hedging more than that but it’s accurate in spirit.
I usually say we prove the patches correct! But Niplav is correct: it’s a hard social problem, many critical systems maintainers are particularly slop-phobic and won’t want synthetic code checked in. That’s why I try to emphasize that the two trust points are the spec and the checker, and the rest is relinquished to a shoggoth. That’s the vision anyway– we solve this social problem by involving the slop-phobic maintainers in writing the spec and conveying to them how trustworthy the deductive process is.
Niplav’s squiggle model: Median $~1b worth of tokens, plus all the “setting up the project, paying human supervisors and reviewers, costs for testing infrastructure & compute, finding complicated vulnerabilities that arise from the interaction of different programs…” etc costs. I think a lot’s in our action space to reduce those latter costs, but the token cost imposes a firm lower bound.
But this is an EA Forum post, meaning the project is being evaluated as an EA cause area: is it cost effective? To be cost effective, the savings from alleviating some disvalue have to be worth the money you’ll spend. As a programming best practices chauvinist, one of my pastimes is picking on CrowdStrike, so let’s not pass up the opportunity. The 2024 outage is estimated to have cost about $5b across the top 500 companies excluding microsoft. A public goods project may not have been able to avert CrowdStrike, but it’s instructive for getting a flavor of the damage, and this number suggests it could be easily worth spending around Niplav’s estimate. On cost effectiveness though, even I (who works on this “LLMs driving Hot FV Summer” thing full time) am skeptical, only because open source software is pretty hardened already. Curl/libcurl saw 23 CVEs in 2023 and 18 in 2024, which it’d be nice to prevent but really isn’t a catastrophic amount. Other projects are similar. I think a lot about the Tony Hoare quote “It has turned out that the world just does not suffer significantly from the kind of problem that our research was originally intended to solve.” Not every bug is even an exploit.
I’m happy this is reaching exactly the right people :-D
As for proving invariances, that makes sense as a goal, and I like it. If I perform any follow-up I’ll try to estimate how much more tokens that’ll produce, since IIRC seL4 or CakeML had proofs that exceeded 10× the length of their source code.
A recent experience I’ve had is to try and use LLMs to generate Lean definitions and proofs for a novel mathematical structure I’m toying with, they do well with anything below 10 lines but start to falter with more complicated proofs, and
sorrytheir way out of anything I’d call non-trivial. My understanding is that a lot of software formal verification is gruntwork but there also needs to be interwoven moments of brilliance.I’m always unsure what to think of claims that markets will incentivize the correct level of investment in software security. Like, initial computer security in the aughts seems to me like it was actually pretty bad, and while it became better over time it did take at least a decade. From afar, markets look efficient, from close up you can see efficiency establish itself. And then it’s the question how much of the cost is internalized, which I feel for private companies should be close to 100%? For open source projects of course that number then goes close to zero.
It’d be cool to see a time series of the number of found exploits in open source software, thanks for the
curlnumbers. You picked a fairly old/established codebase with an especially dedicated developer, I wonder what it’s like with newer ones, and whether one discovers more exploits in the early, middle, or late stage of development. The adoption of better programming languages than C/C++ of course helps.Lean synthesis capabilities aren’t maximally elicited right now, because a lot of people view it as a text-to-text problem which leads to a bunch of stress about low amount of syntax in the pretraining data and the high code velocity (until about a year ago, language models still hadn’t fully internalized migrations from Lean3 to Lean4). Techniques like Cobblestone or the stuff that Higher Order Company talks about (logic programming / language model API call hybrid architecture) seem really promising to me (and, especially as HOC points out, so much cheaper!).
Thanks for your comment. I had broken my ankle in three places and was on too much oxycodone to engage the first time I read it. I continue to recommend your essay a lot.
Yeah, I goofed by using Claude for math, not any of the OpenAI models, which are much better at math.