題目: 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.