Core Concepts
大規模言語モデルは数学的推論問題を解くことができるようになってきたが、その解答には論理的および計算上の誤りが含まれている。本研究では、モデルの訓練データに十分な数の形式数学の例が含まれていれば、モデルに自動的に非形式的な数学的記述を形式的な言語(Isabelle)に翻訳させることができ、その翻訳結果を自動定理証明システムで検証することで、正しい解答を識別できることを示す。
Abstract
本研究は、大規模言語モデル(LLM)の数学的推論能力の検証と改善を目的としている。LLMは近年、中学校レベルの数学ワードプロブレムから高校数学コンペティションレベルの問題まで、幅広い数量的推論問題を解くことができるようになってきた。しかし、LLMの生成する解答にはしばしば単純な計算ミスや正当化されていない論理的飛躍が含まれている。
本研究では、LLMの訓練データに十分な数の形式数学の例が含まれていれば、LLMに非形式的な数学的記述を形式的な言語(Isabelle)に自動的に翻訳させることができ、その翻訳結果を自動定理証明システムで検証することで、正しい解答を識別できることを示す。具体的には以下の手順を踏む:
非形式的な問題記述を形式的な定理に翻訳する。
非形式的な解答を形式的な証明スケッチに翻訳する。
自動定理証明システムを用いて、形式的な定理が形式的な証明スケッチによって証明できるかを検証する。
検証に成功した非形式的解答のみを集計し、最も多い解答を最終的な答えとする。
この手法を GSM8K、MATH、MultiArith の各データセットで評価した結果、従来の多数決ベースの手法に比べて12%以上の性能向上が得られることを示した。また、モデルサイズを変えた実験でも、一貫して提案手法の有効性が確認された。