Abstract

One of the first big hurdles that mathematicians encounter when considering writing formal proofs is the necessity to get acquainted with the formal terminology and the parsing mechanisms used in the large ITP libraries. This includes the large number of formal symbols, the grammar of the formal languages and the advanced mechanisms instrumenting the proof assistants to correctly understand the formal expressions in the presence of ubiquitous overloading.

In this work we start to address this problem by developing approximate probabilistic parsing techniques that autonomously train disambiguation on large corpora. Unlike in standard natural language processing, we can filter the resulting parse trees by strong ITP and AR semantic methods such as typechecking and automated theorem proving, and even let the probabilistic methods self-improve based on such semantic feedback. We describe the general motivation and our first experiments, and build an online system for parsing ambiguous formulas over the Flyspeck library.

BibTeX

@inproceedings{CKJUJV-IJCAI15,
  author    = "Cezary Kaliszyk and Josef Urban and Ji\v{r}\'i Vysko\v{c}il",
  title     = "Learning to Parse on Aligned Corpora (Rough Diamond)",
  booktitle = "Proceedings of the 6th International Conference on
               Interactive Theorem Proving (ITP 2015)",
  editor    = "Christian Urban and Xingyuan Zhang",
  series    = "Lecture Notes in Computer Science",
  volume    = 9236,
  pages     = "227--233",
  year      = 2015,
  doi       = "10.1007/978-3-319-22102-1_15"
}