Fetching the paper…
Reading the bibliography…
Humans prove theorems by relying on substantial high-level reasoning and problem-specific insights.
Recursive functions of symbolic expressions and their computation by machine, part i
McCarthy, J · 1960
Earlier work this paper cites.
A learning algorithm for continually running fully recurrent neural networks
Williams, R. J. and Zipser, D · 1989
Earlier work this paper cites.
Isabelle: A generic theorem prover , volume 828
Paulson, L. C · 1994
Earlier work this paper cites.
Circuits as streams in coq: Verification of a sequential multiplier
Paulin-Mohring, C · 1995
Earlier work this paper cites.
Hol light: A tutorial introduction
Harrison, J · 1996
Earlier work this paper cites.
The Coq proof assistant reference manual: Version 6.1
Barras, B., Boutin, S., Cornes, C., Courant, J., Filliatre, J.-C., Gimenez, E., Herbelin, H., Huet, G., Munoz, C., Murthy, C., et al · 1997
Earlier work this paper cites.
Solution of the robbins problem
McCune, W · 1997
Earlier work this paper cites.
Formal verification in hardware design: a survey
Kern, C. and Greenstreet, M. R · 1999
Earlier work this paper cites.
A tactic language for the system coq
Delahaye, D · 2000
Earlier work this paper cites.
Isaplanner: A prototype proof planner in isabelle
Dixon, L. and Fleuriot, J · 2003
Earlier work this paper cites.
Mptp–motivation, implementation, first experiments
Urban, J · 2004
Earlier work this paper cites.
A theorem proving approach to analysis of secure information flow
Darvas, Á., Hähnle, R., and Sands, D · 2005
Earlier work this paper cites.
Z3: An efficient smt solver
De Moura, L. and Bjørner, N · 2008
Earlier work this paper cites.
Formal verification of a realistic compiler
Leroy, X · 2009
Earlier work this paper cites.
The tptp problem library and associated infrastructure
Sutcliffe, G · 2009
Earlier work this paper cites.
Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers
Paulson, L. C. and Blanchette, J. C · 2010
Earlier work this paper cites.
Malecop machine learning connection prover
Urban, J., Vyskočil, J., and Štěpánek, P · 2011
Earlier work this paper cites.
On the naturalness of software
Hindle, A., Barr, E. T., Su, Z., Gabel, M., and Devanbu, P · 2012
Cited alongside, same era.
Lecture 6.5—RmsProp: Divide the gradient by a running average of its recent magnitude
Tieleman, T. and Hinton, G · 2012
Cited alongside, same era.
A machine-checked proof of the odd order theorem
Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O’Connor, R., Biha, S. O., et al · 2013
Cited alongside, same era.
First-order theorem proving and vampire
Kovács, L. and Voronkov, A · 2013
Cited alongside, same era.
System description: E 1.8
Schulz, S · 2013
Cited alongside, same era.
Machine learning for first-order theorem proving
Bridge, J. P., Holden, S. B., and Paulson, L. C · 2014
Cited alongside, same era.
Learning to represent programs with graphs
Allamanis, M., Brockschmidt, M., and Khademi, M · 2017
Later among the works it cites.
A formal proof of the kepler conjecture
Hales, T., Adams, M., Bauer, G., Dang, T. D., Harrison, J., Le Truong, H., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T. T., et al · 2017
Later among the works it cites.
End-to-end optimization of task-oriented dialogue model with deep reinforcement learning
Liu, B., Tur, G., Hakkani-Tur, D., Shah, P., and Heck, L · 2017
Later among the works it cites.
Deep network guided proof search
Loos, S., Irving, G., Szegedy, C., and Kaliszyk, C · 2017
Later among the works it cites.
End-to-end differentiable proving
Rocktäschel, T. and Riedel, S · 2017
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Cho, K., Van Merriënboer, B., Gulcehre, C., Bahdanau, D., Bougares, F., Schwenk, H., and Bengio, Y · 2014
Cited alongside, same era.
History of interactive theorem proving
Harrison, J., Urban, J., and Wiedijk, F · 2014
Cited alongside, same era.
Learning-assisted automated reasoning with flyspeck
Kaliszyk, C. and Urban, J · 2014
Cited alongside, same era.
Mizar: State-of-the-art and beyond
Bancerek, G., Byliński, C., Grabowski, A., Korniłowicz, A., Matuszewski, R., Naumowicz, A., Pak, K., and Urban, J · 2015
Cited alongside, same era.
Sepia: search for proofs using inferred automata
Gransden, T., Walkinshaw, N., and Raman, R · 2015
Cited alongside, same era.
Improved semantic representations from tree-structured long short-term memory networks
Tai, K. S., Socher, R., and Manning, C. D · 2015
Cited alongside, same era.
Premise selection for theorem proving by deep graph embedding
Wang, M., Tang, Y., Wang, J., and Deng, J · 2017
Later among the works it cites.
A syntactic neural model for general-purpose code generation
Yin, P. and Neubig, G · 2017
Later among the works it cites.
code2vec: Learning distributed representations of code
Alon, U., Zilberstein, M., Levy, O., and Yahav, E · 2018
Later among the works it cites.
Learning to solve smt formulas
Balunovic, M., Bielik, P., and Vechev, M · 2018
Later among the works it cites.
Hammer for coq: Automation for dependent type theory
Czajka, Ł. and Kaliszyk, C · 2018
Later among the works it cites.
Learning to prove with tactics
Gauthier, T., Kaliszyk, C., Urban, J., Kumar, R., and Norrish, M · 2018
Later among the works it cites.
Reinforcement learning of theorem proving
Kaliszyk, C., Urban, J., Michalewski, H., and Olšák, M · 2018
Later among the works it cites.
Holist: An environment for machine learning of higher-order theorem proving (extended version)
Bansal, K., Loos, S. M., Rabe, M. N., Szegedy, C., and Wilcox, S · 2019
Closest in time.
Generative code modeling with graphs
Brockschmidt, M., Allamanis, M., Gaunt, A. L., and Polozov, O · 2019
Closest in time.
Gamepad: A learning environment for theorem proving
Huang, D., Dhariwal, P., Song, D., and Sutskever, I · 2019
Closest in time.
A convolutional attention network for extreme summarization of source code
Allamanis, M., Peng, H., and Sutton, C · 2091
Closest in time.