Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving

TL;DR

This paper presents a novel context-based semantic parsing method that combines statistical learning, type checking, and theorem proving to improve the automated parsing of informal mathematical expressions into formal representations.

Contribution

It introduces a new parsing approach integrating deep statistical models with semantic pruning, significantly advancing formalization of informal math texts.

Findings

Improved parsing accuracy on Flyspeck corpus

Effective combination of statistical learning and theorem proving

Enhanced semantic understanding of informal mathematical expressions

Abstract

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.