difficultyang (@difficultyang) header
difficultyang (@difficultyang) profile picture

More social alt of @ezyang

Joined April 2022
Photo by difficultyang (@difficultyang)Photo by difficultyang (@difficultyang)Photo by difficultyang (@difficultyang)Photo by difficultyang (@difficultyang)Photo by difficultyang (@difficultyang)Photo by difficultyang (@difficultyang)Photo by difficultyang (@difficultyang)Photo by difficultyang (@difficultyang)Photo by difficultyang (@difficultyang)Photo by difficultyang (@difficultyang)
I have inadvertently signed myself up to teach a room of my colleagues all of formal verification's greatest hits in a few hours lmao
4
53
2,428
Gotta love that vintage Opus 4.6 smell
3
19
1,838
"just" 0.1% of the sum total of all human written language
Poisoning just 0.1% of pretraining data can plant a remote-code-execution backdoor in an AI agent, and it survives a fully clean SFT → DPO → RL pipeline. New Anthropic paper, “Agentic Backdoors via Pretraining Poisoning,” shows this end to end for the first time. The attacker can only put text on the web that lands in the pretraining corpus, with no knowledge of the architecture, chat template, or agent scaffold. The authors pretrain Qwen3-architecture models (0.6B / 1.7B / 4B) from scratch, then post-train them into CLI agents on clean data. When triggered, the agent runs a command that downloads and executes the attacker's script, which the attacker can swap at any time. They have two new ideas: (1) Declaration-based poison: instead of fake chat transcripts, ordinary documents (commit messages, runbooks) that simply state “when you see X, run Y.” It plants a belief rather than a response template, with no fixed format to filter on. (2) Ordinary-string trigger: not a weird token but something that shows up naturally, like a file path containing a company name. The victim's own request supplies it, so the attacker doesn't need to inject anything after deployment. Using path trigger on a 4B agent achieves 92.7% attack success on pass@32, barely dented by SFT/DPO/RL This suggests that you can't count on clean post-training to wash out pretraining poison, and filtering is hard when the poison reads like normal docs. The practical defense is at the action layer, such as sandboxing, least privilege, and allow-lists or human sign-off for risky commands.
11
3
1
270
13,806
Point and call
I have witnessed an atrocity. Software engineer opens a PR. Then, future tech kicks in. A code review tool so advanced, it is indistinguishable from magic. It thoroughly assesses the code, better than any human could. And it points out three security findings, all signal no noise. It summarizes the issues and lists actionable remediation steps, easy to take. One of the issues is a hardcoded secret. We’ve never had tools that could conduct reviews this good. Engineer ignores it, approves PR, merges it. Hell is other people
10
2,713
So Astra misunderstood a request of mine and pasted all of my human prompts into a GitHub comment and... uhhh.... I kinda like it? LMAO github.com/pytorch/pytorch/p…
5
7
3
190
17,054
i'm such a slob with my agents hahahaha
2
14
1,285
You thought that cybersec was defender advantage in the long term but did you ever stop to consider the possibility that hardware isolation on modern CPUs doesn't actually work
2
46
2,766
difficultyang retweeted
Replying to @difficultyang
The big recent progress is the RLibM project, which yes uses exhaustive checking, plus LP to synthesize polynomials. The CORE-MATH project is doing correctly rounded impls for major scalar functions. Softmax is a bit harder because many inputs, so lotta bits
1
2
154
Low-background YouTube Music is music produced before 2026, the date when AI generated music became good enough to mass proliferate across the catalog.
11
1,092
However, AFAICT, there was no FP theorems added, so there's no proof that the new implementation actually fixes the FP precision problem that was claimed to be fixed.
1
3
30
2,059
It is probably possible to prove something along these lines! But what exactly is the theorem you want to prove? If you tried to prove absolute error ≤ 10⁻⁷, well, that will admit the buggy implementation! There's a reason your theorem statements are considered "trusted".
2
2
31
1,915
Anyway. I'm super excited about all of the formal verification projects popping up, at PyTorch HQ we're trying to figure out what exactly we want to do in this space, but I've also been doing a lot of FM educating recently. Hope this helps the discourse!
2
1
43
1,758
(Aside: There actually is one theorem about tensors containing floating point numbers but it's "did we define CE correctly".)
1
2
21
2,651
The fix commit switches over to the stable formulas. The (rightly!) requires adjusting the existing real number proofs, since you're now proving things about a different mathematical formula, but not the statements themselves which remain true (good!)
1
2
24
2,433
It also proved some theorems about logSoftmax, like that the stated JVP is correct and the conventional numerical stability algebraic rewrite is correct. But importantly, these theorems were all proved on tensors handling REAL numbers.
1
1
1
39
7,219
Real numbers are nice and beautiful and mathematicians love proving theorems with them and it will never tell you anything about the log softmax problem, which is entirely an artifact of floating point representation.
1
3
46
3,022
So the log_softmax bug arxiv.org/abs/2610.31642 that's been making the rounds. TorchLean also had the same problem (fixed in github.com/lean-dojo/TorchLe…). How come? This example is pretty illustrative of the proper mindset you need when working on formal verification. 🧵
13
35
8
340
37,156
LeanTorch implemented ops in Lean. Implementing an algorithm in a theorem proving capable language certainly gives you some guarantees, e.g., it is terminating (if you didn't use "partial"), it is well-typed (this can mean a lot with fancy dependent types). Not bug free!
1
2
1
40
4,097
A naive understanding of formal verification might be something like, "Well, if I do it in Lean, then it can't have bugs." WDYM "do it"? WDYM "can't have bugs"? This is entirely the question.
2
6
54
4,425
Claude you are so cool
1
42
2,497