Fetching the paper…
Reading the bibliography…
We present an environment, benchmark, and deep learning driven automated theorem prover for higher-order logic.
A new method of stochastic approximation type
Boris Teodorovich Polyak · 1990
Earlier work this paper cites.
Acceleration of stochastic approximation by averaging
Boris T Polyak and Anatoli B Juditsky · 1992
Earlier work this paper cites.
Metamath: A computer language for pure mathematics
Norman Megill · 1997
Earlier work this paper cites.
Learning search control knowledge for equational deduction , volume 230 of DISKI
Stephan Schulz · 2000
Earlier work this paper cites.
E - A Brainiac Theorem Prover
Stephan Schulz · 2002
Earlier work this paper cites.
leanCoP: lean connection-based theorem proving
Jens Otten and Wolfgang Bibel · 2003
Earlier work this paper cites.
The use of data-mining for the automatic formation of tactics
Hazel Duncan, A Bundy, J Levine, A Storkey, and M Pollet · 2004
Earlier work this paper cites.
The netflix prize
James Bennett, Stan Lanning, et al · 2007
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.
A brief overview of hol4
Konrad Slind and Michael Norrish · 2008
Earlier work this paper cites.
The isabelle framework
Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow · 2008
Earlier work this paper cites.
Liblinear: A library for large linear classification
Rong-En Fan, Kai-Wei Chang, Cho-Jui Hsieh, Xiang-Rui Wang, and Chih-Jen Lin · 2008
Earlier work this paper cites.
Imagenet: A large-scale hierarchical image database
Jia Deng, Wei Dong, Richard Socher, Li-Jia Li, Kai Li, and Li Fei-Fei · 2009
Earlier work this paper cites.
sel4: Formal verification of an os kernel
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood · 2009
Earlier work this paper cites.
Malecop machine learning connection prover
Josef Urban, Jiří Vyskočil, and Petr Štěpánek · 2011
Earlier work this paper cites.
Initial experiments with external provers and premise selection on hol light corpora
Cezary Kaliszyk and Josef Urban · 2012
Cited alongside, same era.
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
Cited alongside, same era.
Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions
Yves Bertot and Pierre Castéran · 2013
Cited alongside, same era.
Stronger automation for flyspeck by feature weighting and strategy evolution
Cezary Kaliszyk and Josef Urban · 2013
Cited alongside, same era.
Mash: machine learning for sledgehammer
Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban · 2013
Cited alongside, same era.
Microsoft coco: Common objects in context
Premise selection and external provers for hol4
Thibault Gauthier and Cezary Kaliszyk · 2015
Later among the works it cites.
Squad: 100,000+ questions for machine comprehension of text
Pranav Rajpurkar, Jian Zhang, Konstantin Lopyrev, and Percy Liang · 2016
Later among the works it cites.
Deepmath-deep sequence models for premise selection
Alexander A Alemi, François Chollet, Geoffrey Irving, Niklas Eén, Christian Szegedy, and Josef Urban · 2016
Later among the works it cites.
Holophrasm: a neural automated theorem prover for higher-order logic
Daniel Whalen · 2016
Later among the works it cites.
A learning-based fact selector for isabelle/hol
Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban · 2016
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Tsung-Yi Lin, Michael Maire, Serge Belongie, James Hays, Pietro Perona, Deva Ramanan, Piotr Dollár, and C Lawrence Zitnick · 2014
Cited alongside, same era.
Findings of the 2014 workshop on statistical machine translation
Ondrej Bojar, Christian Buck, Christian Federmann, Barry Haddow, Philipp Koehn, Johannes Leveling, Christof Monz, Pavel Pecina, Matt Post, Herve Saint-Amand, et al · 2014
Cited alongside, same era.
Learning-assisted automated reasoning with flyspeck
Cezary Kaliszyk and Josef Urban · 2014
Cited alongside, same era.
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.
Machine learning for first-order theorem proving
James P. Bridge, Sean B. Holden, and Lawrence C. Paulson · 2014
Cited alongside, same era.
Adam: A method for stochastic optimization
Diederik P Kingma and Jimmy Ba · 2014
Cited alongside, same era.
Librispeech: an asr corpus based on public domain audio books
Vassil Panayotov, Guoguo Chen, Daniel Povey, and Sanjeev Khudanpur · 2015
Cited alongside, same era.
Aäron Van Den Oord, Sander Dieleman, Heiga Zen, Karen Simonyan, Oriol Vinyals, Alex Graves, Nal Kalchbrenner, Andrew Senior, and Koray Kavukcuoglu · 2016
Later among the works it cites.
A formal proof of the kepler conjecture
Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al · 2017
Later among the works it cites.
Tactictoe: Learning to reason with hol4 tactics
Thibault Gauthier, Cezary Kaliszyk, and Josef Urban · 2017
Later among the works it cites.
Deep network guided proof search
Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk · 2017
Later among the works it cites.
Holstep: A machine learning dataset for higher-order logic theorem proving
Cezary Kaliszyk, François Chollet, and Christian Szegedy · 2017
Later among the works it cites.
Premise selection for theorem proving by deep graph embedding
Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng · 2017
Later among the works it cites.
Gamepad: A learning environment for theorem proving
Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever · 2018
Later among the works it cites.
The Mizar Mathematical Library
Mizar · 2018
Later among the works it cites.
Reinforcement learning of theorem proving
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Mirek Olšák · 2018
Later among the works it cites.
Curriculum learning and theorem proving
Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, and Josef Urban · 2019
Closest in time.