6×5ボード上の全駒
チェスのパズルで、6×5のボード上にキング、クイーン、そして2つのルーク、2つのナイト、2つのビショップ、8つのポーンという全駒を配置する問題を、大規模言語モデルClaudeを用いてZ3/Pythonのコードで解く方法を紹介する。以前の投稿ではPrologを使った解法を扱っていたが、今回はZ3ソルバーを用いたアプローチを試みている。
背景メモ
- ジョン・D・クック（John D. Cook）は応用数学者で、数値計算やプログラミングに関するブログを長年運営している。
- 本記事は「6×5のチェス盤上に全種類のチェスピース（キング、クイーン、ルーク×2、ビショップ×2、ナイト×2、ポーン×8）を、互いに利き筋が重ならないように配置するパズル」を扱う。
- Z3はMicrosoft Researchが開発したSAT/SMTソルバー。与えられた制約条件を満たす解を自動で探索できる定理証明器であり、パズルやハードウェア検証などに使われる。
- 筆者はClaude（AnthropicのLLM）にZ3/Pythonのコードを生成させてこのパズルを解かせた実験を紹介。以前の記事ではClaudeにPrologを、ChatGPTにPrologを生成させる同種の実験を行っている。
- この一連の投稿は、LLMが形式論理や制約プログラミングのコードをどの程度正確に生成できるかを検証する文脈の一部。