HackerPapers

arXiv:2009.03393cs.LG

Generative Language Modeling for Automated Theorem Proving

Stanislas Polu, Ilya Sutskever

Abstract

We explore the application of transformer-based language models to automated theorem proving. This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans -- the generation of original mathematical terms -- might be addressable via generation from language models. We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance. GPT-f found new short proofs that were accepted into the main Metamath library, which is to our knowledge, the first time a deep-learning based system has contributed proofs that were adopted by a formal mathematics community.

arXiv comments
15+5 pages
Journal reference
DOI
Subjects
cs.LGMachine Learning cs.AIArtificial Intelligence cs.CLComputation and Language stat.MLMachine Learning (Statistics)

On Hacker News

Linked by 6 identifiable commenters in 9 comments across 9 threads, from Sep 2020 to Jul 2024. Found in 2 HN submissions from Sep 2020 to Sep 2020. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments9 threads

  1. AI solves International Math Olympiad problems at silver medal level 1 comment
  2. Lean4 helped Terence Tao discover a small bug in his recent paper 1 comment

    • Sounds like you've stumbled into the wonderful world of machine-learning guided proof synthesis! While I don't think the full system you're describing has been built yet, many similar systems and pieces have. In terms of the initial phase of supervised learning on existing…

      aSanchezSternView on HNParent context

  3. The NetHack Challenge: Dungeons, Dragons, and Tourists (2021) 1 comment

    • Because Nethack and video games remove most of the reasons that GOFAI failed; for example, everything hard about perception from pixels is removed when you have a little parsed text grid of cells presented to you or are hooked into the game engine and query objects directly.…

      gwernView on HNParent context

  4. Mathematicians welcome computer-assisted proof in ‘grand unification’ theory 1 comment

    • It's worth noting that GPT-f already gets a big performance boost from pretraining on Arxiv etc (https://arxiv.org/pdf/2009.03393.pdf#page=7) despite those sources containing next to no Metamath or anything that looks like a raw Metamath proof, just regular natural language &…

      gwernView on HNParent context

  5. DALL·E: Creating Images from Text 1 comment

    • > The accuracy largely comes from the fact that addition rarely requires carrying more than a single digit. So it's easy to pattern match from single digit problems that it was previously trained on. Again, not at all true due to BPEs. [12] [65] [25] [42] [185] + [580] [22] [75]…

      VeedracView on HNParent context

  6. AI Expert Roadmap 1 comment

    • > Aren't you shifting the goalposts a bit? No, I don't think so. My original comment was “I have looked at the program synthesis literature before and it really does not seem very advanced to me. The General Program Synthesis Benchmark Suite lists unsolved benchmarks like “Given…

      VeedracView on HNParent context

  7. The Collatz Conjecture: the simple math problem we still can’t solve 1 comment
  8. At the International Mathematical Olympiad, computers prepare to go for the gold 1 comment

    • OA has done that, as 'GPT-f': https://arxiv.org/abs/2009.03393#openai They also have ambitions of IMO: https://twitter.com/spolu/status/1303693595833237504 I assume it's not mentioned in OP because GPT-f came out too recently for them to interview or profile compared to this…

      gwernView on HNParent context

  9. Graph Representations for Higher-Order Logic and Theorem Proving (2019) 1 comment

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.