論文の概要: SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code Generation

• arxiv url: http://arxiv.org/abs/2502.14328v1
• Date: Thu, 20 Feb 2025 07:25:21 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-21 14:28:57.748065
• Title: SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code Generation
• Title（参考訳）: SolSearch: 効率的なSAT-Solvingコード生成のためのLLM駆動フレームワーク
• Authors: Junjie Sheng, Yanqiu Lin, Jiehao Wu, Yanhong Huang, Jianqi Shi, Min Zhang, Xiangfeng Wang,
• Abstract要約: Satisfiability(SAT)問題は、ソフトウェア工学における重要な応用において、中核的な課題である。 本稿では,大規模言語モデル(LLM)を利用してSAT解決戦略の自動発見と最適化を行う新しいフレームワークであるSolSearchを提案する。
• 参考スコア（独自算出の注目度）: 13.056487325961688
• License:
• Abstract: The Satisfiability (SAT) problem is a core challenge with significant applications in software engineering, including automated testing, configuration management, and program verification. This paper presents SolSearch, a novel framework that harnesses large language models (LLMs) to discover and optimize SAT-solving strategies automatically. Leveraging a curriculum-based, trial-and-error process, SolSearch enables the LLM to iteratively modify and generate SAT solver code, thereby improving solving efficiency and performance. This automated SAT-solving paradigm has the advantage of being plug-and-play, allowing integration with any SAT solver and accelerating the development or design process of new SAT solvers (new methods). Our preliminary experimental results are encouraging by demonstrating that the LLM-powered paradigm improves state-of-the-art SAT solvers on general SAT benchmarks and significantly enhances the performance of the widely used Z3 solver (11\% on PAR-2 score). These results highlight the potential for using LLM-driven methods to advance solver adaptability and effectiveness in real-world software engineering challenges. Future research directions are discussed to further refine and validate this approach, offering a promising avenue for integrating AI with traditional software engineering tasks.
• Abstract（参考訳）: Satisfiability(SAT)問題は、自動テスト、構成管理、プログラム検証など、ソフトウェア工学における重要なアプリケーションにおいて、中核的な課題である。 本稿では,大規模言語モデル(LLM)を利用してSAT解決戦略の自動発見と最適化を行う新しいフレームワークであるSolSearchを提案する。 SolSearchはカリキュラムベースの試行錯誤プロセスを活用することで、LCMがSATソルバコードを反復的に修正・生成し、解決効率と性能を向上させる。 この自動SAT解決パラダイムは、プラグイン・アンド・プレイの利点があり、SATソルバと統合し、新しいSATソルバの開発・設計プロセス(新しい方法)を加速することができる。 予備実験の結果は, LLM のパラダイムが SAT ベンチマークにおける最先端 SAT ソルバを改良し,広く使用されている Z3 ソルバ (PAR-2 スコア 11 %) の性能を著しく向上することを示すものである。 これらの結果は、現実のソフトウェア工学の課題において、LLM駆動の手法が問題解決の適応性と有効性を向上させる可能性を強調している。 このアプローチをさらに洗練し、検証するために、今後の研究の方向性が議論され、AIを従来のソフトウェアエンジニアリングタスクに統合するための有望な道を提供する。

関連論文リスト

• Deeply Optimizing the SAT Solver for the IC3 Algorithm [0.23749905164931204]
  観測結果に基づいて,IC3におけるSATソルバの最適化について述べる。 バイナリヒープをバケットに置き換えて、一定時間操作を実現しています。 我々はこれらの最適化を統合した新しい軽量CDCL SATソルバであるGipSATを開発した。
  論文  参考訳（メタデータ） (2025-01-24T12:40:43Z)
• OptiBench Meets ReSocratic: Measure and Improve LLMs for Optimization Modeling [62.19438812624467]
  大規模言語モデル (LLM) は数学的推論における問題解決能力を示した。 本稿では,人間可読入力と出力を用いたエンドツーエンド最適化問題のベンチマークであるOptiBenchを提案する。
  論文  参考訳（メタデータ） (2024-07-13T13:27:57Z)
• 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)
• SEGO: Sequential Subgoal Optimization for Mathematical Problem-Solving [64.38649623473626]
  大規模言語モデル(LLM)は人工知能の大幅な進歩を導いた。 数学的問題を解く能力を高めるために,textbfSEquential subtextbfGoal textbfOptimization (SEGO) という新しいフレームワークを提案する。
  論文  参考訳（メタデータ） (2023-10-19T17:56:40Z)
• 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)
• W2SAT: Learning to generate SAT instances from Weighted Literal Incidence Graphs [11.139131079925113]
  W2SATは、現実世界/産業インスタンスから固有の構造と特性を学ぶことによってSAT式を生成するフレームワークである。 Weighted Literal Incidence Graph (WLIG)と呼ばれる新しいSAT表現を導入する。 WLIGからSAT問題への復号化は、新しい丘登り最適化法で重なり合う斜角を見つけることをモデル化する。
  論文  参考訳（メタデータ） (2023-02-01T06:30:41Z)
• 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)

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

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