(Kaliszyk et al. 2017)[1]


Evaluation Edit

Parse evaluation only Edit

In Kaliszyk et al. 2017 Edit

  • Sentences are shuffled
  • 100-fold cross-validation
  • Evaluate 20 highest-ranked parses

ATP evaluation Edit

In Kaliszyk et al. 2017 Edit

  • Make use of chronological order
  • ...

Corpora Edit

  • Informalized Flyspeck (Kaliszyk et al. 2015[2])

?cited as additional annotation: T. Hales. Dense Sphere Packings: A Blueprint for Formal Proofs, volume 400 of London Mathematical Society Lecture Note Series. Cambridge University Press, 2012

People Edit

  • Cezary Kaliszyk (Innsbruck)
  • Josef Urban (Czech Technical University)
  • Jirı Vyskocil (Czech Technical University)

Projects Edit

References Edit

  1. Kaliszyk, C., Urban, J., & Vyskočil, J. (2017). Automating formalization by statistical and semantic parsing of mathematics. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 10499 LNCS(714034), 12–27.
  2. C. Kaliszyk, J. Urban, and J. Vyskocil. Learning to parse on aligned corpora (rough diamond). In C. Urban and X. Zhang, editors, Interactive Theorem Proving - 6th International Conference, ITP 2015, volume 9236 of LNCS, pages 227–233. Springer, 2015.