論文の概要: Monte Carlo Forest Search: UNSAT Solver Synthesis via Reinforcement learning

• arxiv url: http://arxiv.org/abs/2211.12581v1
• Date: Tue, 22 Nov 2022 20:52:50 GMT
• ステータス: 処理完了
• システム内更新日: 2022-11-24 14:14:37.289766
• Title: Monte Carlo Forest Search: UNSAT Solver Synthesis via Reinforcement learning
• Title（参考訳）: モンテカルロ森林探索:強化学習によるUNSATソルバー合成
• Authors: Chris Cameron, Jason Hartford, Taylor Lundy, Tuan Truong, Alan Milligan, Rex Chen, Kevin Leyton-Brown
• Abstract要約: MCFSは、強い木探索ソルバを合成し、与えられた分布に対する不満足性を証明するためのオフラインアルゴリズムである。 本稿では, MCFS-SATを提案する。MCFS-SATは, 整合性(SAT)問題を解決するための分岐ポリシーを学習するためのMCFSの実装である。
• 参考スコア（独自算出の注目度）: 11.729374460065745
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We introduce Monte Carlo Forest Search (MCFS), an offline algorithm for automatically synthesizing strong tree-search solvers for proving \emph{unsatisfiability} on given distributions, leveraging ideas from the Monte Carlo Tree Search (MCTS) algorithm that led to breakthroughs in AlphaGo. The crucial difference between proving unsatisfiability and existing applications of MCTS, is that policies produce trees rather than paths. Rather than finding a good path (solution) within a tree, the search problem becomes searching for a small proof tree within a forest of candidate proof trees. We introduce two key ideas to adapt to this setting. First, we estimate tree size with paths, via the unbiased approximation from Knuth (1975). Second, we query a strong solver at a user-defined depth rather than learning a policy across the whole tree, in order to focus our policy search on early decisions, which offer the greatest potential for reducing tree size. We then present MCFS-SAT, an implementation of MCFS for learning branching policies for solving the Boolean satisfiability (SAT) problem that required many modifications from AlphaGo. We matched or improved performance over a strong baseline on two well-known SAT distributions (\texttt{sgen}, \texttt{random}). Notably, we improved running time by 9\% on \texttt{sgen} over the \texttt{kcnfs} solver and even further over the strongest UNSAT solver from the 2021 SAT competition.
• Abstract（参考訳）: 我々は,モンテカルロ木探索 (mcts) アルゴリズムのアイデアを活用し,与えられた分布上で \emph{unsatisfiability} を証明するための強木探索ソルバを自動合成するオフラインアルゴリズムであるmonte carlo forest search (mcfs) を導入する。 MCTSの既存の応用と満足できないことを証明する重要な違いは、ポリシーが道ではなく木を生み出すことである。 木の中に良い経路(溶出)を見つける代わりに、探索問題は、候補となる証明木のある森内の小さな証明木を探すようになる。 この設定に適応するための2つの重要なアイデアを紹介します。 まず,knuth (1975) の非バイアス近似により,経路を持つ木の大きさを推定する。 第2に、木全体のポリシーを学ぶのではなく、ユーザ定義の深さで強力な解法をクエリし、木のサイズを減らす最大の可能性を提供する早期決定にポリシー検索を集中させる。 そこで我々は,AlphaGo から多くの修正を必要とする Boolean satisfiability (SAT) 問題を解くための分岐ポリシーを学習するための MCFS の実装である MCFS-SAT を提案する。 我々は,2つのよく知られたSAT分布(\texttt{sgen}, \texttt{random})の強いベースライン上での性能を一致または改善した。 特に,2021年のSATコンペティションにおいて,texttt{kcnfs} ソルバ上でのランニング時間を 9 % 改善し,UNSAT ソルバよりも高めに改善した。

関連論文リスト

• 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)
• LiteSearch: Efficacious Tree Search for LLM [70.29796112457662]
  本研究では,動的ノード選択とノードレベルの探索予算を備えた新しいガイド付き木探索アルゴリズムを提案する。 GSM8KおよびTabMWPデータセットを用いて行った実験により,本手法はベースライン法に比べて計算コストが大幅に低いことを示した。
  論文  参考訳（メタデータ） (2024-06-29T05:14:04Z)
• Autonomous Tree-search Ability of Large Language Models [58.68735916408101]
  大規模言語モデルは、高度なプロンプト技術で顕著な推論能力に優れています。 近年の研究では、LLMがより困難な推論タスクを解くために受動的木探索を行えるように、検索ロジックを定義するために外部プログラムを活用することが提案されている。 我々は,LLMの自律木探索能力という新しい概念を提案し,正しい解を求める探索軌跡を含む応答を自動生成する。
  論文  参考訳（メタデータ） (2023-10-14T14:14:38Z)
• Structure-Unified M-Tree Coding Solver for MathWord Problem [57.825176412485504]
  従来,数式表現の2次木構造を考慮に入れたモデルでは,性能が向上した。 本稿では、出力構造を統一するために、任意のM枝(M-tree)を持つ木を適用した構造統一M-Tree符号化(S-UMCr)を提案する。 広く使われているMAWPSとMath23Kデータセットの実験結果は、SUMC-rが複数の最先端モデルを上回るだけでなく、低リソース条件下でもはるかに優れた性能を発揮することを示した。
  論文  参考訳（メタデータ） (2022-10-22T12:20:36Z)
• Unbiased and Efficient Sampling of Dependency Trees [0.0]
  ほとんどのツリーバンクは、すべての有効な依存ツリーがROOTノードから出てくる単一のエッジを持つ必要がある。 Zmigrodらは最近、単一ルート依存ツリーの分布から置き換えることなくサンプリングするアルゴリズムを提案している。 我々は、Wilson-RCを置換したサンプリングアルゴリズムが実際にバイアスを受けていることを示す。
  論文  参考訳（メタデータ） (2022-05-25T09:57:28Z)
• CITS: Coherent Ising Tree Search Algorithm Towards Solving Combinatorial Optimization Problems [0.0]
  本稿では、マルコフ連鎖からSAに基づく奥行き制限木への探索空間の拡大による探索アルゴリズムを提案する。 それぞれのイテレーションにおいて、このアルゴリズムは、先を見据えて、木に沿って探索することで、実現可能な探索空間内で最高の準最適解を選択する」。 以上の結果から,IsingのNP最適化問題に対する高次木探索戦略は,より少ないエポックの範囲で解決可能であることが示唆された。
  論文  参考訳（メタデータ） (2022-03-09T10:07:26Z)
• What's Wrong with Deep Learning in Tree Search for Combinatorial Optimization [8.879790406465556]
  本稿では、NP-hard Maximum Independent Set問題に対するオープンソースのベンチマークスイートについて、その重み付けと非重み付けの両変種について述べる。 また,Li らによる木探索アルゴリズム (NeurIPS 2018) の詳細な解析を行い,小型および大規模合成および実世界のグラフ上で様々な構成を検証した。 木探索で用いられるグラフ畳み込みネットワークは,解構造の有意な表現を学ばず,実際にランダムな値に置き換えることができることを示す。
  論文  参考訳（メタデータ） (2022-01-25T17:37:34Z)
• Towards Optimally Efficient Tree Search with Deep Learning [76.64632985696237]
  本稿では,線形モデルから信号整数を推定する古典整数最小二乗問題について検討する。 問題はNPハードであり、信号処理、バイオインフォマティクス、通信、機械学習といった様々な応用でしばしば発生する。 本稿では, 深いニューラルネットワークを用いて, 単純化されたメモリバウンドA*アルゴリズムの最適推定を推定し, HATSアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2021-01-07T08:00:02Z)
• Exploring search space trees using an adapted version of Monte Carlo tree search for combinatorial optimization problems [0.6882042556551609]
  このアプローチでは,問題インスタンスの探索空間木を探索するアルゴリズムを用いる。 このアルゴリズムはモンテカルロ木探索(Monte Carlo tree search)をベースとしている。
  論文  参考訳（メタデータ） (2020-10-22T08:33:58Z)
• Parameterizing Branch-and-Bound Search Trees to Learn Branching Policies [76.83991682238666]
  Branch and Bound (B&B) は、Mixed-Integer Linear Programming Problem (MILP) の解法として一般的に用いられる木探索法である。 本稿では,新しい模倣学習フレームワークを提案し,分岐を表現するための新しい入力機能とアーキテクチャを提案する。
  論文  参考訳（メタデータ） (2020-02-12T17:43:23Z)

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

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