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 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?
Understanding the process that led to the proof helps to understand how to do further work on top of it, which is the goal of most mathematical research. It's not as though mathematicians are going to go launch a startup operationalizing their knowledge of how densely hyperspheres may be packed.
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 agree with your reading of the presentation and I mostly agree with the presentation - but I believe the recommendations should go a bit further than they do there.
I can't help but wonder about the human motivation there though. For instance as it became increasingly clear that LLMs were capable (and becoming ever more capable) of competently solving meaningfully complex software development tasks, suddenly then there came to be a lot of talk of 'prompt engineering' as a skill. The chronology doesn't make a ton of sense unless you consider that the main motivation may have been simply looking for a way to keep software engineers in the loop.
Pure math is relatively outside my domain, so I find it difficult to grok the exact relevance of the various published discoveries beyond that they are not insignificant, and LLM competence is expanding quite steadily across the field. If this trend continues to the point of LLMs being able to competently expand pure math, it seems somewhat predictable to expect there to be a number of people aiming to find ways to try to keep human mathematicians in the loop.
I've no idea what I think about this one way or the other, beyond that it's certainly a phenomena and one that's going to drive motivated reasoning that may not be entirely sound.
I think those concerned about ensuring a place for human mathematicians usually go in different directions than my suggestion, at least those I've seen so far. Like this post that was recently featured on HN: https://kirwinhampshire.substack.com/p/the-dark-night-of-mat...
My perspective is more like a FOSS philosophy for math. Even if a closed version has the same immediate effect, it's just better for everyone if everyone can look under the hood and tinker with it.
> suddenly then there came to be a lot of talk of 'prompt engineering' as a skill.
I would've thought pretty much the exact opposite. "Prompt engineering" was somewhat important in 2023/2024 when the models were much weaker, it doesn't seem at all necessary anymore (unless just "clearly stating your requirements" counts as prompt engineering). Most of the discussion I've seen seems consistent with this?
The reason it's a meme right now is because there were a lot of people taking it seriously even when it was completely obvious nonsense. And one can argue it always was. There was some good advice that was mostly self evident, like having the most relevant instructions near the end of your context, but there was never a time when a 'prompt engineer' would produce dramatically better output than a random guy just clearly stating what he wants.
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.
So, formal methods produce runnable systems, but communication remains the challenge.
If a formal spec is messy, then it's a proof of ... what, exactly?
A formal specification that bridges tech and product, that lets non-technical contributors read and discuss all the logical nuances, directly as operational code, at product's level of abstraction of interest, would transform a lot.
It's no longer a challenge to create code, it's a challenge to create business requirements and translate them into systems.
The spec and proof are separate. In this blog article he mentions seL4 formal verification, where they state that the spec was 4900 lines of Isabelle and the proof was 200K lines. Obviously human has to understand the spec deeply.
There's an information theoretic aspect about generating a proof which is essentially not human readable from 4900 lines of spec. I wonder how much additional signal they're getting out beyond what's in that 4900 lines, and what's the percentage of noise in the 200k lines of proof?
The problem is that generating either code or proofs with LLMs is very expensive, and generating good proofs (I don't mean elegant, I mean proving the most important properties) is probably not very fast, either. Reducing the verification time of a program from 100 years to 10 years or the cost from $1bn to $100m is still not practical enough to become truly mainstream.
Things can be improved when people help guide and focus the LLMs, but these people still need to be formal methods experts.
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!
The article I am responding to (which I've read) shows that these LLMs come with all sorts of hacks (= context bits) to make it behave more like this or more like that.
There is probably a whole testing workflow at AI companies to tweak each new model until it "looks" acceptable.
But they still don't understand what they are doing. This is purely empirical.
It's interesting to think about what the process will look like when we do understand them. I imagine pulling bits of LLM off the shelf like libraries and compiling them together into a functioning "brain", precisely tailored to your needs.
That all of their model outputs should be influenced by whatever personality prompt voodoo the wise artisan at OpenAI decided to stuff it with during RL should give everyone pause.
That Nerdy personality prompt made me gag. As a card-carrying Nerd, I feel offended
Just to clarify, it's not the prompt voodoo that caused the affinity for goblins. It's the reward. They rewarded it for mentioning goblins when set to Nerdy, and it's still the same model as the other personalities, so the effects can carry over.
Makes sense, but I don't know why they'd let said prompt voodoo touch RL. I'm OK with prompting to get the model to, I don't know, write better Rust or build Excel spreadsheets. I am less OK with making it "quirky" or having some "personality" in a way that becomes ingrained in the model for everyone else
TL;DR the cringe nerdy shit should be (optionally) switched on at inference, not as part of RL
They do it because training different personalities is more effective than just changing the system prompt. Ever try asking ChatGPT to adopt a specific personality in a prompt? Its standard style bleeds through.
As the article says, the personalities weren't supposed to affect other personalities. OpenAI was as surprised by the goblins as you are. Training can be tricky.
I configured it to use the nerdy personality when I used it to help me on a personal project (setting up a home server, nothing too fancy). LLMs are great at parsing documentation and combing through forums to find out the configurations that matched my goals.
The first time it said something along the lines of "let's use these options to avoid future gremlins haunting you", I sort of rolled my eyes but it was okay, I thought its attempt to sound endearing almost cute. A bit of a "hello fellow kids" attempt at sounding nerdy.
It quickly became noise though. It was extremely overused. Sometimes multiple mentions to goblins in the same reply.
I don't really have an opinion about it, but I sort of came to prefer a more neutral tone instead.
The difference is that in a software project you can throw more than one instance of the model at the code. If you tell it to follow your naming conventions and it fails to do so, that can be picked up by an instance of the same LLM that's running checks before you commit anything. Even though it's the same model it'll usually detect stuff like that. You can even have it do multiple passes.
The way most people are coding with AI today is like Baby's First AI™ compared to how we'll all be using LLMs for coding in the future. Soon that "double check everything" step will be built in to the coding agents and you'll have configuration options for how many passes you want it to perform (speed VS accuracy tradeoff).
> 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?
If anything has, minimally, a robust spatiotemporal sense of itself, and can project that sense forward to evaluate future outcomes, then it has a robust "self."
What this requires is a persistent internal model of: (A) what counts as its own body/actuators/sensors (a maintained self–world boundary), (B) what counts as its history in time (a sense of temporal continuity), and (C) what actions it can take (degrees of freedom, i.e. the future branch space), all of which are continuously used to regulate behavior under genuine epistemic uncertainty. When (C) is robust, abstraction and generalization fall out naturally. This is, in essence, sapience.
By "not trivially reducible," I don't mean "not representable in principle." I mean that, at the system's own operative state/action abstraction, its behavior is not equivalent to executing a fixed policy or static lookup table. It must actually perform predictive modeling and counterfactual evaluation; collapsing it to a reflex table would destroy the very capacities above. (It's true that with an astronomically large table you can "look up" anything -- but that move makes the notion of explanation vacuous.)
Many robots and AIs implement pieces of this pipeline (state estimation, planning, world models,) but current deployed systems generally lack a robust, continuously updated self-model with temporally deep, globally integrated counterfactual control in this sense.
If you want to simplify it a bit, you could just say that you need a robust and bounded spatial-temporal sense, coupled to the ability to generalize from that sense.
