jsenn

I feel like this is conflating 2 separate results in a slightly misleading way.

> We find that frontier LLMs are surprisingly good at natively reading and writing neural network weights

This claim is backed up by the ability of Astra, given a text representation of the weights of tiny (20k) special-purpose models, to figure out what those models do and in some cases improve them beyond what RL could do just by reading the weights with no tool calls. They call this "weight-space programming".

> Likewise, asked to make Qwen3.5-0.8B better at math without gradients, Astra identifies an issue in its weights causing reasoning loops that Qwen’s own model card warns about, and fixes this by natively editing 0.016% of the weights

Here it did use tool calls, and seemingly used standard steering vector techniques to identify and fix reasoning loops in this small Qwen model. This doesn't seem that related to the previous results.

This is really cool work. The particular spec structure/methodology does seem awkward though:

1. Prove the ASan-instrumented binary doesn't crash

2. Prove the non-instrumented binary doesn't crash

3. Prove the instrumented and non-instrumented binaries have the same behaviour (under a particular model of a Linux process's behaviour)

This is a clever hack for automatically generating a formal spec for an existing program, but the fact that you need ASan in there makes it seem like this is less general than it sounds. Could the agents directly prove that out of bounds memory accesses don't occur on the original binary and skip ASan altogether? It's convenient to let the spec just be "it doesn't crash", and ASan provides a crash when the other bad things you care about happen (i.e. out of bounds memory accesses), but I wonder if modelling the memory accesses directly would simplify things.

This is a cool idea. It would be interesting to see how sensitive the results are to the strength of the LLM used for query augmentation. They used GPT-5 in their experiments, and generating all those tokens would presumably add a lot of latency in your query pipeline.

Another baseline that would be interesting to see is just pure LLM reranking--is Jev/the query augmentation adding anything? Presumably the idea is that Jev is cheaper, but even with a costly LLM you might get a lot of cache hits as long as the query (the variable portion) goes last. Even setting caching aside, almost the entire request is prefill plus a very small amount of generation for the judgment itself. You may end up generating fewer tokens just using the LLM as a judge directly than you need to generate the rubric for Jev. OTOH if queries can be normalized or are naturally repetitive you may be able to cache the rubric...

You are picking on 1 bullet point out of 7. I think the following bullet point is the crux of his argument:

> Could the AI solution be somehow misaligned by exploiting a weakness in the trial process or its math models?

Many of our institutions and cultural practices have evolved around human beings, not ruthless paperclip maximizers. Do you think the current drug approval process is bullet proof enough that a completely novel AI-generated drug candidate with zero prior research literature can be considered safe if it makes it through the process?

Tao is a mathematician. He thinks that the institutions and cultural practices in math are not up to the task of dealing with AI-generated mathematics. In software, we are finding that programming interviews, code review, testing, and many other practices are too easy to exploit by AIs, or humans augmented with AIs, and we will have to adapt too. I think it is plausible that other institutions in society will have to change for similar reasons.

This is probably a harness problem rather than a model problem. GitHub Copilot will happily and effectively use Powershell while Claude Code struggles in my experience.

I don’t see Tao suggesting what you have suggested there. Instead he suggests that humans responsibly disclose AI use, and that mathematicians develop a set of norms to deal with an overabundance of AI generated results. For example, he suggests that authors should be able to discuss their results in detail to demonstrate understanding before publication.

I can see this being important if you only care about the results as evaluations of AI progress, but if what you care about is the math itself why should you care about the prompt or anything other than the proof?

This looks cool, but I wonder how well their trained compiler generalizes to new task families. They trained on 29 specific types of tasks, with 800 sub tasks and many rephrasings of each one (the specs). They hold out some specs for validation, but don’t seem to have held out a full task family and maybe not even full sub tasks?

If the compiler can’t generalize well to unseen tasks then it’s effectively acting as a fancy router to one of 29/800 predefined LoRAs.

Their demo is almost unbelievably fast, but as I understand it, the limitation of Taalas's strategy is KV-cache. This grows with context length, so either needs to be stored in SRAM (small) or streamed in (slow). Even for a tiny model like the Llama 8B they have in their demo, the KV cache will be ~64kb per token at 8-bit quantization, so at a 1,000-token sequence length you are already at 64MB of SRAM for a single user. This is probably why their demo only lets you generate 1,000 tokens: they can't go beyond that without slowing down inference.

So I'm curious what their strategy is. It seems to me that the options are: 1. Target smaller usecases that can live with a tiny context window 2. Use huge amounts of SRAM (at which point they look like Groq or Cerebras) 3. Make it up with extreme KV-cache compression/quantization 4. Run linear-attention/sliding window attention models

Other commenters have mentioned robotics as a potential application, which sounds interesting.

> isn't the verification code going to be sloppy as well

The beauty of formal methods is it doesn't matter if your proof is sloppy. As long as it passes verification, it is correct. And unlike in pure math, the proof that a software system is correct is usually a huge mess of special cases, loop invariants, proofs by induction, and boilerplate that requires a large amount of human labour while providing no insight.

Proofs are also brittle: a tiny change in the code can force you to throw your proof away and start from scratch.

To me, the exciting thing about formal methods in the LLM era is it allows humans to offload the difficult and tedious work of writing proofs to a computer. Taken to an extreme, the human could live entirely in the world of a formal specification, and the LLM could generate 100% of the code. The code may be a mess, but if the system proves it satisfies the spec then it can't be wrong.

The article you are responding to showed that a strange LLM behaviour was caused by a training signal that was explicitly designed to produce that type of behaviour. They were able to isolate it, clearly demonstrate what happened, and roll out a mitigation using a mechanism they engineered for exactly this type of thing (the developer prompt). That doesn’t sound like sorcery to me. If anything I’m surprised you can so easily engineer these things!

Is this parlour trick so different from useful tasks like “implement this feature while following the naming conventions of my project”?

> Section 2.6 gives the hidden state size per token, which, on first read, is strictly larger than the hidden state in normal attention

This is where you’ve gone off track. The “hidden state” for their model is a fixed size thing, like in an RNN, not per token. For a transformer, the “hidden state” is called the KV cache, and it grows with sequence length. This is why their method is linear not quadratic.

The Taylor Series they derive isn’t just for softmax (after all, real implementations of softmax will likely already use the Taylor series!), it’s for the entire tensor-level softmax(QK) computation.

You can find papers discussing "cubic" attention, i.e. each token gets to interact with each pair of other tokens, but always in very theoretical settings with single-layer transformers on contrived synthetic tasks.

Keep in mind that LLMs have many many layers, so they have plenty of opportunity to model higher-order interactions without needing to brute force every possible combination of 10 previous tokens, of which the vast majority will be useless. Empirically, even full "quadratic" attention is not always necessary, as evidenced by the existence of linear/sparse attention variants that perform almost as well.

If you remove the terms "self", "agency", and "trivially reducible", it seems to me that a classical robot/game AI planning algorithm, which no one thinks is conscious, matches these criteria.

How do you define these terms without begging the question?

I don’t know the post you’re referring to but I highly recommend How the Immune System Works by Lauren Sompayrac. It explains the interesting parts without getting bogged down in the details of every signalling pathway, but without dumbing things down too much.

A string fixed at both ends produces harmonic sounds because of its particular structure. In order to have a non-integer overtone the ends would have to move up and down, which by construction they can't. Similarly for wind instruments: the air stops at either end and is reflected back, and a non-integer overtone would require changing the length of the tube (or sticking holes in it to allow the pressure to go to zero at the hole, effectively creating an artificial "end" of the tube).

By contrast, a freely vibrating bar (not fixed at the ends) does not have harmonic overtones. To make the bars of a xylophone, marimba, or vibraphone sound nice, you have to cut out a little "scoop" shape from the bottom of the bar to force it to vibrate such that its overtones match up with integer multiples of the fundamental frequency of the bar.

As you say, most sounds in nature do not have a harmonic spectrum, so if a fan did I would find that surprising and interesting.

> It will have overtones that are integer multiples of the fundamental that give it its characteristic sound.

What I’m wondering is why would the overtones go in integer multiples (I.e. be harmonic) for a fan? A flute and a saxophone have harmonic(ish) overtones because of the physics of a vibrating column of air

Is the drone of a fan harmonic? I would’ve thought it’s more like a repetition pitch so its overtones would not be harmonic and would not exhibit a missing fundamental.

Agree with the broader point, just curious if there’s some interesting physics that creates a harmonic sound.

Apple's implementation of this is discussed here: https://news.ycombinator.com/item?id=43685714

yeah, the linked paper [1] has more detail--basically they seem to start with a seed set of "class labels" and subcategories (e.g. "restaurant review" + "steak house"). They ask an LLM to generate lots of random texts incorporating those labels. They make a differentially private histogram of embedding similarities from those texts with the private data, then use that histogram to resample the texts, which become the seeds for the next iteration, sort of like a Particle Filter.

I'm still unclear on how you create that initial set of class labels used to generate the random seed texts, and how sensitive the method is to that initial corpus.

[1] https://arxiv.org/abs/2403.01749

> This approach works by randomly polling participating devices for whether they’ve seen a particular fragment, and devices respond anonymously with a noisy signal. By noisy, we mean that devices may provide the true signal of whether a fragment was seen or a randomly selected signal for an alternative fragment or no matches at all. By calibrating how often devices send randomly selected responses, we ensure that hundreds of people using the same term are needed before the word can be discoverable. As a result, Apple only sees commonly used prompts, cannot see the signal associated with any particular device, and does not recover any unique prompts. Furthermore, the signal Apple receives from the device is not associated with an IP address or any ID that could be linked to an Apple Account. This prevents Apple from being able to associate the signal to any particular device.

The way I read this, there's no discovery mechanism here, so Apple has to guess a priori which prompts will be popular. How do they know what queries to send?

I think the main advantage is that you can compute the extra parameters (the PRNG seeds) from the network weights alone, whereas most other quantization methods require simulating the quantization procedure at training time (Quantization-Aware Training) or setting them from a calibration dataset (Post-Training Quantization)

> What makes this technique particular to LLM weights

This is my understanding as a non-expert.

LLM activations tend to be relatively sparse with large outliers. With linear quantization, this means you either have to clip off the outliers or you have to stretch your range to include the outliers, which wastes precious bits. Neither of these works well, so essentially all LLM quantization research is using various heuristics to get around these outliers. For example, you can do linear quantization but split the activations up into smaller blocks to make it less likely that any given block contains an outlier.

Another trick people have discovered (predates LLMs) is applying a random rotation/projection to the embeddings. This has the effect of making sure no one dimension in the vector dominates the others (which again hurts quantization). This works because in order for a single dimension to dominate, all the others have to "conspire" to be near zero. When you have 10,000+ dimensions, that's very unlikely.

This paper applies the latter trick. Instead of pre-generating the random projection matrices, they generate them on the fly on the accelerator from a seed that is fixed for each block. The seed is chosen from an offline brute-force search that needs only the weights of the network. This separates it from a lot of other quantization methods that either require calibration data or have to be simulated at training time so the network learns the quantization parameters itself.

You might think this is wasteful/might hurt performance, but it turns out that LLM inference is heavily memory-bound as it involves streaming a very large neural network into the accelerator (GPU/TPU/NPU/whatever) to operate on a relatively small amount of data, so there are lots of "free cycles" to generate these random numbers. Of course, if you care about power usage that might not be a great idea...

This doesn’t answer your question, but one thing to keep in mind is that past the very first layer, every “token” position is a weighted average of every previous position, so adjacency isn’t necessarily related to adjacent input tokens.

A borderline tautological answer might be “because the network learns that putting related things next to each other increases the usefulness of the convolutions”