Solving Hard Mizar Problems with Instantiation and Strategy Invention

要約

この研究では、いくつかの ATP および AI 手法を使用して、これまで ATP で証明されていなかった 3,000 を超える Mizar/MPTP 問題を証明し、ATP で解決される Mizar 問題の数を 75\% から 80\% 以上に引き上げました。
まず、以前に Mizar に適用されていた重ね合わせベースのシステムとは異なるいくつかのインスタンス化ベースのヒューリスティックを使用する cvc5 SMT ソルバーの実験を開始し、多くの新しいソリューションを追加します。
次に、自動戦略発明を使用して、難しい問題に対する cvc5 のパフォーマンスを大幅に向上させる cvc5 戦略を開発します。
特に、発明された最良の戦略は、以前に利用可能な最良の cvc5 戦略よりも 14\% 以上多くの問題を解決します。
また、さまざまな解明方法がそのようなインスタンス化ベースの方法に大きな影響を与え、やはり多くの新しい解決策が生み出されることも示します。
合計すると、この方法により、これまで未解決だった Mizar のハード問題 14163 件のうち 3021 件 (21.3\%) が解決されました。
これは、Mizar ラージ理論ベンチマークを超える新たなマイルストーンであり、Mizar のハンマー手法の大幅な強化です。

要約(オリジナル)

In this work, we prove over 3000 previously ATP-unproved Mizar/MPTP problems by using several ATP and AI methods, raising the number of ATP-solved Mizar problems from 75\% to above 80\%. First, we start to experiment with the cvc5 SMT solver which uses several instantiation-based heuristics that differ from the superposition-based systems, that were previously applied to Mizar,and add many new solutions. Then we use automated strategy invention to develop cvc5 strategies that largely improve cvc5’s performance on the hard problems. In particular, the best invented strategy solves over 14\% more problems than the best previously available cvc5 strategy. We also show that different clausification methods have a high impact on such instantiation-based methods, again producing many new solutions. In total, the methods solve 3021 (21.3\%) of the 14163 previously unsolved hard Mizar problems. This is a new milestone over the Mizar large-theory benchmark and a large strengthening of the hammer methods for Mizar.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google