最近、制約解決と形式化の分野における国際的なトップコンペティションである 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 が従来の補助調整の限界を突破し、解決器のアルゴリズムやコード設計に深く関与し、新しい、未見のデータセット上で安定した再現可能な性能向上を形成できることを示しています。