数理・計算科学系 談話会 Cezary Kaliszyk 特任准教授

題目: Machine Learning Problems in Theorem Proving

概要:
As formalization becomes a more accepted means of establishing
correctness of mathematical theories, the usability of proof
assistants and the automation level which they provide becomes more
important. In this talk I will discuss various automated reasoning
tasks that give rise to machine learning problems. First, I will
present heuristic search for related mathematical knowledge. Next, we
will look at the choice of the optimal strategies for proof automation.
We will continue with internal guidance, the prediction of the actual
inference rules to apply at a given proof step. Finally we will look
at conjecture and intermediate lemma generation.