論文の概要: Automatically discovering heuristics in a complex SAT solver with large language models

• arxiv url: http://arxiv.org/abs/2507.22876v1
• Date: Wed, 30 Jul 2025 17:52:25 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-07-31 16:14:18.377006
• Title: Automatically discovering heuristics in a complex SAT solver with large language models
• Title（参考訳）: 大規模言語モデルを持つ複素SATソルバにおけるヒューリスティックの自動発見
• Authors: Yiwen Sun, Furong Ye, Zhihan Chen, Ke Wei, Shaowei Cai,
• Abstract要約: SAT(Satisfiability problem)は、幅広い産業応用における計算複雑性の基盤である。 現代のSATソルバは手動による制約付き検索スペースに依存し、限られた性能向上をもたらす。 本研究は,Large Language Models (LLM) を用いた複雑なSATソルバを効果的に最適化する新しいパラダイムを導入する。
• 参考スコア（独自算出の注目度）: 9.96578394096009
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Satisfiability problem (SAT) is a cornerstone of computational complexity with broad industrial applications, and it remains challenging to optimize modern SAT solvers in real-world settings due to their intricate architectures. While automatic configuration frameworks have been developed, they rely on manually constrained search spaces and yield limited performance gains. This work introduces a novel paradigm which effectively optimizes complex SAT solvers via Large Language Models (LLMs), and a tool called AutoModSAT is developed. Three fundamental challenges are addressed in order to achieve superior performance: (1) LLM-friendly solver: Systematic guidelines are proposed for developing a modularized solver to meet LLMs' compatibility, emphasizing code simplification, information share and bug reduction; (2) Automatic prompt optimization: An unsupervised automatic prompt optimization method is introduced to advance the diversity of LLMs' output; (3) Efficient search strategy: We design a presearch strategy and an EA evolutionary algorithm for the final efficient and effective discovery of heuristics. Extensive experiments across a wide range of datasets demonstrate that AutoModSAT achieves 50% performance improvement over the baseline solver and achieves 30% superiority against the state-of-the-art (SOTA) solvers. Moreover, AutoModSAT attains a 20% speedup on average compared to parameter-tuned alternatives of the SOTA solvers, showcasing the enhanced capability in handling complex problem instances. This work bridges the gap between AI-driven heuristics discovery and mission-critical system optimization, and provides both methodological advancements and empirically validated results for next-generation complex solver development.
• Abstract（参考訳）: SAT問題(Satisfiability problem)は、幅広い産業アプリケーションにおいて計算複雑性の基盤となる問題であり、複雑なアーキテクチャのため、現代のSATソルバを現実の環境で最適化することは依然として困難である。 自動構成フレームワークは開発されているが、手動で制約された検索スペースに依存し、限られた性能向上をもたらす。 本研究は,Large Language Models (LLMs) による複雑なSATソルバを効果的に最適化する新しいパラダイムを導入し,AutoModSATと呼ばれるツールを開発した。 1) LLM フレンドリな解法: LLM の互換性を満たすためのモジュール化された解法を開発するための体系的ガイドライン,(2) コードの単純化,情報共有,バグの削減,(2) 自動迅速な最適化: LLM の出力の多様性を向上するために教師なしの自動迅速な最適化手法を導入;(3) 効率的な探索戦略: 事前探索戦略と EA 進化アルゴリズムを設計し,ヒューリスティックの最終的な効率的かつ効果的な発見を目指した。 幅広いデータセットにわたる大規模な実験により、AutoModSATはベースラインソルバよりも50%のパフォーマンス向上を実現し、最先端(SOTA)ソルバに対して30%の優位性を達成した。 さらに、AutoModSATは、SOTAソルバのパラメータ調整された代替品と比較して平均20%のスピードアップを実現し、複雑な問題インスタンスの処理能力の向上を示している。 この研究は、AI駆動のヒューリスティックス発見とミッションクリティカルシステム最適化のギャップを埋め、方法論的な進歩と、次世代の複素解法開発のための実証的な結果の両方を提供する。

関連論文リスト

• Grammar-Guided Evolutionary Search for Discrete Prompt Optimisation [63.97051732013936]
  本稿では,2段階からなる離散的な自動最適化に対する進化的探索手法を提案する。 第1段階では、文法誘導型遺伝的プログラミングが実行され、プロンプト生成プログラムを合成する。 第2段階では、局所探索を用いて、最高のパフォーマンスプログラムの周辺を探索する。
  論文  参考訳（メタデータ） (2025-07-14T14:34:15Z)
• CROP: Circuit Retrieval and Optimization with Parameter Guidance using LLMs [4.481239665281804]
  本稿では,最初の大規模言語モデル(LLM)を用いた自動VLSI設計フローチューニングフレームワークであるCROPを提案する。 提案手法は,(1)RTLソースコードを高密度ベクトル表現に変換するスケーラブルな手法,(2)意味的に類似した回路と設計をマッチングする埋め込み型検索システム,(3)検索強化型LLM誘導パラメータ探索システムを含む。 実験の結果、CROPのQoR(Quality-of-Results)の能力は、工業設計における既存のアプローチよりも少ないイテレーションで達成され、消費電力は9.9%削減された。
  論文  参考訳（メタデータ） (2025-07-02T20:25:47Z)
• Dynamic Location Search for Identifying Maximum Weighted Independent Sets in Complex Networks [0.47248250311484113]
  本稿では,最大重み付き独立集合(MWIS)問題を解くための,新しい,効率的なアルゴリズムを提案する。 MWIS問題のNPハード性を考えると,提案アルゴリズムであるDynLSには3つの重要なイノベーションが組み込まれている。 我々の実験結果はDynLSの優れた性能を示し、1000秒以内の高品質なソリューションを一貫して提供した。
  論文  参考訳（メタデータ） (2025-05-07T10:35:53Z)
• ZeroLM: Data-Free Transformer Architecture Search for Language Models [54.83882149157548]
  現在の自動プロキシ発見アプローチは、検索時間の拡張、データの過度なオーバーフィットへの感受性、構造的な複雑さに悩まされている。 本稿では,効率的な重み統計によるモデルキャパシティの定量化を目的とした,新しいゼロコストプロキシ手法を提案する。 本評価は,FlexiBERT ベンチマークで Spearman's rho 0.76 と Kendall's tau 0.53 を達成し,このアプローチの優位性を示すものである。
  論文  参考訳（メタデータ） (2025-03-24T13:11:22Z)
• SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code Generation [13.056487325961688]
  Satisfiability(SAT)問題は、ソフトウェア工学における重要な応用において、中核的な課題である。 本稿では,大規模言語モデル(LLM)を利用してSAT解決戦略の自動発見と最適化を行う新しいフレームワークであるSolSearchを提案する。
  論文  参考訳（メタデータ） (2025-02-20T07:25:21Z)
• Autoformulation of Mathematical Optimization Models Using LLMs [50.030647274271516]
  本稿では,自然言語問題記述から解法対応最適化モデルを自動生成する,$textitautoformulation$の問題にアプローチする。 オートフォーミュレーションの3つの主要な課題を識別する: $textit(1)$ 巨大で問題に依存した仮説空間、および$textit(2)$ 不確実性の下でこの空間を効率的かつ多様に探索する。 我々は,$textitLarge Language Models$と$textitMonte-Carlo Tree Search$を併用した新しい手法を提案する。
  論文  参考訳（メタデータ） (2024-11-03T20:41:38Z)
• 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)
• AutoSAT: Automatically Optimize SAT Solvers via Large Language Models [10.359005620433136]
  本稿では,既存のCDCLソルバをベースとしたモジュール型検索空間の自動最適化フレームワークであるAutoSATを提案する。 AutoSATは12データセット中9データセットでMiniSatを上回り、4データセットで最先端のハイブリッドソルバKissatを上回ります。
  論文  参考訳（メタデータ） (2024-02-16T14:04:56Z)
• Machine Learning Insides OptVerse AI Solver: Design Principles and Applications [74.67495900436728]
  本稿では,Huawei CloudのOpsVerse AIソルバに機械学習(ML)技術を統合するための総合的研究について述べる。 本稿では,実世界の多面構造を反映した生成モデルを用いて,複雑なSATインスタンスとMILPインスタンスを生成する手法を紹介する。 本稿では,解解器性能を著しく向上させる,最先端パラメータチューニングアルゴリズムの導入について詳述する。
  論文  参考訳（メタデータ） (2024-01-11T15:02:15Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)

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

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