Fugu-MT 論文翻訳(概要): AutoSAT: Automatically Optimize SAT Solvers via Large Language Models

論文の概要: AutoSAT: Automatically Optimize SAT Solvers via Large Language Models

arxiv url: http://arxiv.org/abs/2402.10705v2
Date: Fri, 31 May 2024 11:38:00 GMT
ステータス: 処理完了
システム内更新日: 2024-06-03 19:52:35.357492
Title: AutoSAT: Automatically Optimize SAT Solvers via Large Language Models
Title（参考訳）: AutoSAT: 大規模言語モデルによるSATソルバーの自動最適化
Authors: Yiwen Sun, Xianyin Zhang, Shiyu Huang, Shaowei Cai, BingZhen Zhang, Ke Wei,
Abstract要約: 本稿では,SATソルバの自動最適化のための新しいフレームワークであるAutoSATを紹介する。 AutoSATは、コードの自動生成が可能なLarge Language Models (LLM)に基づいている。 AutoSATはプラグイン・アンド・プレイベースで動作し、広範なエンタープライズおよびモデルトレーニングの必要性を排除している。
参考スコア（独自算出の注目度）: 10.87846542244079
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Heuristics are crucial in SAT solvers, but no heuristic rules are suitable for all SAT problems. Therefore, it is helpful to refine specific heuristics for specific problems. In this context, we present AutoSAT, a novel framework for automatically optimizing heuristics in SAT solvers. AutoSAT is based on Large Language Models (LLMs) which is able to autonomously generate codes, conduct evaluation, and then utilize feedback to further optimize heuristics, thereby reducing human intervention and enhancing solver capabilities. AutoSAT operates on a plug-and-play basis, eliminating the need for extensive enterprise and model training, and fosters a Multi-Agent-based collaborative process with fault tolerance to ensure robust heuristic optimization. We implement AutoSAT on a lightweight Conflict-Driven Clause Learning (CDCL) solver EasySAT (the volume of EasySAT is about one-fiftieth of the State-of-the-Art hybrid solver Kissat) and extensive experiments on seven datasets demonstrate its superior performance. Out of the seven testing datasets, AutoSAT shows a superior performance to Kissat in two datasets and displays an overall similar performance in three datasets. Some heuristics generated by AutoSAT are even counter-intuitive but are very effective.
Abstract（参考訳）: SATソルバではヒューリスティックが重要であるが、すべてのSAT問題にはヒューリスティックなルールが適していない。したがって、特定の問題に対する特定のヒューリスティックスを洗練させるのに役立つ。本稿では,SATソルバのヒューリスティックスを自動的に最適化する新しいフレームワークであるAutoSATを紹介する。 AutoSATはLarge Language Models (LLMs)をベースにしており、コードを生成し、評価を行い、フィードバックを利用してヒューリスティックスをさらに最適化し、人間の介入を減らし、解決能力を向上させる。 AutoSATはプラグイン・アンド・プレイベースで動作し、広範なエンタープライズおよびモデルトレーニングの必要性を排除し、堅牢なヒューリスティック最適化を保証するために、フォールトトレランスを備えたマルチエージェントベースのコラボレーティブプロセスを促進する。我々は、軽量な衝突駆動クロース学習(CDCL)ソルバ、EasySAT(EasySATの体積は、State-of-the-ArtハイブリッドソルバKissatの約5分の1)にAutoSATを実装し、その優れた性能を示す7つのデータセットに関する広範な実験を行った。 7つのテストデータセットのうち、AutoSATは2つのデータセットでKissatよりも優れたパフォーマンスを示し、3つのデータセットで全体的な同様のパフォーマンスを示している。 AutoSATが生成したヒューリスティックは直感に反するものもあるが、非常に効果的である。

関連論文リスト

Resource-Constrained Heuristic for Max-SAT [0.848762374187855]
より大規模な問題をより小さなサブコンポーネントに繰り返し分解する,Max-SATのインスタンスに対するリソース制約を提案する。本研究では,所定のSATインスタンスの構造を利用するグラフベースの新しい手法を含む,変数選択手法の集合を分析する。我々は,Max-SAT評価ベンチマークを用いて,ランダムに生成されたMax-SATインスタンスと実世界の実例について実験を行った。
論文参考訳（メタデータ） (2024-10-11T18:20:08Z)
Navigating the Labyrinth: Evaluating and Enhancing LLMs' Ability to Reason About Search Problems [59.72548591120689]
我々は,11種類の検索問題を含む新しいベンチマークであるSearchBenchを紹介する。もっとも先進的なLCMでさえ、これらの問題をエンドツーエンドのテキストで解決することができないことを示す。 LLMにその問題を解決するコードを生成するように指示することは助けになるが、GPT4のパフォーマンスは11.7%向上した。
論文参考訳（メタデータ） (2024-06-18T00:44:58Z)
Machine Learning for SAT: Restricted Heuristics and New Graph Representations [0.8870188183999854]
SATは、自動スケジューリングを含む多くのアプリケーションにおいて、基本的なNP完全問題である。大きなインスタンスを解決するためには、SATソルバは、例えばDPLLとCDCLソルバの分岐変数を選択するなど、ブールアンに依存する必要がある。我々は、訓練されたMLモデルでいくつかの初期ステップを行い、古典的なランタイムに制御をリリースする戦略を提案する。
論文参考訳（メタデータ） (2023-07-18T10:46:28Z)
SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
論文参考訳（メタデータ） (2023-05-16T17:55:51Z)
Towards Tackling MaxSAT by Combining Nested Monte Carlo with Local Search [10.70006528984961]
UCTMAXSAT上でのアルゴリズム的バリエーションを2つ紹介する。まず、Nested Monte Carlo Searchアルゴリズムにインスパイアされた木探索のネストは、ベンチマークのほとんどのインスタンスタイプに有効である。第二に、SLSの静的フリップ制限を用いることで、理想的な予算はインスタンスサイズに大きく依存し、動的に設定することを提案する。
論文参考訳（メタデータ） (2023-02-26T03:37:26Z)
Efficient Adversarial Contrastive Learning via Robustness-Aware Coreset Selection [59.77647907277523]
敵対的コントラスト学習(ACL)は、高価なデータアノテーションを必要としないが、敵対的攻撃に耐える堅牢な表現を出力する。 ACLは、すべてのトレーニングデータの逆の変種を生成するのに、膨大な実行時間が必要です。本稿では,ACLの高速化を目的としたロバストネス対応コアセット選択(RCS)手法を提案する。
論文参考訳（メタデータ） (2023-02-08T03:20:14Z)
Efficient Non-Parametric Optimizer Search for Diverse Tasks [93.64739408827604]
興味のあるタスクを直接検索できる,スケーラブルで汎用的なフレームワークを初めて提示する。基礎となる数学表現の自然木構造に着想を得て、空間を超木に再配置する。我々は,モンテカルロ法を木探索に適用し,レジェクションサンプリングと等価形状検出を備える。
論文参考訳（メタデータ） (2022-09-27T17:51:31Z)
New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization [0.0]
本稿では,多目的組合せ最適化のための2つの新しい不満足性に基づくアルゴリズムを提案する。 1つはコア誘導MOCOソルバ、もう1つはヒットセットベースのMOCOソルバである。実験の結果,新しい不満足性に基づくアルゴリズムは,MOCOの最先端SATベースのアルゴリズムより優れていることがわかった。
論文参考訳（メタデータ） (2022-04-22T09:46:44Z)
Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
本論文は, Boolean satisfiability problem (SAT) を機械学習技術で解くことに関する最近の文献をレビューする。 ML-SATソルバを手作り特徴を持つナイーブ分類器からNeuroSATのような新たなエンド・ツー・エンドSATソルバまで,進化するML-SATソルバについて検討する。
論文参考訳（メタデータ） (2022-03-02T05:14:12Z)
Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文参考訳（メタデータ） (2021-07-15T04:47:35Z)

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

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