Automatically discovering heuristics in a complex SAT solver with large language models

基本情報

• arXiv ID: 2507.22876v1 (https://arxiv.org/abs/2507.22876v1)
• 著者: Yiwen Sun, Furong Ye, Zhihan Chen, Ke Wei, Shaowei Cai
• 所属: School of Data Science, Fudan University; Leiden Institute of Advanced Computer Science, Leiden University; Key Laboratory of System Software, Institute of Software, Chinese Academy of Sciences; School of Computer Science and Technology, University of Chinese Academy of Sciences
• 投稿日: 2025年07月31日
• カテゴリ: cs.AI, cs.LO

簡単に説明すると

AutoModSATは、大規模言語モデル（LLM）を活用して複雑なSATソルバーのヒューリスティクスを自動的に発見し最適化するツールです。SAT（充足可能性問題）は、与えられた論理式が真となるような変数の割り当てが存在するかを判定する問題です。ソフトウェア検証、人工知能、暗号解析などの産業応用において重要な役割を果たしています。

従来のSATソルバーは数十年にわたって手動で最適化されてきましたが、問題のタイプごとにチューニングが必要でした。AutoModSATは、LLMの推論能力を活用して、人間が設計した探索空間を超えた新しいヒューリスティクスを自動的に発見します。実験では、元のソルバーと比較して50%の性能向上を達成し、KissatやCadicalなどの高性能SATソルバーに対しても30%の優位性を示しました。

このプロジェクトは、AIによる複雑なソルバーの自動最適化における画期的な事例であり、ミッションクリティカルなシステム最適化への応用可能性を示しています。コードリポジトリへの言及は論文中にありませんが、産業応用を視野に入れた実用的な研究成果です。

1. 研究概要

1.1 背景と動機

SAT（充足可能性問題）は、論理学とコンピュータサイエンスにおける基本的な問題です。与えられたブール論理式を真にする変数割り当てが存在するかを判定します。最初に証明されたNP完全問題として計算複雑性の理論の礎石となっています。SATの多項式時間解法は全てのNPクラスの問題に対する多項式時間解法を意味します。

現代のSATソルバーは、半導体製造、サイバーセキュリティ、ミッションクリティカルなソフトウェア開発など、産業界の重要な応用を支える基盤技術となっています。しかし、数十年にわたる開発と改良により、現代のSATソルバーは複雑なヒューリスティクスを備えており、理論的な平均ケース分析に大きく抵抗してきました。

産業界のユーザーは、異なる実世界のアプリケーションに対して異なるSATソルバーをカスタマイズするために膨大な労力を費やす必要があります。例えば、EDA（電子設計自動化）タスクでは、SATソルバーが様々な複雑な問題インスタンスを処理する必要があります。これに対処するため、ハイパーパラメータ最適化アプローチが開発されてきました。しかし、これらのフレームワークは手動で定義された探索空間と限定的な性能改善という本質的な制限があります。

大規模言語モデル（LLM）の最近の進歩は、手動で設計されたフレームワークの制限を超える新しい機会を提供しています。DeepMindのFunSearchにおける先駆的な研究の後、LLMは自動アルゴリズム設計において有望な応用を示してきました。しかし、複雑なデータ構造と過度なコードベースのスケールという課題により、現代のSATソルバーのような複雑なプログラムの最適化にはほとんど成功していませんでした。

1.2 主要な貢献

本研究では、以下の3つの主要な貢献があります。

• 複雑なSATソルバーをLLMで最適化可能にするモジュール化されたソルバー（ModSAT）の開発。3つの指導原則（関数のシンプル化と焦点化、クラス変数による情報共有、バグの事前防止）に基づいて設計されており、LLMがローカルにヒューリスティクスを修正できるようにする。
• LLMの出力の多様性を高めるための教師なし自動プロンプト最適化手法の導入。シャノンエントロピーを評価指標として使用し、コード埋め込みのクラスタリングに基づいて多様性を定量化する。
• ヒューリスティクス発見を高速化するための前探索戦略と(1+λ)EA進化アルゴリズムの設計。小規模な予備テストで関数候補を剪定し、洗練されたサブセットで進化的探索を行うことで、組み合わせ爆発を緩和する。

2. 提案手法

2.1 手法の概要

AutoModSATは、LLMを活用して複雑なSATソルバーを最適化するフレームワークです。全体のワークフローは4つのコアコンポーネントで構成されています。

まず、モジュール化されたSATソルバー（ModSAT）を開発します。これは、LLMのトークン長制限と互換性を満たすように設計された、よく構造化された関数を持つソルバーです。ModSATでは、SATソルバーの性能に大きく影響する7つの重要なヒューリスティクスを定義し、LLMが探索する探索空間として提供します。

次に、自動プロンプト最適化を採用します。多様なプロンプトはLLMの出力を強化し、AutoModSATがより効果的なヒューリスティクスを発見できるようにします。シャノンエントロピーを評価指標とする教師なし自動プロンプト最適化手法を採用し、プロンプトエンジニアリングの労力を最小限に抑えながら、発見されるヒューリスティクスの性能を向上させます。

第三に、前探索戦略を導入します。まず、元のデータセットから50%の問題インスタンスで構成される代表的なサブセットを構築し、このコンパクトなサブセットで各候補関数のスタンドアロンでの影響を評価します。その後、洗練された関数セットを使用して、フルデータセットで(1+λ)EAを実行します。

最後に、最適化されたプロンプト、モジュール化されたSATソルバー、前探索の関数候補を取得した後、異なるシナリオでヒューリスティクスを発見します。このフェーズには、ヒューリスティクスの生成、実行可能なコードの統合、ソルバーの評価が含まれます。

2.2 技術的詳細

ModSATの開発において、3つの指導原則に従っています。

第一に、「関数をシンプルで焦点を絞ったものに保つ」という原則です。LLMによって最適化される関数は、複雑なソルバーで一般的なものとは異なり、シンプルで明示的である必要があります。現代のソルバーはC/C++で実装されています。複雑なデータ構造と貧弱にモジュール化された関数を使用することが多いです。これによりLLMが変数スコープを誤解し、ソルバーを最適化する際に誤ったコードを生成する原因となります。

第二に、「共有情報にクラス変数を使用する」という原則です。元のソルバー実装では関数は通常少数の変数のみを使用しますが、LLMはヒューリスティクスの多様性を強化するために追加の変数と協調する傾向があります。そのため、プロンプトで全ての可能な変数の情報を提供する代わりに、関連するクラスメンバー変数のみをコンテキスト情報として提供します。

第三に、「ヒューリスティクス発見中のバグを積極的に防ぐ」という原則です。多くのコンパイルエラーは、欠落したインクルードや変数スコープの誤解釈などの一般的な問題から生じる直接的な解決策を持っています。バグを積極的に修正することは、LLMがより多様で正しいコードを生成するのに役立ちます。

自動プロンプト最適化では、CodeT5+埋め込みモデルを使用して合成されたコードの埋め込みを生成し、K-Means++を使用してクラスタリングを行います。各クラスタの確率分布を計算し、シャノンエントロピーH(X) = -Σp_i log(p_i)を計算します。高いエントロピースコアは、個体が探索空間全体により均一に分布していることを示唆し、探索を促進します。

2.3 新規性

AutoModSATの新規性は、以下の点にあります。

• LLMを使用して複雑なカスタマイズされたデータ構造と長いテキストコードを持つ大規模ソルバーを最適化する最初の成功例である。従来のLLMベースのアルゴリズム設計は単純なアルゴリズムに限定されていたが、本研究は実世界の複雑なソルバーに直接適用可能である。
• 従来のハイパーパラメータ最適化手法における人間設計の探索空間を超えて、LLMの推論能力を活用して競争力のあるヒューリスティクスプログラムを発見する。これにより、異なるアプリケーションシナリオ全体での反復的な手動チューニングを排除する。
• LLMとの互換性を満たすためのモジュール化アーキテクチャを開発し、複雑なソルバーを扱う際のトークン長制限を克服する。この方法論は、他の複雑なソルバーの最適化にも拡張可能である。

3. 実験結果

3.1 実験設定

実験では11のデータセットを選択しました。これには、SAT Competition 2023および2024から7つのデータセット、Picatで生成された3つのデータセット、実際の産業EDAシナリオからの1つのデータセットが含まれます。

SAT Competitionデータセットでは、20未満のインスタンスを持つファミリーをフィルタリングし、平均解決時間に大きな変動があるデータセットを選択しました。これにより、argumentation_2023、argumentation_2024、cryptography-ascon、register-allocation、social-golfer、hashtable-safetyの7つのファミリーが選ばれました。

ベースラインとして、クラシックなCDCLベースのSATソルバーMiniSatに加えて、最先端のSATソルバーKissatとCadicalと比較しました。これらのソルバーの性能は、ハイブリッドヒューリスティクスと複雑なデータ構造を通じて完全に最適化されています。さらに、SMAC3（Sequential Model-based Algorithm Configuration）を使用してパラメータチューニングを行ったバージョンとも比較しました。

実験設定では、LLMへの新しいヒューリスティクスのリクエストまたはSMAC3への新しいパラメータのリクエスト回数を表す予算Bを50に設定しました。DeepSeek-V3を使用した場合のAutoModSATの優れた性能により、本論文ではこの結果のみを報告します。標準的な5000秒のタイムアウトは過度に長いため、トレーニングでは元のソルバーから報告された中央値の解決時間の半分をタイムアウト閾値として使用しました。

3.2 主要な結果

実験結果は、AutoModSATが評価された全てのデータセットで既存のSATソルバーを大幅に上回ることを示しています。

ModSATに対して、AutoModSATは50%以上の性能改善を達成しました。これは実質的な進歩です。さらに、AutoModSATは各データセットで他の最先端ソルバーに対して実質的な改善を示し、平均で30%を超える性能向上を達成しました。

パラメータチューニングされたベースラインソルバー（"para"として表記）は、一般的に全てのデータセットで元のものよりも改善された性能を示しました。それにもかかわらず、AutoModSATは一貫してパラメータチューニングされたModSATソルバーを30%のスピードアップで上回り、最先端ソルバー（KissatとCadiCal）のパラメータチューニングされた代替品と比較して平均20%のスピードアップを達成しました。

具体的には、11のデータセットのうち8つ（cryptography-ascon、register-allocation、social-golfer、hashtable-safety、Hamiltonian、EDA、Minesweeper）で最短のPAR-2スコアを達成し、同時に解決されたインスタンス数を一致または超過しました。これは、AutoModSATが既存の最先端ソルバーとそのファインチューニングされた対応物を全体的に上回る高効率なヒューリスティクスを発見できることを示しています。

3.3 既存手法との比較

AutoModSATは、特に暗号学、システム検証、グラフベースの問題で優れた性能を発揮する堅牢で効率的なソルバーとして確立されています。デフォルトバージョンとパラメータ最適化バージョンの両方の最先端ソルバーを一貫して上回る能力は、最適化フレームワークの有効性を強調しています。

例えば、register-allocationデータセットでは、ModSATのPAR-2スコアが7213.23（5つのインスタンスを解決）だったのに対し、AutoModSATは1177.8（18のインスタンスを解決）を達成しました。これは、パラメータチューニングされたKissat（6321.95、8つのインスタンスを解決）やCadical（8774.00、3つのインスタンスを解決）よりもはるかに優れています。

hashtable-safetyデータセットでは、AutoModSATは60.82のPAR-2スコアを達成し、ModSAT（83.25）、Kissat（456.8）、Cadical（252.29）を大幅に上回りました。これらの結果は、AutoModSATがリソース集約的なドメインで特に効果的であることを示しています。

探索プロセスの分析では、各データセットで3つのヒューリスティクス発見実験を実行しました。各実行で、LLMは異なる関数にわたって複数の有用なヒューリスティクスを生成し、最終的な結果に集合的に貢献しました。これは、AutoModSATが各データセットに対して段階的に効果的なヒューリスティクスを生成することを示しています。

4. 実用性評価

4.1 実装の容易性

AutoModSATは、既存のSATソルバーインフラストラクチャとの統合を考慮して設計されています。システムは3つの独立したコンポーネントで構成されており、段階的な導入と独立した最適化が可能です。

しかし、実装にはいくつかの課題があります。まず、大規模LLMの展開と推論インフラストラクチャの構築が必要です。次に、ユーザー行動データの効率的な圧縮と処理パイプラインの実装が必要です。さらに、既存のSATソルバーとの統合と互換性の確保も重要です。

産業界での大規模な応用では、既存のインフラストラクチャと専門知識を活用できる場合がありますが、小規模な組織では実装コストが増大する可能性があります。それでも、AutoModSATのモジュール化アプローチにより、組織は段階的に採用し、最も影響の大きいコンポーネントから始めることができます。

4.2 計算効率

AutoModSATは、計算効率を向上させるための複数の最適化手法を採用しています。

前探索戦略により、組み合わせ爆発を効果的に緩和しています。元のデータセットの50%で構成される代表的なサブセットで予備テストを行い、高影響の関数を特定することで、完全な最適化に必要な反復回数を大幅に削減します。経験的に、この戦略により最適化の複雑さを75%削減できます。

さらに、LLMトークン制限への対処として、ModSATはよく構造化された関数と明確なインターフェースを持つように設計されており、LLMがコード全体を理解することなくローカルな修正を行えるようになっています。これにより、各ヒューリスティクス生成の計算コストが削減されます。

評価フェーズでは、トレーニング中に短縮されたタイムアウト（元の中央値の解決時間の半分）を使用することで、計算オーバーヘッドを大幅に削減しながら、意味のある性能評価を維持しています。

4.3 応用可能性

AutoModSATのアプローチは、SAT以外の複雑なソルバーにも拡張可能です。提案された3つの原則（関数のシンプル化、クラス変数の使用、バグの事前防止）は、他の最適化問題のソルバーにも適用できる一般的なガイドラインです。

具体的な応用分野としては以下が考えられます。

• 制約充足問題（CSP）ソルバー：SATと同様の構造を持つため、直接的な拡張が可能
• 混合整数計画法（MIP）ソルバー：複雑なヒューリスティクスを持つため、同様のアプローチが有効
• SMTソルバー：SATの拡張であるため、技術的な適応により適用可能
• グラフアルゴリズム：最短経路や最大フローなどの問題に対するヒューリスティクス最適化

産業界では、特定のドメインに特化したソルバーの需要が高いため、AutoModSATのような自動最適化アプローチは大きな価値を提供します。電子設計自動化、ソフトウェア検証、スケジューリング、暗号解析など、様々な分野での応用が期待されます。

5. まとめと所感

5.1 論文の意義

本研究は、LLMを通じて複雑なSATソルバーを自動的に最適化する新しいパラダイムを導入しました。知る限り、複雑なソルバーを最適化するための最初の体系的なフレームワークであり、複数のデータセットでサブ最先端のベースラインから最先端の結果を超えるまでの性能飛躍を実現しました。

AutoModSATの最も重要な貢献は、理論的な可能性と実際の実装のギャップを埋めたことです。従来のAI研究でのアルゴリズム設計の快適ゾーンを超えて、実世界の複雑な問題に直接対処し、実用的な応用に貢献することを目指しています。

特に注目すべきは、人間が設計した探索空間を超えたヒューリスティクスの発見能力です。LLMが生成したヒューリスティクスの分析により、従来のSATソルバーの実装を超越する新しいヒューリスティクスを発見できることが示されました。例えば、動的再起動戦略やレベルベースの変数活性化など、人間の認知バイアスを克服し、反直感的なヒューリスティクスを発見する能力を示しています。

5.2 今後の展望

現在のLLMベースの最適化手法にはまだいくつかの課題があります。

第一に、ベースラインのモジュール化されたソルバーの性能を向上させる必要があります。ModSATは最先端のソルバーよりも性能が劣るため、より高性能なベースラインから始めることで、さらなる改善が期待できます。

第二に、より複雑で高品質なコードを生成するために、LLMの長文脈能力を改善する必要があります。現在の制限を超えることで、より洗練されたヒューリスティクスの発見が可能になります。

第三に、探索プロセスのフィードバックをより効果的に活用して次の探索を導く必要があります。現在の方法は各反復を独立して扱いますが、過去の成功と失敗から学習することで、より効率的な探索が可能になるでしょう。

これらの制限に対処することで、LLMは現在の最先端ソルバーを大幅に上回るソルバーを開発できる可能性があります。本研究は、複雑なソルバー最適化にLLMを適用するための基礎的なフレームワークと方法論的進歩を提供し、人工知能の応用における理論的可能性と実際の実装のギャップを埋める重要な一歩となります。