Isabelle/HOL中更快更智能的归纳
Faster Smarter Induction in Isabelle/HOL
摘要：
归纳证明在形式化验证和数学中起着重要的作用。然而，它的自动化仍然是计算机科学长期存在的挑战之一。为了解决这个问题，我们开发了sem_ind。给定归纳问题，sem_ind建议将哪些参数传递给induct方法。为了提高sem_ind的准确性，我们引入了定义量词，这是一种新的量词，它不仅允许我们研究归纳问题的句法结构，还允许我们以领域不可知的方式研究相关常数的定义。我们的评估表明，与其前身相比，sem_ind提高了推荐的准确性，从20.1%到38.2%，最有希望的候选人在5.0秒的超时，同时减少执行时间的中值从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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
