Progress on Superhuman Theorem Proving?

Steve Omohundro, Founding Editor

Harmonic (which is working on "Mathematical Superintelligence") just closed their $75 million Series A round led by Sequoia Capital https://harmonic.fun/news The New York Times did a piece ab= out them and about the use of mathematical proof as a "path around hallucinations" as DeepMind's David Silver put it. He says "Proof is a form of truth". "Is Math the Path to Chatbots Th= at Don�t Make Stuff Up? Chatbots like ChatGPT get stuff wrong. But researchers= are building new A.I. systems that can verify their own math � and maybe more."

https://archive.ph/O7qaG

Here�s the full interview with the Harmonic guys: &quo= t;Why Vlad Tenev and Tudor Achim of Harmonic Think AI Is About to Change Math�and= Why It Matters"

https://www.youtube.com/watch?v=3DNvAxuCIBb-c&ab_c= hannel=3DSequoiaCapital

They hope that an AI-human collaboration might solve a Millennium Prize problem by 2028 and the Riemann hypothesis by 2029.

Vlad Tenev says "If you define it as something th= at can reason and solve math problems in excess of any human, something that would give Terry Tao a run for his money, I think we're a couple of years away. B= ut I think the models within the next year will get to the 99.99th percentile.&q= uot; If he is correct, I think this is a complete game changer, upending all of the basic assumptions on both the capabilities = and the safety sides of AI.

I've been discussing with the provably safe crew about whether superhuman theorem proving *next year* will advance provable safety= or cyberattack capabilities more rapidly. Here are some of my thoughts on the tradeoffs:

Typical current methods for attacking systems use tech= niques like "fuzzing": https://en.wikipedia.org/wiki/Fuzzing� to simulate a bunch of random attacks a= nd see if anything succeeds. The distribution of generated attacks can be selected using knowledge of the system and can be adapted as the search proceeds. But with a good theorem prover, the attacker can search over *subsets* of the attack space rather than just particular attacks. When a subset is proven s= afe, it can be removed from the space of candidate attacks. Branch and bound can then home in on the possible candidates and dramatically speed up the search for successful attacks, I think.

On the face of it, the defense task seems much harder:= now we have to search over both the space of possible designs and the space of attacks to find one for which we can prove that no attack can succeed. A priori, that double search seems much more challenging and expensive. But I think there are two things that improve things enormou= sly:

1) We can perform the two searches simultaneously and = use theorem proving to generalize discoveries. A successful attack doesn't just rule out one design, it eliminates a whole set of potential designs. And a proof that there are no attacks also applies to a whole set of designs.

2) We can build designs out of reusable components for= which we have already proven safety properties. If we have also proven the safety impacts of certain forms of composition, then many designs will just involve combining pre-proven components selected from a library and combining them = with pre-proven methods.

And I think we are also likely to create specification= s in that way: from component specs with proven properties and proven compositio= nal methods (eg. often just conjunction: "I wa= nt no memory leaks *and* no buffer overflows").

Similarly, models of attacker capabilities also seem naturally compositional.

I've been delving more into the Lean ecosystem and I'm becoming more and more impressed with it. It really seems pretty natural for the tasks that are needed for forma= lizaton and proofs of safety. And they've even done amazing things with the program= ming language implementation of things like memory management. There are tons of training materials which are generally well-written. But I haven't found practically oriented materials aimed at helping people formalize and prove properties of real systems. This book is somewhat practically oriented but still not quite what is needed, I think: The Hitchhiker's Guide to Logical Verification, 2024 LMU Desktop Edition, March 28, 2024

https://github.com/blanchette/interactive_theorem_prov= ing_2024/blob/main/hitchhikers_guide_2024_lmu_desktop.pdf