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.

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.

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/

> 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.

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.

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.