Automating Formalization by Statistical and Semantic Parsing of Mathematics

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Automating Formalization by Statistical and Semantic Parsing of Mathematics

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Automating Formalization by Statistical and Semantic Parsing of Mathematics

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/EF15_003%2F0000466" target="_blank" >EF15_003/0000466: Umělá inteligence a uvažování</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2017

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Interactive Theorem Proving

ISBN

978-3-319-66106-3

ISSN

—

e-ISSN

—

Počet stran výsledku

16

Strana od-do

12-27

Název nakladatele

Springer

Místo vydání

Basel

Místo konání akce

Brasilia

Datum konání akce

26. 9. 2017

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—