@inproceedings{cunningham-etal-2022-towards,
title = "Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs",
author = "Cunningham, Garett and
Bunescu, Razvan and
Juedes, David",
editor = "Ferreira, Deborah and
Valentino, Marco and
Freitas, Andre and
Welleck, Sean and
Schubotz, Moritz",
booktitle = "Proceedings of the 1st Workshop on Mathematical Natural Language Processing (MathNLP)",
month = dec,
year = "2022",
address = "Abu Dhabi, United Arab Emirates (Hybrid)",
publisher = "Association for Computational Linguistics",
url = "https://aclanthology.org/2022.mathnlp-1.4",
doi = "10.18653/v1/2022.mathnlp-1.4",
pages = "25--32",
abstract = "The ever-growing complexity of mathematical proofs makes their manual verification by mathematicians very cognitively demanding. Autoformalization seeks to address this by translating proofs written in natural language into a formal representation that is computer-verifiable via interactive theorem provers. In this paper, we introduce a semantic parsing approach, based on the Universal Transformer architecture, that translates elementary mathematical proofs into an equivalent formalization in the language of the Coq interactive theorem prover. The same architecture is also trained to translate simple imperative code decorated with Hoare triples into formally verifiable proofs of correctness in Coq. Experiments on a limited domain of artificial and human-written proofs show that the models generalize well to intermediate lengths not seen during training and variations in natural language.",
}
<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="cunningham-etal-2022-towards">
<titleInfo>
<title>Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs</title>
</titleInfo>
<name type="personal">
<namePart type="given">Garett</namePart>
<namePart type="family">Cunningham</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Razvan</namePart>
<namePart type="family">Bunescu</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">David</namePart>
<namePart type="family">Juedes</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<originInfo>
<dateIssued>2022-12</dateIssued>
</originInfo>
<typeOfResource>text</typeOfResource>
<relatedItem type="host">
<titleInfo>
<title>Proceedings of the 1st Workshop on Mathematical Natural Language Processing (MathNLP)</title>
</titleInfo>
<name type="personal">
<namePart type="given">Deborah</namePart>
<namePart type="family">Ferreira</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Marco</namePart>
<namePart type="family">Valentino</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Andre</namePart>
<namePart type="family">Freitas</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Sean</namePart>
<namePart type="family">Welleck</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Moritz</namePart>
<namePart type="family">Schubotz</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<originInfo>
<publisher>Association for Computational Linguistics</publisher>
<place>
<placeTerm type="text">Abu Dhabi, United Arab Emirates (Hybrid)</placeTerm>
</place>
</originInfo>
<genre authority="marcgt">conference publication</genre>
</relatedItem>
<abstract>The ever-growing complexity of mathematical proofs makes their manual verification by mathematicians very cognitively demanding. Autoformalization seeks to address this by translating proofs written in natural language into a formal representation that is computer-verifiable via interactive theorem provers. In this paper, we introduce a semantic parsing approach, based on the Universal Transformer architecture, that translates elementary mathematical proofs into an equivalent formalization in the language of the Coq interactive theorem prover. The same architecture is also trained to translate simple imperative code decorated with Hoare triples into formally verifiable proofs of correctness in Coq. Experiments on a limited domain of artificial and human-written proofs show that the models generalize well to intermediate lengths not seen during training and variations in natural language.</abstract>
<identifier type="citekey">cunningham-etal-2022-towards</identifier>
<identifier type="doi">10.18653/v1/2022.mathnlp-1.4</identifier>
<location>
<url>https://aclanthology.org/2022.mathnlp-1.4</url>
</location>
<part>
<date>2022-12</date>
<extent unit="page">
<start>25</start>
<end>32</end>
</extent>
</part>
</mods>
</modsCollection>
%0 Conference Proceedings
%T Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs
%A Cunningham, Garett
%A Bunescu, Razvan
%A Juedes, David
%Y Ferreira, Deborah
%Y Valentino, Marco
%Y Freitas, Andre
%Y Welleck, Sean
%Y Schubotz, Moritz
%S Proceedings of the 1st Workshop on Mathematical Natural Language Processing (MathNLP)
%D 2022
%8 December
%I Association for Computational Linguistics
%C Abu Dhabi, United Arab Emirates (Hybrid)
%F cunningham-etal-2022-towards
%X The ever-growing complexity of mathematical proofs makes their manual verification by mathematicians very cognitively demanding. Autoformalization seeks to address this by translating proofs written in natural language into a formal representation that is computer-verifiable via interactive theorem provers. In this paper, we introduce a semantic parsing approach, based on the Universal Transformer architecture, that translates elementary mathematical proofs into an equivalent formalization in the language of the Coq interactive theorem prover. The same architecture is also trained to translate simple imperative code decorated with Hoare triples into formally verifiable proofs of correctness in Coq. Experiments on a limited domain of artificial and human-written proofs show that the models generalize well to intermediate lengths not seen during training and variations in natural language.
%R 10.18653/v1/2022.mathnlp-1.4
%U https://aclanthology.org/2022.mathnlp-1.4
%U https://doi.org/10.18653/v1/2022.mathnlp-1.4
%P 25-32
Markdown (Informal)
[Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs](https://aclanthology.org/2022.mathnlp-1.4) (Cunningham et al., MathNLP 2022)
ACL