Papers of the day   All papers

Generative Language Modeling for AutomatedTheorem Proving

Comments

Stanislas Polu: Posted my first paper on arXivπŸ’₯πŸ™Œ GPT-f is a Transformer-based automated theorem prover. We show that Transformer + Search is suitable to formal reasoning and continuous self-improvement 🦾 https://arxiv.org/abs/2009.03393 https://t.co/5ttVX0MNBC

16 replies, 950 likes


Ilya Sutskever: Transformers can prove theorems!

4 replies, 548 likes


Aran Komatsuzaki: Generative Language Modeling for Automated Theorem Proving GPT-f, a Transformer LM pretrained on arXiv and trained through continuous self improvement for theorem proving, finds novel short proofs. https://arxiv.org/abs/2009.03393 https://t.co/iYzqnHAddJ

5 replies, 338 likes


Greg Brockman: New result: GPT for formal theorem proving. We produced shorter proofs of existing theorems (https://github.com/metamath/set.mm/pull/1547), and proofs of assertions people hadn't yet written formal proofs for (https://github.com/metamath/set.mm/pull/1710), which have been merged into the Metamath proof database.

4 replies, 322 likes


AK: Generative Language Modeling for Automated Theorem Proving pdf: https://arxiv.org/pdf/2009.03393.pdf abs: https://arxiv.org/abs/2009.03393 https://t.co/nKKECgFhpT

1 replies, 34 likes


Connor Leahy: Compute is eating AI. @OpenAI trains a state of the art theorem prover using a GPT architecture. I was waiting for this to happen, neat! Though for real...wtf is this proof? Maybe the gains were just that you need an AI to understand this language haha! https://arxiv.org/abs/2009.03393 https://t.co/cNpqNiZmcc

4 replies, 27 likes


Mark O. Riedl: You had me at GPT + search

0 replies, 21 likes


Matt Shumer: The transformer architecture is going to become way more common in the near future. Its flexibility is incredible. Paper on GPT models trained to prove theorems: http://arxiv.org/abs/2009.03393

0 replies, 9 likes


ε°ηŒ«ιŠγ‚Šγ‚‡γ†οΌˆγŸγ‹γ«γ‚ƒγ—γƒ»γ‚Šγ‚‡γ†οΌ‰: β€œWe study the effect of pre-training on the performance of our models. We pre-train our models on both GPT-3’s post-processed version of CommonCrawl as well as a more reasoning-focused mix of Github, arXiv and Math StackExchange.” https://arxiv.org/abs/2009.03393

1 replies, 8 likes


Thomas: Generative Language Modeling for Automated Theorem Proving "... to our knowledge, the first time a deep-learning based system has contributed proofs that were adopted by a formal mathematics community." https://arxiv.org/abs/2009.03393 https://t.co/yi67uEv2gh

0 replies, 8 likes


Carlos E. Perez: The future comes too us too fast "GPT-f automated prover and proof assistant and show that the Transformer is suitable to formal reasoning, achieving a new state of the art result on the Metamath library." https://arxiv.org/abs/2009.03393

1 replies, 7 likes


Daisuke Okanohara: GPT-f uses transformer-based LMs for automated theorem proving; LMs are pre-trained by math-related articles and then trained to generate proof steps conditioned on the proof goal, and its likelihood is used at search. It could find new shorter proofs. https://arxiv.org/abs/2009.03393

0 replies, 7 likes


Gonzalo de Polavieja: Applying transformers to automatic theorem proving, https://arxiv.org/abs/2009.03393

0 replies, 4 likes


Ben Sprecher: "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." And, it scales!

0 replies, 3 likes


akira: https://arxiv.org/abs/2009.03393 They proposed GPT-f, which automatically proves theorems using a transformer. The proofs of theorems are defined as a language model such as [GOAL,(theorem),PROOFSTEP,…]. They have succeeded in shortening the theorem proofs with 23 theorems. https://t.co/eeux7K5xET

0 replies, 3 likes


JosΓ© A. Alonso: Generative language modeling for automated theorem proving. ~ Stanislas Polu, Ilya Sutskever. https://arxiv.org/abs/2009.03393 #ATP #MachineLearning #DeepLearning

0 replies, 2 likes


hardmaru: GPT-f: Generative Language Modeling for Automated Theorem Proving Amazing progress. The SOTA baseline is also from 2020. https://arxiv.org/abs/2009.03393 https://t.co/WiQXHVgvOr

0 replies, 2 likes


Stephen Pimentel: Generative Language Modeling for Automated Theorem Proving https://arxiv.org/abs/2009.03393

0 replies, 1 likes


arXiv CS-CL: Generative Language Modeling for Automated Theorem Proving http://arxiv.org/abs/2009.03393

0 replies, 1 likes


nikete: Generative Language Modeling for Automated Theorem Proving https://arxiv.org/abs/2009.03393 (doubles the starte of the street performance on a benchmark), this is fantastic to see

0 replies, 1 likes


Content

Found on Sep 09 2020 at https://arxiv.org/pdf/2009.03393.pdf

PDF content of a computer science paper: Generative Language Modeling for AutomatedTheorem Proving