論文の概要: UNSAT Solver Synthesis via Monte Carlo Forest Search
- arxiv url: http://arxiv.org/abs/2211.12581v3
- Date: Sat, 13 Jul 2024 02:55:33 GMT
- ステータス: 処理完了
- システム内更新日: 2024-07-17 05:38:07.577517
- Title: UNSAT Solver Synthesis via Monte Carlo Forest Search
- Title（参考訳）: モンテカルロ森林探索によるUNSATソルバー合成
- Authors: Chris Cameron, Jason Hartford, Taylor Lundy, Tuan Truong, Alan Milligan, Rex Chen, Kevin Leyton-Brown,
- Abstract要約: 木MDPにおける学習ポリシーのための強化学習(RL)アルゴリズムであるモンテカルロ森林探索(MCFS)を紹介する。
そのような問題の例としては、SAT公式の不満足性の証明、SAT公式の解の数を数えることがある。
我々は,満足度(SAT)問題を解決するためにDPLL分岐ポリシーを学習するMCFSアルゴリズムであるKnuth Synthesisをダブした。
- 参考スコア（独自算出の注目度）: 10.754275929551593
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We introduce Monte Carlo Forest Search (MCFS), a class of reinforcement learning (RL) algorithms for learning policies in {tree MDPs}, for which policy execution involves traversing an exponential-sized tree. Examples of such problems include proving unsatisfiability of a SAT formula; counting the number of solutions of a satisfiable SAT formula; and finding the optimal solution to a mixed-integer program. MCFS algorithms can be seen as extensions of Monte Carlo Tree Search (MCTS) to cases where, rather than finding a good path (solution) within a tree, the problem is to find a small tree within a forest of candidate trees. We instantiate and evaluate our ideas in an algorithm that we dub Knuth Synthesis, an MCFS algorithm that learns DPLL branching policies for solving the Boolean satisfiability (SAT) problem, with the objective of achieving good average-case performance on a given distribution of unsatisfiable problem instances. Knuth Synthesis is the first RL approach to avoid the prohibitive costs of policy evaluations in an exponentially-sized tree, leveraging two key ideas: first, we estimate tree size by randomly sampling paths and measuring their lengths, drawing on an unbiased approximation due to Knuth (1975); second, we query a strong solver at a user-defined depth rather than learning a policy across the whole tree, to focus our policy search on early decisions that offer the greatest potential for reducing tree size. We matched or exceeded the performance of a strong baseline on three well-known SAT distributions, facing problems that were two orders of magnitude more challenging than those addressed in previous RL studies.
- Abstract（参考訳）: 我々は,モンテカルロ森林探索(MCFS)を紹介した。このアルゴリズムは,指数的規模の木を横断する政策実行を伴う,木MDPにおける政策学習のための強化学習(RL)アルゴリズムである。
そのような問題の例としては、SAT公式の不満足性の証明、SAT公式の解の数を数えること、混合整数プログラムの最適解を見つけることなどがある。
MCFSアルゴリズムはモンテカルロ木探索(MCTS)の拡張と見なすことができ、木の中に良い経路(解法)を見つけるのではなく、候補木のある森の中に小さな木を見つけることが問題となる。
Knuth Synthesis という DPLL 分岐ポリシーを学習してブール充足可能性 (SAT) 問題に対処するアルゴリズムを考案し,提案手法を検証した。
第1に、経路をランダムにサンプリングし、その長さを計測することで、木の大きさを推定し、Knuth (1975) による偏りのない近似に基づいて、木の大きさを推定する。
我々は,3つのよく知られたSAT分布において,従来のRL研究よりも2桁ほど難しい問題に直面した。
関連論文リスト
- 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。