21
$\begingroup$

Attempts to apply machine-learning (as opposed to hand-crafted automation) to formal theorem proving are still in their infancy.

Still, there have been some successes. GPT-f found some proofs that were shorter than existing proofs in the Metamath library, and were accordingly accepted there.

Are there other applications of machine-learning to constructing proofs in any proof assistant that attained a success of at least this magnitude - i.e. finding somewhat better versions of existing proofs, if not entirely new proofs?

"Better" can be measured by whatever standards that proof assistant's community usually uses to evaluate proofs, i.e. a shorter proof might not count if it is less readable or less maintainable.

$\endgroup$
6
  • 1
    $\begingroup$ This is not really to the same level of success that you ask for here, but in case you haven't heard of it, [openai.com/blog/formal-math/](AlphaCode) has been applied with success on some Mathematical Olympiad problems to generate formal proof of them Might be interesting to keep an eye on it, they might use it to extend the field very soon $\endgroup$ Feb 10 at 21:38
  • $\begingroup$ @ÉpiphanieGédéon Well, it also produced new proofs of some statements in mathlib. That would be a valid answer to my question if the new proofs were better than the old! $\endgroup$
    – Will Sawin
    Feb 10 at 21:53
  • $\begingroup$ @ÉpiphanieGédéon You got the link backwards. The link description should be at the front. $\endgroup$
    – Trebor
    Feb 11 at 6:29
  • $\begingroup$ The Lean version of GPT-f in the PACT paper (which is the predecessor to the recent OpenAI Olympiad work) also shortened some proofs. Examples are in the appendix under "Example proofs". $\endgroup$
    – Jason Rute
    Feb 11 at 14:17
  • $\begingroup$ @JasonRute Nice! The key quote from the paper from my perspective is "Our work has been welcomed by members of this community, with Lean power users describing some of the new proofs found by GPT-f as “nontrivial” and “clever”. More than one-third of the proofs found by our models are shorter and produce smaller proof terms (sometimes by several orders of magnitude) than the ground truth. Manually inspecting a portion of these shorter proofs has led to 36 GPT-f co-authored commits to mathlib, some of which reduce proof term sizes and theorem compilation times by an order of magnitude." $\endgroup$
    – Will Sawin
    Feb 11 at 14:26

2 Answers 2

13
$\begingroup$

Only a bit more than two months ago, a new formula for Kazhdan-Lusztig polynomials was found by Google's deep learning subsidiary: DeepMind (the same machine-learning company that wrote AlphaGo to beat humans at the board game Go). This formula is presented as Theorem 3.7 in the above-linked paper, and the authors conjectured in the same paper that the formula gives the right answer for any hypercube decomposition (which they indeed checked computationally for all of the Bruhat intervals up to $S_9$, which turned out to be more than a million of them). This conjecture which they computationally found to be very likely true, implies the combinatorial invariance conjecture for symmetric groups, which has been unproven since it was first formulated the 1980s.

The proof of Theorem 3.7 is given in Sections 4-5 of the above-linked-paper, but and is very much a "pen-and-paper" proof, but the theorem itself was discovered amidst the training of machine learning models to predict Kazhdan-Lusztig polynomials from Bruhat graphs, in Nature (2021) "Advancing mathematics by guiding human intuition with AI" which was only published about 2 months ago (Fig 3 shows which hypercube edges are the most important ones as determined from a saliency analysis, and these turned out to be precisely the edges related to the new theorem). Carlo Beenakker called this "the first significant advance in pure mathematics generated by artificial intelligence" in the highest-voted answer to "Breakthroughs in Mathematics in 2021" on MathOverflow (an answer on which you were the first to write a comment!).

Overall, the combinatorial invariance conjecture for symmetric groups remains unproven, but machine-learning helped to discover a "Lemma" which is very likely to be a part of the proof. I would call this a major "success of machine learning in theorem proving", but about this part of your question:

"Are there other applications of machine-learning to constructing proofs in any proof assistant that attained a success of at least this magnitude - i.e. finding somewhat better versions of existing proofs, if not entirely new proofs?"

I hope I'm wrong, but even for proofs done by theorem provers without machine learning, the ones I know were not for entirely new proofs but for finding somewhat better versions of existing proofs. In the case I described above, a new proof would rely on a Lemma which the saliency analysis (a machine learning technique borrowed from the computer vision community) was able to help find.

$\endgroup$
2
  • 3
    $\begingroup$ This is a great example of a success in machine learning, but it wouldn't count for my question unless someone formalized the proof! I guess if you formalize the proof I will accept your answer, but I very much doubt that is sufficient reward to motivate anyone to undertake the effort of formalization. $\endgroup$
    – Will Sawin
    Feb 11 at 12:48
  • 1
    $\begingroup$ I was worried about that after re-reading the question a few times, but by then I had already put in too much effort, and didn't think everything I wrote should go to waste! $\endgroup$ Feb 11 at 16:42
7
$\begingroup$

The group at OpenAI has recently published a new paper, among other problems they have been able to prove two questions from the International Mathematical Olympiad. Isabelle's Sledgehammer has been able to find solutions to some of these examples as well, and they of course have been proved by many people already.

I guess it's open for debate whether the proofs found by GPT-f are better than the ones found by ATP or constructed by humans, but at least Kevin Buzzard finds some of the proofs quite surprising.

$\endgroup$
1
  • 1
    $\begingroup$ This is sort of what motivated the question - it would be great to have an explanation of what makes the proofs surprising / interesting. $\endgroup$
    – Will Sawin
    Feb 11 at 12:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.