用逻辑编程教会AI理解定理证明中策略适用的规则。
Learning Rules Explaining Interactive Theorem Proving Tactic Prediction
- 将策略选择转为归纳逻辑编程任务，学习符号化规则。
- 通过背景知识引入复杂属性，提升特征表达能力。
- 学出的规则可过滤错误策略，适合初学者使用。
形式化验证数学证明如今更加便捷，但顶尖交互式定理证明器（ITP）对新手仍存在陡峭的学习曲线。面对众多可能的下一步证明步骤，如何选择并推理仍是难题。现有基于机器学习的策略推荐方法难以捕捉策略与证明状态结构之间的深层关系，并以符号表达呈现。为此，本文提出：(i) 将问题建模为归纳逻辑编程（ILP）任务；(ii) 利用ILP表示，通过背景知识谓词编码计算成本较高的额外属性，扩充特征空间；(iii) 在该增强特征空间中学习解释何时适用某一策略的规则；(iv) 使用所学规则过滤已有策略选择模型的输出，实证表明该方法优于无过滤方案。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。