Post #4193744

2026-07-29 10:35 UTC

(sorry, I somehow flubbed my keyboard and posted this half-finished, so I deleted it) an important thing to understand here is that software like theorem provers were designed around the assumption that the user cares about getting a correct answer, and wouldn't intentionally sabotage themselves by leaning into obscure, buggy behavior but AIs are the proverbial "nasal demons" of programming lore at their most manifest: you said you needed this theorem proved; it will "prove" the theorem at any cost, because the AI itself doesn't know or care about the beauty of mathematical truth, it cares about you clicking the button that indicates you were satisfied with its output today and are likely to pay for more tokens in the future The metaphor of "nasal demons" was invented to teach new programmers about the dire meaning of "undefined behavior": asking the compiler to do something it doesn't have exhaustively clear rules for, so it will do... something. Do nothing at all for one cycle, perhaps. Delete the hard drive, perhaps. Summon demons to pour out of your nose, perhaps. This is of course an absurdly impossible example to get you to remember it, but the point is: if your program causes undefined behavior, it is entirely possible something you don't expect and won't enjoy will happen. LLMs are nasal demons. They do not have exhaustively clear rules for anything: they wing it, all of it, all the time. Asking it to interface with a complex system with hidden bugs and find a miracle solution will cause results that you, as the entity that actually cares about the result being correct, will not enjoy. :neodog_devil:

Replies (5)

@david_chisnall@infosec.exchange 2026-07-29 13:16

@0xabad1dea@infosec.exchange an important thing to understand here is that software like theorem provers were designed around the assumption that the user cares about getting a correct answer This is also a property of compilers. No one (with the possible exception of CakeML) has successfully written a compiler that can treat the programmer as an adversary. This was one of the goals of Java: the compiler generates bytecode, which has some formally verified properties. This is then checked by a verifier and run through a JIT compiler. Java Applets were explicitly sold as using this to be able to sandbox Java: you can load Java and sandbox it and it's safe. Only it didn't work. JREs were so complicated that they had bugs. And these bugs led to sandbox escapes. The same thing happened with ActionScript (Flash) and JavaScript. Modern browsers no longer treat the JavaScript VM as a defensible boundary. They assume an attacker can escape from the JavaScript sandbox and get control over the renderer process, which they treat as the defensible boundary. The Rust core team is also explicit about this. Rust doesn't guarantee any of the nice type system properties against an a programmer who is actively trying to break them. The type system and borrow checker are tools for programmers to help them write code with entire bug categories eliminated (which is enormously valuable). They are not tools that are designed to guarantee that someone who can provide arbitrary text going into the compiler can't do malicious things (and there are over a hundred bugs in the rustc issue tracker marked 'soundness' that can lead to malicious code breaking some of the guarantees).

Open ##4199195
@sabrina@fedi01.unicornsparkle.club 2026-07-29 10:49

@0xabad1dea@infosec.exchange I like that term, nasal demons. I used to say that the full problem space of software testing included making sure that there wasn’t a scenario that caused lawn gnomes to start pouring out of the CD drive. Which is of course an impossible test and yet you can’t say testing is complete unless you’ve covered that scenario. It’s an idea meant to convey the infinite problem space of software testing. Nice to know there’s a concept out there closely related to my own.

Open ##4200217
@s_wilson@mastodon.uno 2026-07-29 11:16

@0xabad1dea@infosec.exchange Just like humans, but with even messier incentives

Open ##4200219
@fl0und3r@defcon.social 2026-07-29 13:11

@0xabad1dea@infosec.exchange imagine a future where AI "solves" math that nobody understands, but don't worry, it's been verified by code that nobody understands and was probably written by AI anyway. Maybe this will happen before we all get paved over to make room for data centers

Open ##4200220
@0xabad1dea@infosec.exchange 2026-07-29 14:46

I'm going to mute this thread because I spent an unhealthy amount of time attempting to resolve a claim that one of my statements was wrong, with the conclusion "I really don't think I'm wrong, but can't conclusively prove it with a smoking gun quote". This is a summary of the dispute: 1) my claim was that the OP of the LLM-generated buggy proof did not know it was buggy when they posted it, and was misled by the LLM but was acting in good faith. 2) Someone counterclaims that the OP of the buggy proof knew perfectly well that it was buggy when they posted it (because they are an expert on theorem provers in general), yet chose not to disclose this up-front and let everyone else figure it out. I think 2) sounds like a rather dickish thing to do, but also, going over the github issues, community threads etc, everything reads to me as if the OP sincerely did not realize it was buggy when they posted it, but is gladly cooperating with figuring out and fixing all the bugs uncovered so this won't happen again. HOWEVER, if you have proof that OP knew it was buggy when they posted it and chose not to say anything up front, feel free to link it and others can check the replies. I don't think it materially changes the point that an LLM can come up with solutions that really seem like they check out but are relying on devastating bugs in other software that you won't spot.

Open ##4208531