Exploration of neural machine translation in autoformalization of mathematics in Mizar
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F20%3A00346154" target="_blank" >RIV/68407700:21730/20:00346154 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.1145/3372885.3373827" target="_blank" >https://doi.org/10.1145/3372885.3373827</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1145/3372885.3373827" target="_blank" >10.1145/3372885.3373827</a>
Alternative languages
Result language
angličtina
Original language name
Exploration of neural machine translation in autoformalization of mathematics in Mizar
Original language description
In this paper we share several experiments trying to automatically translate informal mathematics into formal mathematics. In our context informal mathematics refers to humanwritten mathematical sentences in the LaTeX format; and formal mathematics refers to statements in the Mizar language. We conducted our experiments against three established neural network-based machine translation models that are known to deliver competitive results on translating between natural languages. To train these models we also prepared four informal-to-formal datasets. We compare and analyze our results according to whether the model is supervised or unsupervised. In order to augment the data available for auto-formalization and improve the results, we develop a custom type-elaboration mechanism and integrate it in the supervised translation.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/EF15_003%2F0000466" target="_blank" >EF15_003/0000466: Artificial Intelligence and Reasoning</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2020
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs
ISBN
978-1-4503-7097-4
ISSN
—
e-ISSN
—
Number of pages
14
Pages from-to
85-98
Publisher name
Association for Computing Machinery
Place of publication
New York
Event location
New Orleans
Event date
Jan 20, 2020
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000620147900009