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!
> 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.
> To train DeepSeek-R1-Zero, we adopt a rule-based reward system that mainly consists of two
types of rewards:
> Accuracy rewards: The accuracy reward model evaluates whether the response is correct. For example, in the case of math problems with deterministic results, the model is required to provide the final answer in a specified format (e.g., within a box), enabling reliable rule-based verification of correctness. Similarly, for LeetCode problems, a compiler can be used to generate feedback based on predefined test cases.
> Format rewards: In addition to the accuracy reward model, we employ a format reward model that enforces the model to put its thinking process between ‘<think>’ and ‘</think>’ tags.
This is a post-training step to align an existing pretrained LLM. The state space is the set of all possible contexts, and the action space is the set of tokens in the vocabulary. The training data is a set of math/programming questions with unambiguous and easily verifiable right and wrong answers. RL is used to tweak the model's output logits to pick tokens that are likely to lead to a correctly formatted right answer.
(Not an expert, this is my understanding from reading the paper.)
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.