Automating Formalization by Statistical and Semantic Parsing of Mathematics
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F17%3A00319005" target="_blank" >RIV/68407700:21730/17:00319005 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.1007/978-3-319-66107-0_2" target="_blank" >https://doi.org/10.1007/978-3-319-66107-0_2</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-66107-0_2" target="_blank" >10.1007/978-3-319-66107-0_2</a>
Alternative languages
Result language
angličtina
Original language name
Automating Formalization by Statistical and Semantic Parsing of Mathematics
Original language description
We discuss the progress in our project which aims to automate formalization by combining natural language processing with deep semantic understanding of mathematical expressions. We introduce the overall motivation and ideas behind this project, and then propose a context-based parsing approach that combines efficient statistical learning of deep parse trees with their semantic pruning by type checking and large-theory automated theorem proving. We show that our learning method allows efficient use of large amount of contextual information, which in turn significantly boosts the precision of the statistical parsing and also makes it more efficient. This leads to a large improvement of our first results in parsing theorems from the Flyspeck corpus.
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
2017
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
Interactive Theorem Proving
ISBN
978-3-319-66106-3
ISSN
—
e-ISSN
—
Number of pages
16
Pages from-to
12-27
Publisher name
Springer
Place of publication
Basel
Event location
Brasilia
Event date
Sep 26, 2017
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—