最近、約束求解と形式化の分野における国際的なトップコンペティションであるSAT Competition 2026（満足性問題国際アルゴリズム競技）が終了しました。華為クラウド天籌AIソルバーチーム、華中科技大学のJohn Hopcroft計算センター、及び華為ノアの方舟研究所からなる合同チームが、並行AIトラックのSAT部門で優勝を果たしました。
報道によると、今回の大会には世界のトップ大学や機関から45チームが参加し、一つの大きな見どころはAIトラックが初めて設けられたことです。このトラックは、参加チームがAI技術を利用してソルバーをスマートに調整することを奨励しています。大会のルールに従い、AI調整に基づくソルバーは、最適な非AIソルバーを性能で上回らなければ賞を受けることができません。これは、AIが単なるパラメータ推薦や開発補助ツールとしてではなく、実際の、定量的で検証可能なアルゴリズム性能の向上をもたらさなければならないことを意味します。
AIトラックの設立はアルゴリズム設計の革新を示す
AIトラックの設立は、競技が従来の純粋なアルゴリズム設計の競争から、古典的なアルゴリズムとAIの融合による革新の新たな段階へと進化したことを示しています。今回の大会のデータセットには、ソフトウェアとハードウェアの検証、EDA、暗号解析、組合せ最適化などの応用分野における400の高難易度問題が含まれています。天籌AIソルバーチームが開発したソルバーKissat-MAB-HyPre-Evolveは、複雑な問題解決能力、並行検索効率、アルゴリズムの堅牢性などの総合的な優位性により、並行AIトラックのSAT部門で優勝を果たしました。
この結果は、AIが伝統的な補助調整の限界を突破し、ソルバーのアルゴリズムやコード設計に深く関与し、新たな、未見のデータセットにおいて安定した再現可能な性能向上を形成できることを示しています。