 |
13th International Conference on Artificial Intelligence and Symbolic Computation |
|---|
Speaker: Dr. Cezary Kaliszyk (University of Innsbruck, Austria)
Title: Automating Formalization using Statistical and Neural Approaches
Abstract:
The talk will give a summary of our experiments to automatically translate informal mathematical documents to proof formalizations. We will first introduce a context-based parsing approach that combined statistical deep parse trees with type checking and large-theory automated reasoning. We will next discuss the use of a neural translation model that automatically translates informalized Latex-written text to formal proof assistant languages. Parts of the work have been submitted as a joint paper with Qingxiang Wang and Josef Urban to CICM'18.