Regularization in Spider-Style Strategy Discovery and Schedule Construction

要約

最高のパフォーマンスを達成するために、自動定理証明器は多くの場合、特定の問題に対して (順次または並行して) 試行されるさまざまな証明戦略のスケジュールに依存します。
この論文では、Andrei Voronkov のシステム Spider のアイデアに基づいて、TPTP ライブラリの FOF フラグメントをターゲットにし、そのスケジュールを構築する、Vampire Prover の戦略を発見する大規模な実験について報告します。
私たちはさまざまな角度からプロセスを検証し、CASC コンテスト用の強力なヴァンパイア スケジュールを取得することの難しさ (または容易さ) を議論し、スケジュールが目に見えない問題にどの程度一般化できると期待できるか、またどのような要因がこの特性に影響を与えるかを確立します。

要約(オリジナル)

To achieve the best performance, automatic theorem provers often rely on schedules of diverse proving strategies to be tried out (either sequentially or in parallel) on a given problem. In this paper, we report on a large-scale experiment with discovering strategies for the Vampire prover, targeting the FOF fragment of the TPTP library and constructing a schedule for it, based on the ideas of Andrei Voronkov’s system Spider. We examine the process from various angles, discuss the difficulty (or ease) of obtaining a strong Vampire schedule for the CASC competition, and establish how well a schedule can be expected to generalize to unseen problems and what factors influence this property.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google