ICML 2026論文：AIの数学をLeanで「証明チェック」しながら解くHERMES、推論の正しさを検証可能に

結論から言うと、AIに数学を解かせるとき、「言葉での考え」と「コンピュータで正しさを検証した証明」を交互に使うと、途中のまちがいを減らせる可能性があります。ICML 2026で発表されたポスター論文HERMES（ハーメス）は、そうした「検証しながら考えるAIエージェント」の仕組みを示しました。

ふつうの大規模言語モデル（LLM）は、もっともらしい文章を作るのが得意な一方で、数学の途中計算をまちがえても気づきにくい弱点があります。HERMESは、自由な言葉での推論（インフォーマルな考え）と、証明支援系「Lean」で形式的にチェックした証明（フォーマルな証明）を行き来させ、各ステップの正しさを確かめながら進みます。

さらに、長い証明でも筋道を見失わないよう、これまでの証明を覚えておく「メモリ（記憶）」のしくみを持ち、多段階の推論をつなげます。これにより、ただ答えらしいものを出すのではなく、「本当に正しいと検証できる数学の推論」へ近づけることをねらっています。私たちmanapickの読者に関係するのは、AIの「それっぽいけど間違い」を、外部の検証ツールで減らそうという研究の流れです。

将来、計算や論理が重要な分野で、AIの答えをより安心して使える方向につながります。ただし、これは研究段階で、すぐに製品へ入るとは限りません。専門用語のLeanは、数学の証明を機械的に検証するための言語・ツールです。