Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis

要約

Z3 などの最新の SMT ソルバーは、ユーザーが制御可能な戦略を提供しており、ユーザーが独自のインスタンス セットに合わせて戦略を調整できるため、ユースケースに合わせてソルバーのパフォーマンスが大幅に向上します。
ただし、この戦略カスタマイズのアプローチには重大な課題があります。SMT インスタンスのクラスに対して最適化された戦略を手作りすることは、ソルバー開発者とユーザーの両方にとって依然として複雑で困難な作業です。
この論文では、新しいモンテカルロ ツリー検索 (MCTS) ベースの方法を介して自動 SMT 戦略合成の問題に取り組みます。
私たちの方法では、戦略合成を逐次的な意思決定プロセスとして扱い、その検索ツリーが戦略空間に対応し、MCTS を使用してこの広大な検索空間をナビゲートします。
コストを低く抑えながら、私たちの方法で効果的な戦略を特定できるようにする主な革新は、階層化および段階的な MCTS 検索のアイデアです。
これらの新しいアプローチにより、戦略空間をより深く効率的に探索できるようになり、最先端 (SOTA) SMT ソルバーのデフォルトの戦略よりも効果的な戦略を合成できるようになります。
Z3alpha と呼ばれるメソッドを Z3 SMT ソルバーの一部として実装します。
6 つの重要な SMT ロジックにわたる広範な評価を通じて、Z3alpha は、SOTA 合成ツール FastSMT、デフォルトの Z3 ソルバー、およびほとんどのベンチマークで CVC5 ソルバーと比較して優れたパフォーマンスを実証します。
注目すべきことに、難しい QF_BV ベンチマーク セットでは、Z3alpha は、Z3 SMT ソルバーのデフォルト戦略よりも 42.7% 多くのインスタンスを解決します。

要約(オリジナル)

Modern SMT solvers, such as Z3, offer user-controllable strategies, enabling users to tailor them for their unique set of instances, thus dramatically enhancing solver performance for their use case. However, this approach of strategy customization presents a significant challenge: handcrafting an optimized strategy for a class of SMT instances remains a complex and demanding task for both solver developers and users alike. In this paper, we address this problem of automatic SMT strategy synthesis via a novel Monte Carlo Tree Search (MCTS) based method. Our method treats strategy synthesis as a sequential decision-making process, whose search tree corresponds to the strategy space, and employs MCTS to navigate this vast search space. The key innovations that enable our method to identify effective strategies, while keeping costs low, are the ideas of layered and staged MCTS search. These novel approaches allow for a deeper and more efficient exploration of the strategy space, enabling us to synthesize more effective strategies than the default ones in state-of-the-art (SOTA) SMT solvers. We implement our method, dubbed Z3alpha, as part of the Z3 SMT solver. Through extensive evaluations across 6 important SMT logics, Z3alpha demonstrates superior performance compared to the SOTA synthesis tool FastSMT, the default Z3 solver, and the CVC5 solver on most benchmarks. Remarkably, on a challenging QF_BV benchmark set, Z3alpha solves 42.7% more instances than the default strategy in the Z3 SMT solver.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google