论文标题
Isabelle/Hol的更快智能感应速度
Faster Smarter Induction in Isabelle/HOL
论文作者
论文摘要
通过归纳证明在整个正式验证和数学中起着至关重要的作用。但是，它的自动化仍然是计算机科学中长期存在的挑战之一。为了解决这个问题，我们开发了SEM_IND。给定归纳问题，SEM_IND建议将哪些论点传递给归纳方法。为了提高SEM_IND的准确性，我们引入了定义性量词，这是一种新型的量词，使我们不仅可以研究归纳问题的句法结构，而且还可以研究相关常数的定义，以域 - 敏锐的样式。我们的评估表明，与其前任SEM_IND相比，建议在超时5.0秒内，最有前途的候选人的推荐准确性从20.1％提高到38.2％，同时将执行时间中值的中位数从2.79秒降低到1.06秒。
Proof by induction plays a critical role in formal verification and mathematics at large. However, its automation remains as one of the long-standing challenges in Computer Science. To address this problem, we developed sem_ind. Given inductive problem, sem_ind recommends what arguments to pass to the induct method. To improve the accuracy of sem_ind, we introduced definitional quantifiers, a new kind of quantifiers that allow us to investigate not only the syntactic structures of inductive problems but also the definitions of relevant constants in a domain-agnostic style. Our evaluation shows that compared to its predecessor sem_ind improves the accuracy of recommendation from 20.1% to 38.2% for the most promising candidates within 5.0 seconds of timeout while decreasing the median value of execution time from 2.79 seconds to 1.06 seconds.
