技術要約：HERMES – LLMにおける効率的かつ検証可能な数学的推論に向けて

1. 問題提起

大規模言語モデル（LLM）は、Chain-of-Thought（CoT）のような非形式的な手法を通じて、数学的推論において顕著な能力を示してきた。しかし、純粋に非形式的な推論は、特に長い推論の連鎖において、論理的な飛躍、微細な誤り、あるいはハルシネーション（幻覚）に対して脆弱である。一方で、形式的な定理証明システム（Lean4やCoqなど）は、厳密で機械検証可能な推論を提供するが、自然言語による問題解決が持つ探索的な柔軟性や表現力に欠けることが多い。これら両者のギャップを埋めようとする現在の試み（PRMやORMなど）は、ステップごとの数学的正当性を明示的に検証することなく、数値的なスコアを割り当てるブラックボックス型の評価器に依存している。さらに、これらの報酬ベースの手法は、多大な人間のキュレーションを必要とし、評価に使用されるLLMの確率性やバイアスを継承してしまうことがあり、真のステップごとの正当性と乖離する可能性がある。

本研究が取り組む核心的な課題は、LLMベースの数学エージェントが、非形式的な推論の柔軟性と形式的な証明の検証可能性を、いかにして効率的かつ解釈可能な形で組み合わせるかという、原理的なメカニズムの欠如である。

2. 手法：Hermesフレームワーク

著者らは、非形式的な推論とLean4による形式検証済みの証明を交互に組み合わせるように設計された、マルチモジュール型のツール支援型エージェントであるHermes（Hybrid AgEnt for Reasoning in Mathematics with NEuro-Symbolic Lean4 verification）を導入する。このフレームワークは、以下の4つの主要モジュールを含む反復的な推論時プロセスを通じて動作する。

• Reasoning LLM（推論LLM）： 自然言語による推論ステップを生成する。このモデルは、最終的な証明に寄与するすべての重要な数学的ステップを検証するように指示される。
• Formalization Module（形式化モジュール）： 自然言語による証明ステップを、対応するLean4のステートメントへと翻訳する。意味的な忠実性を確保するため、このモジュールは2段階の検証プロセスを採用する。
  1. コンパイルチェック： 生成されたLeanコードが正常にコンパイルされること。
  2. バックトランスレーション（逆翻訳）： コンパイルされたLeanコードを自然言語に逆翻訳する。LLMは、元のステップとバックトランスレーションされたバージョンの等価性を評価する。
     このプロセスは、有効な形式化を保証するために予算 $K_f$ まで繰り返される。
• Prover Module（証明モジュール）： 検証されたLeanステートメントを受け取り、全証明生成モデル（例：Goedel-Prover-V2）と組み込みのLeanソルバーを用いて、目標またはその否定（$\neg \text{goal}$）の証明を試みる。このモジュールはサンプリング予算 $K_p$ の下で動作する。そして、CORRECT（証明発見）、INCORRECT（反証発見）、または VERIFICATION FAILURE（証明も反証も不能）のバイナリ信号を返す。
• Memory Block（メモリブロック）： 検証された証明ステップとそのベクトル表現を格納する構造化データベース。トップ-$k$ 検索メカニタズムを利用して、関連する以前に検証されたコンテキストを現在の推論ステップに注入し、連続性を確保して長い推論の連鎖におけるエラーの伝播を防ぐ。

フィードバックループ： 証明器の信号に基づき、LLMは現在の推論パスを継続するか（検証された場合）、ステップを修正するか（反証が見つかった場合）、あるいは代替のアプローチを探索する。システムはモジュール式に設計されており、オートフォーマライザやプルーバーといったコンポーネントを、それらが改善されるにつれて入れ替えることが可能である。

複雑性分析： 著者らは、トークンレベルの推論複雑性に関する理論的分析を提供している。彼らは、クリティカルなステップのサブセットに対して推論中に検証を挟み込むHermesの複雑性は $O(\tilde{T} K N^2)$ であり（ここで $\tilde{T}$ は検証されたステップ数）、これはPRMベースの手法の複雑性 $O(T K N^2)$ よりも理論的に低く、Best-of-N選択のために複数のフルトレースを生成するよりも大幅に効率的であると主張している。

3. 主な貢献

本論文は、以下の主要な貢献を主張している。

1. 初のツールベースのLean4エージェント： Hermesは、推論中に実行可能な中間証明ステップを検証し、学習された報酬モデルではなく、信頼できるコンパイラから導出されたカーネルベースの正当性信号をLLMに提供する、最初のツールベースのエージェントとして提示されている。
2. Lean4駆動のメモリ： 中間的な主張を蓄積・検証し、コンテキスト内に保持することで、ステップ間の整合性を確保し、長い推論の連鎖におけるエラーの伝播を抑制するメモリブロックの導入。
3. 精度と効率の向上： Hermesが、報酬ベースのアプローチと比較して、推論精度を向上させつつ、トークン使用量と計算コストを大幅に削減することを実証したこと。

4. 実験結果

本フレームワークは、4つの困難な数学的推論ベンチマーク（MATH-500, AIME'25, CollegeMath, HARDMath2）において、様々な規模のLLM（Qwen3-8B, OpenAI o3-mini, DeepSeek-V3.1/V3.2）を用いて評価された。

• 精度の向上： すべての設定において、HermesはゼロショットCoT、多数決（Majority Vote）、および各種報酬モデルのベースライン（ORMおよびPRM）を一貫して上回った。
  • 平均して、Hermesは4つのベンチマーク全体で精度を**23%**向上させた。
  • 難易度の高い AIME'25 データセットにおいて、Hermesはベースモデル（例：DeepSeek-V3.2）に対して40%の精度向上を達成しつつ、報酬ベースの手法と比較して80%少ない総推論FLOPsを使用した。
  • テスト時にスケールアップした場合（Best-of-N サンプリングを用いた Hermes@5）、精度はさらに20%向上した。
• 効率性： Hermesは、スコアベースの手法（Safe, ORM, PRM）よりも大幅に少ないトークンを利用した。報酬ベースの手法は、競争力のある精度を得るために5〜60個の推論トレースを生成する必要があることが多いが、Hermesは単一のトレース（@1）または最小限のサンプリングで優れた結果を達成し、トークン予算を4〜6倍削減した。
• アブレーション研究： Proverモジュールを取り除くと最大の性能低下（例：AIMEで相対的に25%の低下）が発生し、証明探索エンジンの必要性が浮き彫りになった。メモリバッファを取り除くと、特に推論の連鎖が長い困難なデータセットにおいて、推論の連続性が損なわれた。
• ドメイン感度： 精度向上は、容易なデータセット（MATH-500）よりも困難なデータセット（HARDMath2, AIME）でより顕著であり、Hermesが高度な推論におけるエラー修正に特に効果的であることを示唆している。システムは代数や方程式（Mathlibが密集している領域）で強いパフォーマンスを示したが、幾何学では現在の形式ライブラリの状態に起因して、わずかに低い利得となった。

5. 意義と主張

著者らは、Hermesを、非形式的な数学的推論と形式的な数学的推論を統合するための重要な一歩として位置づけている。形式的な検証を推論ループに直接統合することで、本フレームワークは以下を提供すると主張している。

• 解釈可能性： ブラックボックス型の報酬モデルとは異なり、Hermesはステップレベルの正当性のフィードバックを明示的に提供し、なぜ推論パスが妥当であるか、あるいは不備があるのかを明らかにする。
• スケーラビリティとモジュール性： 設計により、オートフォーマライザやプルーバーの改良版をシームレスに統合することができ、分野の進展に伴ってシステムが最新の状態を維持できる。
• リソース効率： 本研究は、高品質な数学的推論には、数千の候補トレースを生成することに関連する膨大な計算予算を必ずしも必要とせず、ターゲットを絞った検証可能な中間チェックが、より優れた効率と精度をもたらすことを示している。

結論として、Hermesは、LLMの柔軟性と形式的な定理証明の厳密さの間のギャップを効果的に埋める、スケーラブルで検証可能、かつ解釈可能な数学的推論エージェントへの移行を象徴するものである。