Fetching the paper…
Reading the bibliography…
Theorem proving in natural mathematical language - the mixture of symbolic and natural language used by humans - plays a central role in mathematical advances and education, and tests aspects of reasoning that are core to intelligence.
The mathematical experience
Davis and Hersh · 1981
Earlier work this paper cites.
The role and function of proof in Mathematics
M. de Villiers · 1990
Earlier work this paper cites.
Learning to reason via instruction in argumentation
J. F. Voss and M. L. Means · 1991
Earlier work this paper cites.
Penn State Law eLibrary Journal Articles Faculty Works 1992, Proof in Law and Science
D. H. Kaye · 1992
Earlier work this paper cites.
Surprises from mathematics education research: Student (mis)use of mathematical definitions
B. S. Edwards and M. B. Ward · 2004
Earlier work this paper cites.
Gleu: Automatic evaluation of sentence-level fluency
A. Mutton, M. Dras, S. Wan, and R. Dale · 2007
Earlier work this paper cites.
Thinking Like a Lawyer
Erik G. Jensen · 2014
Earlier work this paper cites.
The lean theorem prover (system description)
L. M. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer · 2015
Earlier work this paper cites.
Guided open vocabulary image captioning with constrained beam search
P. Anderson, B. Fernando, M. Johnson, and S. Gould · 2017
Earlier work this paper cites.
Lexically constrained decoding for sequence generation using grid beam search
C. Hokamp and Q. Liu · 2017
Earlier work this paper cites.
Wizard of wikipedia: Knowledge-powered conversational agents
E. Dinan, S. Roller, K. Shuster, A. Fan, M. Auli, and J. Weston · 2019
Earlier work this paper cites.
Language models are unsupervised multitask learners
A. Radford, J. Wu, R. Child, D. Luan, D. Amodei, and I. Sutskever · 2019
Earlier work this paper cites.
Analysing mathematical reasoning abilities of neural models
D. Saxton, E. Grefenstette, F. Hill, and P. Kohli · 2019
Earlier work this paper cites.
Language models are few-shot learners
T. B. Brown, B. Mann, N. Ryder, M. Subbiah, J. Kaplan, P. Dhariwal, A. Neelakantan, P. Shyam, G. Sastry, A. Askell, S. Agarwal, A. Herbert-Voss, G. Krueger, T. J. Henighan, R. Child, A. Ramesh, D. M. Ziegler, J. Wu, C. Winter, C. Hesse, M. Chen, E. Sigler, M. Litwin, S. Gray, B. Chess, J. Clark, C. Berner, S. McCandlish, A. Radford, I. Sutskever, and D. Amodei · 2020
Earlier work this paper cites.
Natural language premise selection: Finding supporting statements for mathematical text
D. Ferreira and A. Freitas · 2020
Earlier work this paper cites.
Premise selection in natural language mathematical texts
D. Ferreira and A. Freitas · 2020
Cited alongside, same era.
The Pile: An 800gb dataset of diverse text for language modeling
L. Gao, S. Biderman, S. Black, L. Golding, T. Hoppe, C. Foster, J. Phang, H. He, A. Thite, N. Nabeshima, S. Presser, and C. Leahy · 2020
Cited alongside, same era.
Deep learning for symbolic mathematics
G. Lample and F. Charton · 2020
Cited alongside, same era.
Generative language modeling for automated theorem proving, 2020
S. Polu and I. Sutskever · 2020
Cited alongside, same era.
PRover: Proof generation for interpretable reasoning over rules
S. Saha, S. Ghosh, S. Srivastava, and M. Bansal · 2020
Cited alongside, same era.
A Promising Path Towards Autoformalization and General Artificial Intelligence , 2020
I. Drori, S. Zhang, R. Shuttleworth, L. Tang, A. Lu, E. Ke, K. Liu, L. Chen, S. Tran, N. Cheng, R. Wang, N. Singh, T. L. Patti, J. Lynch, A. Shporer, N. Verma, E. Wu, and G. Strang · 2021
Later among the works it cites.
Measuring mathematical problem solving with the math dataset, 2021
D. Hendrycks, C. Burns, S. Kadavath, A. Arora, S. Basart, E. Tang, D. Song, and J. Steinhardt · 2021
Later among the works it cites.
NeuroLogic decoding: (un)supervised neural text generation with predicate logic constraints
X. Lu, P. West, R. Zellers, R. Le Bras, C. Bhagavatula, and Y. Choi · 2021
Later among the works it cites.
Webgpt: Browser-assisted question-answering with human feedback
R. Nakano, J. Hilton, S. A. Balaji, J. Wu, L. Ouyang, C. Kim, C. Hesse, S. Jain, V. Kosaraju, W. Saunders, X. Jiang, K. Cobbe, T. Eloundou, G. Krueger, K. Button, M. Knight, B. Chess, and J. Schulman · 2021
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
C. Szegedy, editor · 2020
Cited alongside, same era.
First neural conjecturing datasets and experiments
J. Urban and J. Jakubuv · 2020
Cited alongside, same era.
Exploration of neural machine translation in autoformalization of mathematics in Mizar
Q. Wang, C. Brown, C. Kaliszyk, and J. Urban · 2020
Cited alongside, same era.
Program synthesis with large language models, 2021
J. Austin, A. Odena, M. Nye, M. Bosma, H. Michalewski, D. Dohan, E. Jiang, C. Cai, M. Terry, Q. Le, and C. Sutton · 2021
Cited alongside, same era.
On the opportunities and risks of foundation models
R. Bommasani, D. A. Hudson, E. Adeli, R. Altman, S. Arora, S. von Arx, M. S. Bernstein, J. Bohg, A. Bosselut, E. Brunskill, E. Brynjolfsson, S. Buch, D. Card, R. Castellon, N. S. Chatterji, A. S. Chen, K. Creel, J. Davis, D. Demszky, C. Donahue, M. Doumbouya, E. Durmus, S. Ermon, J. Etchemendy, K. Ethayarajh, L. Fei-Fei, C. Finn, T. Gale, L. E. Gillespie, K. Goel, N. D. Goodman, S. Grossman, N. Guha, T. Hashimoto, P. Henderson, J. Hewitt, D. E. Ho, J. Hong, K. Hsu, J. Huang, T. F. Icard, S. Jain, D. Jurafsky, P. Kalluri, S. Karamcheti, G. Keeling, F. Khani, O. Khattab, P. W. Koh, M. S. Krass, R. Krishna, R. Kuditipudi, A. Kumar, F. Ladhak, M. Lee, T. Lee, J. Leskovec, I. Levent, X. L. Li, X. Li, T. Ma, A. Malik, C. D. Manning, S. P. Mirchandani, E. Mitchell, Z. Munyikwa, S. Nair, A. Narayan, D. Narayanan, B. Newman, A. Nie, J. C. Niebles, H. Nilforoshan, J. F. Nyarko, G. Ogut, L. Orr, I. Papadimitriou, J. S. Park, C. Piech, E. Portelance, C. Potts, A. Raghunathan, R. Reich, H. Ren, F. Rong, Y. H. Roohani, C. Ruiz, J. Ryan, C. R’e, D. Sadigh, S. Sagawa, K. Santhanam, A. Shih, K. P. Srinivasan, A. Tamkin, R. Taori, A. W. Thomas, F. Tramèr, R. E. Wang, W. Wang, B. Wu, J. Wu, Y. Wu, S. M. Xie, M. Yasunaga, J. You, M. A. Zaharia, M. Zhang, T. Zhang, X. Zhang, Y. Zhang, L. Zheng, K. Zhou, and P. Liang · 2021
Cited alongside, same era.
Flexible generation of natural language deductions
K. Bostrom, X. Zhao, S. Chaudhuri, and G. Durrett · 2021
Cited alongside, same era.
Evaluating large language models trained on code
M. Chen, J. Tworek, H. Jun, Q. Yuan, H. P. d. O. Pinto, J. Kaplan, H. Edwards, Y. Burda, N. Joseph, G. Brockman, et al · 2021
Cited alongside, same era.
M. Nye, A. J. Andreassen, G. Gur-Ari, H. Michalewski, J. Austin, D. Bieber, D. Dohan, A. Lewkowycz, M. Bosma, D. Luan, C. Sutton, and A. Odena · 2021
Later among the works it cites.
Retrieval augmentation reduces hallucination in conversation
K. Shuster, S. Poff, M. Chen, D. Kiela, and J. Weston · 2021
Later among the works it cites.
ProofWriter: Generating implications, proofs, and abductive statements over natural language
O. Tafjord, B. Dalvi, and P. Clark · 2021
Later among the works it cites.
Naturalproofs: Mathematical theorem proving in natural language
S. Welleck, J. Liu, R. L. Bras, H. Hajishirzi, Y. Choi, and K. Cho · 2021
Later among the works it cites.
Towards teachable reasoning systems
B. Dalvi, O. Tafjord, and P. Clark · 2022
Closest in time.
Competition-level code generation with alphacode
Y. Li, D. Choi, J. Chung, N. Kushman, J. Schrittwieser, R. Leblond, T. Eccles, J. Keeling, F. Gimeno, A. D. Lago, et al · 2022
Closest in time.
Formal mathematics statement curriculum learning, 2022
S. Polu, J. M. Han, K. Zheng, M. Baksys, I. Babuschkin, and I. Sutskever · 2022
Closest in time.
Cold decoding: Energy-based constrained text generation with langevin dynamics
L. Qin, S. Welleck, D. Khashabi, and Y. Choi · 2022
Closest in time.
Chain of thought prompting elicits reasoning in large language models, 2022
J. Wei, X. Wang, D. Schuurmans, M. Bosma, E. Chi, Q. Le, and D. Zhou · 2022
Closest in time.
Symbolic brittleness in sequence models: on systematic generalization in symbolic mathematics
S. Welleck, P. West, J. Cao, and Y. Choi · 2022
Closest in time.