Fetching the paper…
Reading the bibliography…
This paper presents a novel approach to premise selection, a crucial reasoning task in automated theorem proving.
Rodrigo Frassetto Nogueira and Kyunghyun Cho · 1901
Earlier work this paper cites.
The mathematical language AUTOMATH, its usage, and some of its extensions
Nicolaas Govert De Bruijn · 1970
Earlier work this paper cites.
Mizar in a nutshell
Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz · 1980
Earlier work this paper cites.
Isabelle: The next 700 theorem provers
Lawrence C. Paulson · 1993
Earlier work this paper cites.
HOL light: A tutorial introduction
John Harrison · 1996
Earlier work this paper cites.
Scaling laws for neural language models
Jared Kaplan, Sam McCandlish, Tom Henighan, Tom B. Brown, Benjamin Chess, Rewon Child, Scott Gray, Alec Radford, Jeffrey Wu, and Dario Amodei · 2001
Earlier work this paper cites.
Combining superposition, sorts and splitting
Christoph Weidenbach · 2001
Earlier work this paper cites.
System description: E 0.81
Stephan Schulz · 2004
Earlier work this paper cites.
Language models are few-shot learners
Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter, Christopher Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, Ilya Sutskever, and Dario Amodei · 2005
Earlier work this paper cites.
Lightweight relevance filtering for machine-generated resolution problems
Jia Meng and Lawrence C. Paulson · 2007
Earlier work this paper cites.
A short presentation of coq
Yves Bertot · 2008
Earlier work this paper cites.
Z3: An efficient SMT solver
Leonardo de Moura and Nikolaj Bjørner · 2008
Earlier work this paper cites.
Fun with functions
Tobias Nipkow · 2008
Earlier work this paper cites.
MaLARea SG1 – machine learner for automated reasoning with semantic guidance
Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jiří Vyskočil · 2008
Earlier work this paper cites.
Generative language modeling for automated theorem proving
Stanislas Polu and Ilya Sutskever · 2009
Earlier work this paper cites.
The probabilistic relevance framework: BM25 and beyond
Stephen E. Robertson and Hugo Zaragoza · 2009
Earlier work this paper cites.
Sledgehammer: Judgement day
Sascha Böhme and Tobias Nipkow · 2010
Earlier work this paper cites.
Solving mathematical problems: A personal perspective
Terence Tao · 2010
Earlier work this paper cites.
Premise selection for mathematics by corpus analysis and kernel methods
Jesse Alama, Daniel Kühlwein, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes · 2011
Earlier work this paper cites.
ImageNet classification with deep convolutional neural networks
Alex Krizhevsky, Ilya Sutskever, and Geoffrey E. Hinton · 2012
Earlier work this paper cites.
Overview and evaluation of premise selection techniques for large theory mathematics
Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes · 2012
Earlier work this paper cites.
Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers
Lawrence Charles Paulson and Jasmin Christian Blanchette · 2012
Earlier work this paper cites.
Extending Sledgehammer with SMT solvers
Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson · 2013
Earlier work this paper cites.
First-order theorem proving and vampire
Laura Kovács and Andrei Voronkov · 2013
Earlier work this paper cites.
MaSh: Machine learning for Sledgehammer
Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban · 2013
Earlier work this paper cites.
Premise selection for mathematics by corpus analysis and kernel methods
Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban · 2014
Cited alongside, same era.
The Lean theorem prover (system description)
Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer · 2015
Cited alongside, same era.
Premise selection and external provers for HOL4
Thibault Gauthier and Cezary Kaliszyk · 2015
Cited alongside, same era.
DeepMath – deep sequence models for premise selection
Alexander A. Alemi, François Chollet, Geoffrey Irving, Christian Szegedy, and Josef Urban · 2016
Cited alongside, same era.
A learning-based fact selector for Isabelle/HOL
Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban · 2016
Cited alongside, same era.
HolStep: A machine learning dataset for higher-order logic theorem proving
Contrastive finetuning of generative language models for informal premise selection
Jesse Michael Han, Tao Xu, Stanislas Polu, Arvind Neelakantan, and Alec Radford · 2021
Later among the works it cites.
Towards unsupervised dense information retrieval with contrastive learning
Gautier Izacard, Mathilde Caron, Lucas Hosseini, Sebastian Riedel, Piotr Bojanowski, Armand Joulin, and Edouard Grave · 2021
Later among the works it cites.
LISA: Language models of ISAbelle proofs
Albert Q. Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu · 2021
Later among the works it cites.
IsarStep: A benchmark for high-level mathematical reasoning
Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson · 2021
Later among the works it cites.
Learning transferable visual models from natural language supervision
Alec Radford, Jong Wook Kim, Chris Hallacy, Aditya Ramesh, Gabriel Goh, Sandhini Agarwal, Girish Sastry, Amanda Askell, Pamela Mishkin, Jack Clark, Gretchen Krueger, and Ilya Sutskever · 2021
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Cezary Kaliszyk, François Chollet, and Christian Szegedy · 2017
Cited alongside, same era.
The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0
G. Sutcliffe · 2017
Cited alongside, same era.
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin · 2017
Cited alongside, same era.
Premise selection for theorem proving by deep graph embedding
Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng · 2017
Cited alongside, same era.
Hammer for Coq: Automation for dependent type theory
Lukasz Czajka and Cezary Kaliszyk · 2018
Cited alongside, same era.
Universal language model fine-tuning for text classification
Jeremy Howard and Sebastian Ruder · 2018
Cited alongside, same era.
PaMpeR: Proof Method Recommendation system for Isabelle/HOL, 2018
Yutaka Nagashima and Yilun He · 2018
Cited alongside, same era.
Later among the works it cites.
Contrastive learning with hard negative samples
Joshua David Robinson, Ching-Yao Chuang, Suvrit Sra, and Stefanie Jegelka · 2021
Later among the works it cites.
Roformer: Enhanced transformer with rotary position embedding
Jianlin Su, Yu Lu, Shengfeng Pan, Bo Wen, and Yunfeng Liu · 2021
Later among the works it cites.
BEIR: A heterogenous benchmark for zero-shot evaluation of information retrieval models
Nandan Thakur, Nils Reimers, Andreas Rücklé, Abhishek Srivastava, and Iryna Gurevych · 2021
Later among the works it cites.
GPT-J-6B: A 6 Billion Parameter Autoregressive Language Model
Ben Wang and Aran Komatsuzaki · 2021
Later among the works it cites.
ProofNet: A benchmark for autoformalizing and formally proving undergraduate-level mathematics problems
Zhangir Azerbayev, Bartosz Piotrowski, and Jeremy Avigad · 2022
Later among the works it cites.
cvc5: A versatile and industrial-strength SMT solver
Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar · 2022
Later among the works it cites.
Improving language models by retrieving from trillions of tokens
Sebastian Borgeaud, Arthur Mensch, Jordan Hoffmann, Trevor Cai, Eliza Rutherford, Katie Millican, George van den Driessche, Jean-Baptiste Lespiau, Bogdan Damoc, Aidan Clark, Diego de Las Casas, Aurelia Guy, Jacob Menick, Roman Ring, Tom Hennigan, Saffron Huang, Loren Maggiore, Chris Jones, Albin Cassirer, Andy Brock, Michela Paganini, Geoffrey Irving, Oriol Vinyals, Simon Osindero, Karen Simonyan, Jack W. Rae, Erich Elsen, and Laurent Sifre · 2022
Later among the works it cites.
The Isabelle ENIGMA
Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, and Josef Urban · 2022
Later among the works it cites.
Proof artifact co-training for theorem proving with language models
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu · 2022
Later among the works it cites.
Training compute-optimal large language models
Jordan Hoffmann, Sebastian Borgeaud, Arthur Mensch, Elena Buchatskaya, Trevor Cai, Eliza Rutherford, Diego de Las Casas, Lisa Anne Hendricks, Johannes Welbl, Aidan Clark, Tom Hennigan, Eric Noland, Katie Millican, George van den Driessche, Bogdan Damoc, Aurelia Guy, Simon Osindero, Karen Simonyan, Erich Elsen, Jack W. Rae, Oriol Vinyals, and Laurent Sifre · 2022
Later among the works it cites.
HyperTree proof search for neural theorem proving
Guillaume Lample, Timothee Lacroix, Marie Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet · 2022
Later among the works it cites.
Solving quantitative reasoning problems with language models
Aitor Lewkowycz, Anders Johan Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Venkatesh Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra · 2022
Later among the works it cites.
Text and code embeddings by contrastive pre-training, 2022
Arvind Neelakantan, Tao Xu, Raul Puri, Alec Radford, Jesse Michael Han, Jerry Tworek, Qiming Yuan, Nikolas Tezak, Jong Wook Kim, Chris Hallacy, Johannes Heidecke, Pranav Shyam, Boris Power, Tyna Eloundou Nekoul, Girish Sastry, Gretchen Krueger, David Schnurr, Felipe Petroski Such, Kenny Hsu, Madeleine Thompson, Tabarak Khan, Toki Sherbakov, Joanne Jang, Peter Welinder, and Lilian Weng · 2022
Later among the works it cites.
Formal premise selection with language models
Szymon Tworkowski, Maciej Mikuła, Tomasz Odrzygóźdź, Konrad Czechowski, Szymon Antoniak, Albert Jiang, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu · 2022
Later among the works it cites.
Memorizing transformers
Yuhuai Wu, Markus Norman Rabe, DeLesley Hutchins, and Christian Szegedy · 2022
Later among the works it cites.
miniF2F: A cross-system benchmark for formal olympiad-level mathematics
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu · 2022
Later among the works it cites.
Machine-learned premise selection for Lean
Bartosz Piotrowski, Ramon Fernández Mir, and Edward W. Ayers · 2023
Closest in time.
Formal mathematics statement curriculum learning
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever · 2023
Closest in time.
LeanDojo: Theorem proving with retrieval-augmented language models
Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar · 2023
Closest in time.