Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


LaTeX_to_Coq_Thesis.pdf (930.63 KB)

ETD Abstract Container

Abstract Header

Translating LaTeX to Coq: A Recurrent Neural Network Approach to Formalizing Natural Language Proofs

Carman, Benjamin Andrew
http://orcid.org/0000-0002-4354-6113
http://rave.ohiolink.edu/etdc/view?acc_num=ouhonors161919616626269

Abstract Details

2021, Bachelor of Science (BS), Ohio University, Computer Science.
There is a strong desire to be able to more easily formalize existing mathematical statements and develop machine-checked proofs to verify their validity. Doing this by hand can be a painstaking process with a steep learning curve. In this paper, we propose a model that could automatically parse natural language proofs written in LaTeX into the language of the interactive theorem prover, Coq, using a recurrent neural network. We aim to show the ability for such a model to work well within a very limited domain of proofs about even and odd expressions and exhibit generalization at test time. We demonstrate the model’s ability to generalize well given small variations in natural language and even demonstrate early promising results for the model to generalize to expressions of intermediate lengths unseen at training time.
David Juedes (Advisor)
48 p.
Computer Science
recurrent neural networks; RNN; LSTM; LaTeX; Coq; semantic parsing; PyTorch; attention; natural language processing; formal verification; proof

Recommended Citations

Citations

  • Carman, B. A. (2021). Translating LaTeX to Coq: A Recurrent Neural Network Approach to Formalizing Natural Language Proofs [Undergraduate thesis, Ohio University]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=ouhonors161919616626269

    APA Style (7th edition)

  • Carman, Benjamin. Translating LaTeX to Coq: A Recurrent Neural Network Approach to Formalizing Natural Language Proofs. 2021. Ohio University, Undergraduate thesis. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=ouhonors161919616626269.

    MLA Style (8th edition)

  • Carman, Benjamin. "Translating LaTeX to Coq: A Recurrent Neural Network Approach to Formalizing Natural Language Proofs." Undergraduate thesis, Ohio University, 2021. http://rave.ohiolink.edu/etdc/view?acc_num=ouhonors161919616626269

    Chicago Manual of Style (17th edition)

ouhonors161919616626269
1,062
© 2021, all rights reserved.
This open access ETD is published by Ohio University Honors Tutorial College and OhioLINK.