一句话：提出 PaMpeR，基于手写证明语料为 Isabelle/HOL 的证明状态推荐证明方法并给出定性解释。
交互式定理证明器中，针对给定证明状态选择合适子工具依赖专家经验。本文提出 PaMpeR，一个面向 Isabelle/HOL 的证明方法推荐系统。它利用已有手写证明语料库，根据当前证明状态推荐可消解目标的证明方法，并提供为何推荐这些方法的定性解释，从而把有经验用户的专业知识迁移给新用户。评估表明，PaMpeR 能正确预测有经验用户调用的证明方法，尤其在专用证明方法上表现更好。
Deciding which sub-tool to use for a given proof state requires expertise specific to each interactive theorem prover (ITP). To mitigate this problem, we present PaMpeR , a proof method recommendation system for Isabelle/HOL. Given a proof state, PaMpeR recommends proof methods to discharge the proof goal and provides qualitative explanations as to why it suggests these methods. PaMpeR generates these recommendations based on existing hand-written proof corpora, thus transferring experienced users’ expertise to new users. Our evaluation shows that PaMpeR correctly predicts experienced users’ proof methods invocation especially when it comes to special purpose proof methods.
DOI 原文 ·
@inproceedings{paperbot4777,
title = {PaMpeR: proof method recommendation system for Isabelle/HOL},
author = {Yutaka Nagashima and Yilun He},
booktitle = {ASE},
year = {2018},
doi = {10.1145/3238147.3238210}
}