SATNet: 深層学習と論理的推論を接続する微分可能な充足可能性ソルバーを使用して

現代のAIシステムにおいて、深層学習アーキテクチャ内に論理的推論を統合することは主要な目標の一つとなっています。本論文では、この目標に向けて新たな方向性を提案し、大規模な深層学習システムのループに組み込むことができる微分可能な（滑らか化された）最大充足問題（MAXSAT）ソルバーを導入します。我々の（近似）ソルバーは、MAXSAT問題に関連する半正定値計画問題（SDP）を解くための高速座標降下法に基づいています。このSDPの解に対して解析的に微分する方法と、関連する逆伝播を効率的に解く方法について説明します。我々は、このソルバーをエンドツーエンド学習システムに統合することで、最小限の教師あり学習で難問の論理構造を学習できる可能性を示します。特に、単一ビットの教師あり信号を使用してパリティ関数を学習する（従来、深層ネットワークにとって難しい課題）ことや、例のみから9x9の数独を解く方法を学習することについて示しています。さらに、「ビジュアル数独」問題も解決しました。これは、数独パズルの画像をその論理的な解にマッピングするもので、我々のMAXSATソルバーと従来の畳み込みアーキテクチャを組み合わせて解決しました。したがって、我々のアプローチは論理構造を深層学習に統合する上で有望であることが示されています。注：「ビジュアル数独」は原文では "visual Sudoku" と表記されており、一般的な日本語表現がないためそのまま引用しています。