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

• arxiv url: http://arxiv.org/abs/2402.10705v1
• Date: Fri, 16 Feb 2024 14:04:56 GMT
• ステータス: 処理完了
• システム内更新日: 2024-02-19 16:04:36.782827
• Title: AutoSAT: Automatically Optimize SAT Solvers via Large Language Models
• Title（参考訳）: AutoSAT: 大規模言語モデルによるSATソルバーの自動最適化
• Authors: Yiwen Sun, Xianyin Zhang, Shiyu Huang, Shaowei Cai, Bing-Zhen Zhang, Ke Wei
• Abstract要約: 本稿では,SATソルバの自動最適化のための新しいフレームワークであるAutoSATを紹介する。 AutoSATはLarge Large Models (LLMs)をベースにしており、コードを生成し、評価を行い、フィードバックを利用してソルバをさらに最適化することができる。 AutoSATはプラグイン・アンド・プレイベースで動作するため、大規模な予備設定やモデルトレーニングは不要である。
• 参考スコア（独自算出の注目度）: 11.526994073302888
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Heuristics are crucial in SAT solvers, while no heuristic rules are suitable for all problem instances. Therefore, it typically requires to refine specific solvers for specific problem instances. In this context, we present AutoSAT, a novel framework for automatically optimizing heuristics in SAT solvers. AutoSAT is based on Large Large Models (LLMs) which is able to autonomously generate code, conduct evaluation, then utilize the 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 preliminary setup and model training, and fosters a Chain of Thought collaborative process with fault-tolerance, ensuring robust heuristic optimization. Extensive experiments on a Conflict-Driven Clause Learning (CDCL) solver demonstrates the overall superior performance of AutoSAT, especially in solving some specific SAT problem instances.
• Abstract（参考訳）: SATソルバではヒューリスティックが重要であり、すべての問題インスタンスにヒューリスティックなルールは適合しない。 したがって、通常は特定の問題インスタンスの特定のソルバを洗練する必要がある。 本稿では,SATソルバのヒューリスティックスを自動的に最適化する新しいフレームワークであるAutoSATを紹介する。 AutoSATはLarge Large Models(LLM)をベースにしており、コードを生成し、評価を行い、フィードバックを利用してヒューリスティックスをさらに最適化し、人間の介入を減らし、解決能力を向上させる。 AutoSATはプラグイン・アンド・プレイベースで動作し、広範な予備設定やモデルトレーニングの必要性を排除し、フォールトトレランスを備えたChain of Thoughtの共同プロセスを促進し、堅牢なヒューリスティックな最適化を保証する。 CDCL(Conflict-Driven Clause Learning)ソルバに関する大規模な実験は、特に特定のSAT問題インスタンスの解決において、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)

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

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