Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving
This addresses the challenge of deep computer understanding of informal mathematical texts, which is incremental as it builds on existing parsing methods with enhanced techniques.
The paper tackled the problem of parsing informal mathematical expressions into formal ones by proposing a context-based approach that combines statistical learning with semantic pruning via type checking and theorem proving, achieving very significant improvements on the Flyspeck corpus.
We study methods for automated parsing of informal mathematical expressions into formal ones, a main prerequisite for deep computer understanding of informal mathematical texts. We 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 the methods very significantly improve on previous results in parsing theorems from the Flyspeck corpus.