a

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.

 

Back