用实例化和策略发明解决困难的Mizar问题
人工智能
2024-06-26 v1 机器学习
计算机科学中的逻辑
符号计算
摘要
在这项工作中，我们通过使用多种ATP和AI方法，证明了超过3000个先前ATP无法证明的Mizar/MPTP问题，将ATP解决的Mizar问题数量从75%提高到80%以上。首先，我们开始用cvc5 SMT求解器进行实验，该求解器使用了多种基于实例化的启发式方法，这些方法不同于先前应用于Mizar的基于超位置的方法，并增加了许多新的解。然后，我们使用自动策略发明来开发cvc5策略，这些策略大大提高了cvc5在困难问题上的性能。特别是，最佳发明的策略比先前可用的最佳cvc5策略多解决了14%以上的问题。我们还表明，不同的子句化方法对此类基于实例化的方法有重大影响，同样产生了许多新的解。总的来说，这些方法解决了14163个先前未解决的困难Mizar问题中的3021个（21.3%）。这是Mizar大理论基准上的一个新里程碑，也是对Mizar锤击方法的重大加强。
引用
@article{arxiv.2406.17762,
title = {Solving Hard Mizar Problems with Instantiation and Strategy Invention},
author = {Jan Jakubův and Mikoláš Janota and Josef Urban},
journal= {arXiv preprint arXiv:2406.17762},
year = {2024}
}