論文の概要: Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis

• arxiv url: http://arxiv.org/abs/2401.17159v2
• Date: Tue, 30 Apr 2024 16:34:58 GMT
• ステータス: 処理完了
• システム内更新日: 2024-05-01 19:28:13.180105
• Title: Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis
• Title（参考訳）: SMT戦略合成のための層状および段状モンテカルロ木探索
• Authors: Zhengyang Lu, Stefan Siemer, Piyush Jha, Joel Day, Florin Manea, Vijay Ganesh,
• Abstract要約: 我々は、Z3 SMTソルバの一部として、Z3alphaと呼ばれる手法を実装した。 Z3alphaは、デフォルトのZ3ソルバであるSOTA合成ツールFastSMTや、ほとんどのベンチマークでCVC5ソルバよりも優れた性能を示している。
• 参考スコア（独自算出の注目度）: 7.348176676723853
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Modern SMT solvers, such as Z3, offer user-controllable strategies, enabling users to tailor solving strategies 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 heuristics 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 six 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.
• Abstract（参考訳）: Z3のような現代のSMTソルバはユーザ制御可能な戦略を提供しており、ユーザーは独自のインスタンスセットの解法をカスタマイズできるため、ユースケースの解法性能は劇的に向上する。 しかし、戦略カスタマイズのこのアプローチは、重要な課題である: SMTインスタンスのクラスに対して最適化された戦略を手作りすることは、解決者開発者とユーザの両方にとって、複雑で要求の多いタスクである。 本稿では,モンテカルロ木探索法(MCTS)を用いた自動SMT戦略合成の課題に対処する。 提案手法は,探索木が戦略空間に対応する逐次決定過程として戦略合成を扱い,MCTSを用いてこの広大な探索空間をナビゲートする。 コストを低く抑えながら有効な戦略を特定できる重要な革新は、層状およびステージ状MCTS探索の考え方である。 これらの新しいヒューリスティックは、戦略空間のより深くより効率的な探索を可能にし、SOTA(State-of-the-art) SMTソルバのデフォルト戦略よりも効果的な戦略を合成することができる。 我々は、Z3 SMTソルバの一部として、Z3alphaと呼ばれる手法を実装した。 Z3alphaは6つの重要なSMT論理の広範な評価を通じて、ほとんどのベンチマークにおいてデフォルトのZ3ソルバであるSOTA合成ツールであるFastSMTやCVC5ソルバよりも優れた性能を示す。 興味深いことに、難しいQF_BVベンチマークセットでは、Z3alphaはZ3 SMTソルバのデフォルト戦略よりも42.7%多くのインスタンスを解決している。

関連論文リスト

• LLaMA-Berry: Pairwise Optimization for O1-like Olympiad-Level Mathematical Reasoning [56.273799410256075]
  このフレームワークはMonte Carlo Tree Search (MCTS)と反復的なSelf-Refineを組み合わせて推論パスを最適化する。 このフレームワークは、一般的なベンチマークと高度なベンチマークでテストされており、探索効率と問題解決能力の点で優れた性能を示している。
  論文  参考訳（メタデータ） (2024-10-03T18:12:29Z)
• PartIR: Composing SPMD Partitioning Strategies for Machine Learning [1.1250231074374903]
  NNパーティショニングシステムの設計であるPartIRについて述べる。 PartIRは書き直しに対する漸進的なアプローチに重点を置いており、ハードウェアとランタイムに依存しない。 予測可能性,表現性,ピーク性能に到達する能力を示すために,いくつかの異なるモデルでPartIRを評価した。
  論文  参考訳（メタデータ） (2024-01-20T10:30:31Z)
• StrategyLLM: Large Language Models as Strategy Generators, Executors, Optimizers, and Evaluators for Problem Solving [76.5322280307861]
  StrategyLLM は LLM が帰納的推論、特定のタスクインスタンスからの一般的な戦略の導出、帰納的推論を可能にし、これらの一般的な戦略を特定のタスク例に適用し、一般化可能で一貫した数発のプロンプトを構築する。 実験の結果、StrategyLLMは、数学推論(34.2%$rightarrow$38.8%)、コモンセンス推論(70.3%$rightarrow$72.5%)、アルゴリズム推論(73.7%$rightarrow$85.0)を含む、4つの難しいタスクにまたがる13のデータセットに対して、人間によるアノテートソリューションを必要とする競争ベースラインのCoT-SCよりも優れていることが示された。
  論文  参考訳（メタデータ） (2023-11-15T09:18:09Z)
• GLS-CSC: A Simple but Effective Strategy to Mitigate Chinese STM Models' Over-Reliance on Superficial Clue [51.713301130055065]
  STMモデルにおける表面的手がかりの影響を解析・緩和する。 本稿では,GLS-CSC (Superficial Clue) を含む学習サンプルをトレーニング戦略として提案する。 GLS-CSCは,中国のSTMモデルの堅牢性と一般化性の向上の観点から,既存の手法よりも優れていることを示す。
  論文  参考訳（メタデータ） (2023-09-08T07:10:57Z)
• Layered controller synthesis for dynamic multi-agent systems [0.0]
  本稿では,多エージェント制御問題に対する階層的アプローチを3段階に分割する。 SWA-SMTソリューションは,ニューラルネットワーク制御ポリシ獲得を目的とした,最終段階の初期トレーニングデータセットとして使用しています。
  論文  参考訳（メタデータ） (2023-07-13T13:56:27Z)
• Choosing Well Your Opponents: How to Guide the Synthesis of Programmatic Strategies [19.143548378141062]
  Local Learner (2L) はゼロサムゲームにおけるプログラム戦略の探索をガイドする参照戦略のセットを提供するアルゴリズムである。 提案手法の利点を実証的に示すとともに,3つのゲームで戦略を合成するための局所探索アルゴリズムを導出する。
  論文  参考訳（メタデータ） (2023-07-10T20:31:23Z)
• Maximize to Explore: One Objective Function Fusing Estimation, Planning, and Exploration [87.53543137162488]
  我々はtextttMEX というオンライン強化学習(オンラインRL)フレームワークを提案する。 textttMEXは、自動的に探索エクスプロイトのバランスをとりながら、見積もりと計画コンポーネントを統合する。 様々な MuJoCo 環境では,ベースラインを安定的なマージンで上回り,十分な報酬を得られる。
  論文  参考訳（メタデータ） (2023-05-29T17:25:26Z)
• SemiNLL: A Framework of Noisy-Label Learning by Semi-Supervised Learning [58.26384597768118]
  SemiNLLはSS戦略とSSLモデルをエンドツーエンドで組み合わせた汎用フレームワークである。 我々のフレームワークは、様々なSS戦略やSSLバックボーンを吸収し、そのパワーを利用して有望なパフォーマンスを実現する。
  論文  参考訳（メタデータ） (2020-12-02T01:49:47Z)
• Revisiting LSTM Networks for Semi-Supervised Text Classification via Mixed Objective Function [106.69643619725652]
  我々は,単純なBiLSTMモデルであっても,クロスエントロピー損失でトレーニングした場合に,競争的な結果が得られるようなトレーニング戦略を開発する。 いくつかのベンチマークデータセット上で,テキスト分類タスクの最先端結果について報告する。
  論文  参考訳（メタデータ） (2020-09-08T21:55:22Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。