HOList: An Environment for Machine Learning of Higher-Order Theorem
Proving

HOList: An Environment for Machine Learning of Higher-Order Theorem Proving

5 April 2019

Christian Szegedy

Papers citing "HOList: An Environment for Machine Learning of Higher-Order Theorem Proving"

19 / 19 papers shown

Title
GamePad: A Learning Environment for Theorem Proving Daniel Huang Prafulla Dhariwal D. Song Ilya Sutskever 76 110 0 02 Jun 2018
Reinforcement Learning of Theorem Proving C. Kaliszyk Josef Urban Henryk Michalewski Miroslav Olsák 34 148 0 19 May 2018
Learning to Reason with HOL4 tactics Thibault Gauthier C. Kaliszyk Josef Urban 57 77 0 02 Apr 2018
Premise Selection for Theorem Proving by Deep Graph Embedding Mingzhe Wang Yihe Tang Jian Wang Jia Deng 58 133 0 28 Sep 2017
HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving C. Kaliszyk François Chollet Christian Szegedy 52 82 0 01 Mar 2017
Deep Network Guided Proof Search Sarah M. Loos G. Irving Christian Szegedy C. Kaliszyk AIMat 68 159 0 24 Jan 2017
WaveNet: A Generative Model for Raw Audio Aaron van den Oord Sander Dieleman Heiga Zen Karen Simonyan Oriol Vinyals Alex Graves Nal Kalchbrenner A. Senior Koray Kavukcuoglu DiffM 379 7,389 0 12 Sep 2016
Holophrasm: a neural Automated Theorem Prover for higher-order logic Daniel Whalen AIMat 61 50 0 08 Aug 2016
SQuAD: 100,000+ Questions for Machine Comprehension of Text Pranav Rajpurkar Jian Zhang Konstantin Lopyrev Percy Liang RALM 256 8,124 0 16 Jun 2016
DeepMath - Deep Sequence Models for Premise Selection Alexander A. Alemi François Chollet N. Eén G. Irving Christian Szegedy Josef Urban LRM AIMat 52 229 0 14 Jun 2016
Premise Selection and External Provers for HOL4 Thibault Gauthier C. Kaliszyk 25 47 0 11 Sep 2015
Adam: A Method for Stochastic Optimization Diederik P. Kingma Jimmy Ba ODL 1.7K 150,006 0 22 Dec 2014
Machine Learning of Coq Proof Guidance: First Experiments C. Kaliszyk L. Mamane Josef Urban LRM 25 17 0 20 Oct 2014
Microsoft COCO: Common Objects in Context Nayeon Lee Michael Maire Serge J. Belongie Lubomir Bourdev Ross B. Girshick James Hays Pietro Perona Deva Ramanan C. L. Zitnick Piotr Dollár ObjD 391 43,619 0 01 May 2014
Machine Learner for Automated Reasoning 0.4 and 0.5 C. Kaliszyk Josef Urban J. Vyskočil LRM 59 23 0 11 Feb 2014
Learning-assisted Theorem Proving with Millions of Lemmas C. Kaliszyk Josef Urban 73 47 0 11 Feb 2014
MizAR 40 for Mizar 40 C. Kaliszyk Josef Urban VLM AI4CE LRM AIMat 101 135 0 10 Oct 2013
Learning-Assisted Automated Reasoning with Flyspeck C. Kaliszyk Josef Urban LRM 78 162 0 29 Nov 2012
Premise Selection for Mathematics by Corpus Analysis and Kernel Methods Jesse Alama Tom Heskes D. Kühlwein Evgeni Tsivtsivadze Josef Urban LRM 82 147 0 17 Aug 2011