LeanCSP、制約の書き換えとソルバー証明をLeanで検証し、探索量を最大2,000万分の1に削減

制約充足問題の求解は、スケジューリング、プランニング、配置などで広く利用されている。しかし、結果の信頼性はソルバーだけに左右されるわけではない。探索を高速化するための対称性の除去やモデル表現の変更も、元の問題を知らないうちに変えてしまう可能性がある。LeanCSPは、この2層のリスクをLean 4による検証の対象にする。開発者は、問題ファミリー全体について、2つの表現が等価または等充足可能であることや、特定の対称性除去によってすべての有効解が削除されないことを証明できる。同じパラメータ化された証明を、後から規模の異なるインスタンスに適用することも可能だ。

実際の求解は引き続きMiniZinc、Z3、cvc5、または疑似ブールソルバーに委ねられる。充足不能な問題については、検証済みのorder encodingによって整数制約をOPBへ変換し、RoundingSatで探索した後、VeriPBで証明を整形する。最後にPBLeanがLean内で証明書を再検査する。充足可能なケースでは、ソルバーが提供したwitnessを改めて照合する。このため、外部ソルバーを信頼基盤に含める必要はない。証明書、変換、witnessのいずれかに不整合があれば、Leanの定理は成立しない。

論文では、鳩の巣原理、グラフ彩色、Schur、N-Queens、数独、回路などの問題ファミリーを評価した。形式的に証明された対称性の除去により、ソルバーの探索量は最大で約2×10^7分の1にまで削減された。最大規模のケースでも、Lean側の認証は数分以内に完了した。ただし、これは一般的な性能保証ではなく、極端な削減率は特定の問題が持つ高度な対称性にも由来する。エンジニアリング上のより重要な進展は、Apache 2.0ライセンスのリポジトリに、50種類を超える制約、MiniZinc／SMT-LIBバックエンド、疑似ブール認証チェーン、再現可能な実験がすでに収録されていることだ。

現時点では、フレームワークのコミット数とユーザー数はまだ少なく、対応する制約や変換経路も、成熟したソルバーのエコシステムには遠く及ばない。今後は、大規模な産業用モデルにおける証明書のサイズ、SATケースでのwitness検査コスト、新しいバックエンドを追加する際に、ソルバー出力の最終段階だけを検証するのではなく、エンドツーエンドの定理を維持できるかどうかが注目点となる。