Magnushammer: A Transformer-based Approach to Premise Selection

要約

前提選択は、自動化された定理証明の基本的な問題です。
以前の研究では、複雑なシンボリック メソッドを使用し、ドメインの知識に依存し、このタスクを解決するために多大なエンジニアリング作業が必要になることがよくありました。
この作業では、ニューラル トランスフォーマー ベースのアプローチである Magnushammer が、従来のシンボリック システムよりも大幅に優れていることを示します。
PISA ベンチマークでテストされた Magnushammer は、最も成熟した人気のある記号ベースのソルバーである Sledgehammer の $38.3\%$ の証明率と比較して、$59.5\%$ の証明率を達成します。
さらに、Magnushammer を言語モデルに基づくニューラル形式証明器と組み合わせることで、これまでの最先端の証明率を $57.0\%$ から $71.0\%$ に大幅に改善します。

要約(オリジナル)

Premise selection is a fundamental problem of automated theorem proving. Previous works often use intricate symbolic methods, rely on domain knowledge, and require significant engineering effort to solve this task. In this work, we show that Magnushammer, a neural transformer-based approach, can outperform traditional symbolic systems by a large margin. Tested on the PISA benchmark, Magnushammer achieves $59.5\%$ proof rate compared to a $38.3\%$ proof rate of Sledgehammer, the most mature and popular symbolic-based solver. Furthermore, by combining Magnushammer with a neural formal prover based on a language model, we significantly improve the previous state-of-the-art proof rate from $57.0\%$ to $71.0\%$.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google