AIが専門の計算ツールを自ら使って難解な論理問題を解く新手法が登場、プログラムも公開

学習して、人間のように文章を理解・生成できるAI。ChatGPTやGeminiの中身。">大規模言語モデルが専門の計算ツールである記号ソルバーと対話し、論理問題を解くための強化学習手法「SAT-RL」に関する論文が、2026年10月15日付でarXivに掲載された。関連するプログラムコードもGitHub上で公開されている。

大規模言語モデルは推論において高い性能を示す一方、制約条件の相互作用や探索空間が拡大すると問題に対処しにくくなる課題を抱えていた。一方、Z3に代表される充足可能性ソルバーは形式理論に基づく検証可能な推論が可能だが、自然言語で書かれた問題文を柔軟に解釈できない。SAT-RLは、言語モデルが複数回のやり取りを通じて記号ソルバーをツールとして実行できるよう訓練する仕組みである。

本手法は、検証可能な解を持つ合成データの生成、ソルバー利用履歴を用いた事前の教師あり学習、ツールの実行結果に応じた報酬を与える強化学習で構成される。実験の結果、訓練と同じ領域だけでなく異なる領域の論理タスクにおいても、ツールを用いた推論能力が大幅に向上したことが確認された。