Formally verifying the correctness of mathematical proofs is more accessible than ever, however, the learning curve remains steep for many of the state-of-the-art interactive theorem provers (ITP). Deriving the most appropriate subsequent proof step, and reasoning about it, given the multitude of possibilities, remains a daunting task for novice users. To improve the situation, several investigations have developed machine learning based guidance for tactic selection. Such approaches struggle to learn non-trivial relationships between the chosen tactic and the structure of the proof state and represent them as symbolic expressions. To address these issues we (i) We represent the problem as an Inductive Logic Programming (ILP) task, (ii) Using the ILP representation we enriched the feature space by encoding additional, computationally expensive properties as background knowledge predicates, (iii) We use this enriched feature space to learn rules explaining when a tactic is applicable to a given proof state, (iv) we use the learned rules to filter the output of an existing tactic selection approach and empirically show improvement over the non-filtering approaches.

翻译：形式化验证数学证明的正确性比以往任何时候都更加容易实现，然而，对于许多最先进的交互式定理证明器（ITP）而言，学习曲线仍然十分陡峭。在众多可能性中推导出最合适的后续证明步骤并对其进行推理，对于新手用户来说仍然是一项艰巨的任务。为了改善这种情况，已有若干研究开发了基于机器学习的策略选择指导方法。这类方法难以学习所选策略与证明状态结构之间的非平凡关系，并将其表示为符号表达式。为解决这些问题，我们（i）将问题表示为归纳逻辑编程（ILP）任务，（ii）利用ILP表示，通过将额外的、计算成本高昂的属性编码为背景知识谓词来丰富特征空间，（iii）使用这个丰富的特征空间来学习解释策略何时适用于给定证明状态的规则，（iv）使用学习到的规则来过滤现有策略选择方法的输出，并通过实验证明其相对于非过滤方法的改进。