Automatic formalization

(Kaliszyk et al. 2017)^[1]

TODO: REAL_NEGNEG (HOL theorem)??

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

• ERC Starting grant no. 714034 SMART
• ERC Consolidator grant no. 649043 AI4REASON

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. http://doi.org/10.1007/978-3-319-66107-0_2
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.