From the appendix [0]: "The proofs written by agents are just as 'good' as any other proof of the same theorem, in that they prove the equivalence theorem. However, it remains to be seen whether agents can scale this verbose proof style directly to more complex programs. Experience from other agent-based verification projects, such as MachCSL, suggests that the answer might be no: the agents hit a complexity wall with the verbose proof style, and scaling up requires the proofs to be structured around better modular abstractions and reasoning principles. If that is the case, how can we help agents discover and introduce the right abstractions to reduce this complexity? Does this require input from expert proof engineers, or can we extract common principles that can guide agents to discovering good abstractions that will enable scalable proofs?"
Some mathematicians have observed a similar pattern in the recent LLM proof drops, leading them to suggest that LLMs will hit a wall in mathematical capability just beyond the convex hull of human mathematics. The sort of proofs done in formal verification are a pretty interesting litmus test for LLM reasoning since the systems considered aren't necessarily on distribution (compare with math where the "systems" and structures worked with, and proofs about them, make appearances in thousands of individual books) so the advantages in broad domain knowledge pretrained LLMs have over humans doesn't really buy you much. IMO this observation from Anthropic/Theorem lends more credibility to the convex hull hypothesis.
[0] https://www-cdn.anthropic.com/files/4zrzovbb/website/6867ead...
"leading them to suggest that LLMs will hit a wall in mathematical capability just beyond the convex hull of human mathematics."
This was to be expected, llms are trained on a very large corpus of data, they 'look' like creative from our point of view, as humans don't have that much knowledge, so, if the LLM proposes something that a human does not know, it looks like creative. But they stay neural networks after all, so very good in interpolation, very bad at extrapolation. Building new knowledge is extrapolation if it's truly outside the convex hull how the dataset.
I usually write code and ideas that are at the border of the convex hull, I haven't seen yet an llm being able to propose a really innovative solution. All the time they reuse building blocks that are already there. And I really tried pushing by making them creating proofs.
If I have an insight on some problem and I ask for the proof for it, it will usually be able to generate the proof, but that proof is never creative, and often it will use novel ideas only if I explain the novel idea. It will not come up with it alone. (And sometimes it's very hard to even explain the ideas, as it tends to return to knew waters)
Its only a data point, but I haven't seen a paper that handle this issue yet, and I don't expect them to magically become good at extrapolation due to the theory behind neural networks.
Coz these machines process representation of knowledge, they don't process knowlegde. That part hasn't been figured out by human yet.
EDIT: typo
I highly doubt this will happen.
You’re assuming that we’re doing more than combining ideas we already know when we’re being “creative”
Sorry if this sounds rough, computer science is probably only about combination, but there are many other fields
Sorry if this sounds rough, no.
Saying that is like saying everything is about combination because well, it is even the creative stuff if you are pedantic.
The wibbily wobbly dna of humans is how we keep recombining things into new shit. Comp sci absolutely has deep creativity in it.
DNA is so many layers below human cognition, it's a bit like explaining the Moon landing's technology by a stick burning.
There is absolutely no DNA recombination during a thought process.
At least in arts, there is a true "creative" element complicated to replicate at least in the current LLMs. True artistic invention involves a "spirit of rule-breaking" that pushes culture forward. If AI is only being trained on past data, it then struggles to make the non-linear, revolutionary creative jumps we've seen throughout history.
For instance, the transition of music from the 1950s to the Beatles, then to Nirvana, hip-hop, and beyond. Before Beatles, there wasn't such thing as Beatles. Before Nirvana, there wasn't anything that sounded like that. Of course you can point out underground bands doing something like that around that era, but stray way back in time to like 1940s and chances of hearing something like Nirvana are near zero.
True art is not easy to make. It is, rather, difficult. If you lower the difficulty to make art, then it is not already a piece of art. It is just another product down the line of plenty of copy cats. Art involves risk taking that AIs I don't think are capable of producing. Art is a medium to express human emotions, and the inherent concept here is that it will end up being consumed by another human being, and it has value because you know that another human being was on the other side of the table making it. Even if you do something you consider art for yourself with an AI, the human being on the other side was, well... you. You prompted it and you guided it. I don't believe people in general would be contempt with an endless stream of autonomous AI generated stuff (if they invent such loop) because it would not only be generic, repetitive and predictable at some point, but also the fact that you know its AI it destroys the whole vibe. Same as if you get an email and you don't know if it was an AI or human behind it. If it was a human being, great, you feel a connection there. If it was AI, well... that sucks to no end, and I guess that is for a very good reason.
Although I'm using art here as the argument for creativity, I believe there may be something analogous to scientific leaps and discoveries. To my understanding, people who seem to be fairly successful in uncover the truths of the universe via science also happen to be pretty good when it comes to some artistic endeavors, even if its only about consuming and appreciating art and not necessarily creating it. So, there might be some link in creativity there. I'm open to be wrong, of course. Creativity is about risk taking and pushing the edges, not re-iterating upon what's been already there.
Writing proofs is just writing code in a niche language (that's what the Curry-Howard isomorphism is all about). Writing modular proofs with better abstractions is just writing modular code with better abstractions.
Yeah agents need to step up their programming game in general. They write too verbose code and are happy with duplicating code. This works up until the code is so big that they can't process the code base effectively.
If I had to guess, if you train agents to write better proofs (better modularized, etc), they will get better at programming in general. Or at very least, better at writing Haskell, since so many theorem provers are just sufficiently powerful functional programming languages. And if you get better at writing Haskell, you probably get a little better at writing Rust too. That's why I think this skill probably generalizes a lot.
So maybe training agents to do math will get them, like, use Creusot [0] or flux [1] or Aenas [2] to write proofs on their Rust code, and even when they don't, they will probably write code in ways that are more amenable for reasoning
[0] https://creusot.rs/
[1] https://flux-rs.github.io/
[2] https://lean-lang.org/use-cases/aeneas/
Curry-Howard doesn't buy you any shortcuts to capability. Surely no expense has been spared in training models to write good (well modularized, robust, generic etc.) code, and yet they still write slop (poorly structured, overfit to specification gaps, etc.) We see the same sloppish habits in their mathematics, perhaps transported along the CH iso. So "train[ing] agents to write better proofs" seems to me like a grand challenge problem for AI research, just like getting them to write good code. It won't be solved just by noticing that the two problems are isomorphic: we'll keep getting models that are a little better at grinding out proofs, hence a little better at grinding out programs, but the abstraction wall won't magically drop in either world just because the same limited behaviors can be transported along CH.
The key is to make general intelligence, and train models in regimes that generalize well among many domains, rather than just a bunch of math proof tricks that don't generalize.
I think LLMs have demonstrated tons of generalization already, but I concede that being good at theorem provers don't automatically translate into being good at other forms of programming and vice versa. But the labs should probably focus on generalizing rather than optimizing for each subfield of programming individually.
Also as an aside, I meant that the use of theorem provers for proving theorems is just programming, that is, Lean, Rocq etc. are programming languages. They are functional programming languages and they invoke Curry-Howard as a reason for them to work, like, at all. And that's why their reasoning is essentially intuitionistic
You make a compelling argument, but, empirically, when you optimize code for performance, you end up with an unreadable mess that breaks all abstractions; but every time I've substantially optimized a proof for performance [of proof checking], I've ended up with better abstractions and more modularity.
That's super interesting. I wonder if you've tried optimizing for type-checking duration of a richly dependently typed program and gotten viscerally nicer code out of that.
A little before that was:
> The most striking feature of agent proofs is that they are verbose, repeatedly spelling out details about the program’s execution: specifying the contents of CPU registers, explicitly writing out integer conversions, explicitly spelling out that many different addresses are all distinct from one another, writing out the exact contents of stack addresses, explicitly considering every possible branch in a function, etc.
> To be sure, these details are important to precisely reason about the execution of code. However, human proof engineers would have immediately introduced abstractions to factor out these types of repetitive specifications.
- - -
This matches my experience when I look at the tests LLMs write to check their own work when I’ve given them a task. The tests are almost universally terrible because they hard code everything in the most brittle way possible. They are nearly useless for regression tests because if I change anything about the source, even in non material ways, the tests all break in stupid ways that aren’t checking any important properties.
If I have the LLM make the then it also has to rewrite all the tests in a new episode of brittle concrete hyper-literal tests. The concept of a regression suite is non-existent.
It’s probably just as well. Having the implementer write the verification is generally a bad idea with people, maybe the problem of carrying over assumptions and blind spots and misconceptions applies to LLMs as well.
One might say it’s operator error, and I’m underspecifying things, but if I have to go to such elaborate lengths to get it to do what I need, I’ll just implement it myself.
It’s probably just as well. Having the implementer write the verification is generally a bad idea with people
Nobody (sane) does that.
Lots of people have the implementer write the tests. But this only seems like a bad thing because of an unfortunate terminology collision:
- Microsoft culture: tests are adversarial verification.
- Google culture: tests are executable documentation.
Both of these things are important. It's really unfortunate we call both of them "tests".
At Microsoft, (verification) tests are written by a different engineer than the one who wrote the code under test. VLSI/Hardware works like this too.
At Google, (documentation) tests are written by the person who wrote the code, because it's their job to document it, and because the point of documentation-tests is to make sure other people who modify your code don't break it.
> LLMs will hit a wall in mathematical capability just beyond the convex hull of human mathematics.
I love that “convex hull” analogy. LLMs can certainly serve as a channel for knowledge transfer. They can help spread knowledge and know-how throughout society, enabling breakthroughs that were simply held back by practical limitations (e.g. lack of money, time, or expertise). Personally, I think LLM is more valuable as a tool for democratizing knowledge than as artificial intelligence.
> leading them to suggest that LLMs will hit a wall in mathematical capability just beyond the convex hull of human mathematics
I mean, even just that would prove to be a very productive workhorse - potentially being able to automate away almost every white collar job.
I agree with the observation but not the extrapolation. After all, RLing on sufficiently hard problems might cause agents to adopt better proof strategies emergently.
Sounds like a software problem.
Experience from other agent-based verification projects, such as MachCSL, suggests that the answer might be no: the agents hit a complexity wall with the verbose proof style, and scaling up requires the proofs to be structured around better modular abstractions and reasoning principles.
This is not just plausible but in fact the most likely result.
We already have plenty of evidence of this phenomenon in programming. LLMs are awesome for working on human-written or at least human-reviewed codebases.
But when you set them loose without a human around to force them to refactor their code into something that fits in meatbag-brain-sized contexts, they drift into the ghastly nightmare of the Anthropocene (go ahead, take a look at the leaked source code for Claude Code). They can handle this for a while, especially if you're doubling your model's weight count every four months.
But when you stop doing that, they choke on their own spaghetti.
It's like Feynman said about teaching -- great theoretical physicists need to re-explain the basics to students from time to time in order to force them to come up with not just the correct physical laws, but the simplest version of those laws. Take away that constraint -- IAS or LLM -- and eventually it all goes wrong.
The difference between math and software verification: in math, the convex hull hypothesis implies that you don't go far beyond human capability, because the bottleneck is out of distribution generalization. In software verification, you can verify just about all the software that exists despite the convex hull hypothesis, because the bottleneck is just scale.