fmap

Even if the test is run by an independent third party, they can always test open weight models against "finetuning attacks" or similar language which every model will fail for structural reasons.

Their financial future is on the line. The Chinese frontier labs have caught up before the IPO that would have allowed them to cash out.

All three demands in the paper make perfect sense from this perspective. Without chip export restrictions, the rest of the world will leapfrog them in a few months. This will happen regardless, since they have more competition than in-house talent, but a ban would buy more time. Testing and banning capable open-weight models would hinder public research into the technology, another speed bump to slow down the competition. Same thing for "distillation", we can't have large scale public evaluations of their products...

It's in Anthropic's best interest to focus the conversation on "distillation".

Imo the more interesting thing to focus on is that there are now several more labs with the expertise and capabilities to train trillion parameter models. That's a serious technical accomplishment and the main reason why open models are catching up to Anthropic and OpenAI (and local models are typically distillations of much larger models).

Who cares that they got some small amount of training data out of Claude. The crux is that the big US labs are not special, they just have a first mover advantage that's slowly shrinking as incremental progress becomes harder.

> The actual opposing argument is that it's impossible to create a billion dollar enterprise without a group effort

The other thing that we're often ignoring is that it's impossible to create a billion dollar enterprise without luck. You have to be at the right place at the right time.

For the most part only capital gets to roll the dice, but even before that it's a sign of the times that we take it seriously at all when people talk about "earning" a billion dollars. We could all do with a bit more humility.

I agree with most of what the author is saying, but the slogan that "a sufficiently detailed spec is code" can be misunderstood as "a sufficiently detailed spec is a program". The statement is only true if you read "code" as "statement in a formal language". Here's a (sketch of a) specification for a compiler:

> For every specification satisfied by the input program, the output program satisfies the same specification.

This is not a program and it does not become a program once you fill in the holes. Making the statement precise clearly requires a formal language, but that language can work at a higher level of abstraction than a programming language. So yes, a specification can absolutely be simpler than a program that implements it.

Apologies if this came across the wrong way. I really do want to know what the novel contributions of the post are, because the author implies that something about what they're doing is solving previously open problems:

> I figured out how to solve manifold Muon in the square case late last year, but I was unable to solve the full rectangular case and thus posed the problem as an open problem on the Modula docs. Jianlin Su solved the problem this summer

It sounds like the generalisation of projected gradient decent to "Muon" is what they're focusing on, but the derivation is all about the retraction map on the Stiefel manifold? I think I'm missing some background here.

The reason deep learning is alchemy is that none of these deep theories have predictive ability.

Essentially all practical models are discovered by trial and error and then "explained" after the fact. In many papers you read a few paragraphs of derivation followed by a simpler formulation that "works better in practice". E.g., diffusion models: here's how to invert the forward diffusion process, but actually we don't use this, because gradient descent on the inverse log likelihood works better. For bonus points the paper might come up with an impressive name for the simple thing.

In most other fields you would not get away with this. Your reviewers would point this out and you'd have to reformulate the paper as an experience report, perhaps with a section about "preliminary progress towards theoretical understanding". If your theory doesn't match what you do in practice - and indeed many random approaches will kind of work (!) - then it's not a good theory.

The usual way to check whether a definition is correct is to prove properties about it that you think should hold. TLA+ has good support for this, both with model checking as well as simple proofs.

I'm personally very excited about the progress in interactive theorem proving. Before the current crop of deep learning heuristics there was no generally useful higher-order automated theorem proving system. Automated theorem proving could prove individual statements based on existing lemmas, but that only works in extremely restricted settings (propositional or first-order logic). The problem is that in order to apply a statement of the form "for all functions with this list of properties, ..." you need to come up with a function that's related to what you're trying to prove. This is equivalent to coming up with new lemmas and definitions, which is the actually challenging part of doing mathematics or verification.

There has finally been progress here, which is why you see high-profile publications from, e.g., Deepmind about solving IMO problems in Lean. This is exciting, because if you're working in a system like Coq or Lean your progress is monotone. Everything you prove actually follows from the definitions you put in. This is in stark contrast to, e.g., using LLMs for programming, where you end up with a tower of bugs and half-working code if you don't constantly supervise the output.

---

But well, the degree of excitement is my own bias. From other people I spoke to recently: - Risk-assessment diagnostics in medicine. There are a bunch of tests that are expensive and complex to run and need a specialist to evaluate. Deep learning is increasingly used to make it possible to do risk assessments with cheaper automated tests for a large population and have specialists focus on actual high-risk cases. Progress is slow for various reasons, but it has a lot of potential. - Weather forecasting uses a sparse set of inputs: atmospheric data from planes, weather baloons, measurements at ground stations, etc. This data is then aggregated with relatively stupid models to get the initial conditions to run a weather simulation. Deep learning is improving this part, but while there has been some encouraging initial progress this needs to be better integrated with existing simulations (purely deep learning based approaches are apparently a lot worse at predicting extreme weather events). Those simulations are expensive, they're running on some of the largest supercomputers in the world, which is why progress is slow.

> even if this doesn’t lead to AGI, at the very least it’s likely the final “warning shot” we’ll get before it’s suddenly and irreversibly here.

I agree that it's good science fiction, but this is still taking it too seriously. All of these "projections" are generalizing from fictional evidence - to borrow a term that's popular in communities that push these ideas.

Long before we had deep learning there were people like Nick Bostrom who were pushing this intelligence explosion narrative. The arguments back then went something like this: "Machines will be able to simulate brains at higher and higher fidelity. Someday we will have a machine simulate a cat, then the village idiot, but then the difference between the village idiot and Einstein is much less than the difference between a cat and the village idiot. Therefore accelerating growth[...]" The fictional part here is the whole brain simulation part, or, for that matter, any sort of biological analogue. This isn't how LLMs work.

We never got a machine as smart as a cat. We got multi-paragraph autocomplete as "smart" as the average person on the internet. Now, after some more years of work, we have multi-paragraph autocomplete that's as "smart" as a smart person on the internet. This is an imperfect analogy, but the point is that there is no indication that this process is self-improving. In fact, it's the opposite. All the scaling laws we have show that progress slows down as you add more resources. There is no evidence or argument for exponential growth. Whenever a new technology is first put into production (and receives massive investments) there is an initial period of rapid gains. That's not surprising. There are always low-hanging fruit.

We got some new, genuinely useful tools over the last few years, but this narrative that AGI is just around the corner needs to die. It is science fiction and leads people to make bad decisions based on fictional evidence. I'm personally frustrated whenever this comes up, because there are exciting applications which will end up underfunded after the current AI bubble bursts...

Adding to this, inference is getting cheaper and more efficient all the time. The investment bubble is probably the biggest reason why inference hardware is so expensive at the moment and why startups in this sector are only targeting large scale applications.

Once this bubble bursts, local inference will become even more affordable than it already is. There is no way that there will be a moat around running models as a service.

---

Similarly, there probably won't be a "data moat". The whole point of large foundation models is that they are great priors. You need relatively few examples to fine tune an LLM or diffusion model to get it to do what you want. So long as someone releases up to date foundation models there is no moat here either.

Agreed, this is a big step forward. Geometry problems are in a different class, since you can translate them into systems of polynomial equations and use well known computer algebra algorithms to solve them.

By contrast, this kind of open ended formalization is something where progress used to be extremely slow and incremental. I worked in an adjacent field 5 years ago and I cannot stress enough that these results are simply out of reach for traditional automated reasoning techniques.

Real automatic theorem proving is also useful for a lot more than pure mathematics. For example, it's simple to write out an axiomatic semantics for a small programming language in lean and pose a question of the form "show that there exists a program which satisfies this specification".

If this approach scales it'll be far more important than any other ML application that has come out in the last few years.

You don't get new theorems if you remove assumptions. Rather, you get the ability to add different assumptions.

The Banach-Tarski paradox shows that classical set theory makes the wrong assumptions to intrinsically model measure theory and probability.

There are other systems which don't suffer from this paradox and hence don't need all the machinery of sigma algebras and measurable sets.

I wish there was a good accessible book/article/blog post about this, but as is you'd have to Google point-free topology or topos of probability (there are several).