論文の概要: HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs

• arxiv url: http://arxiv.org/abs/2511.18760v1
• Date: Mon, 24 Nov 2025 04:50:18 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-25 18:34:25.019406
• Title: HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs
• Title（参考訳）: HERMES:LLMにおける効率的かつ検証可能な数学的推論を目指して
• Authors: Azim Ospanov, Zijin Feng, Jiacheng Sun, Haoli Bai, Xin Shen, Farzan Farnia,
• Abstract要約: Hermesはツール支援エージェントで、リーンシステムにおける検証段階と非公式な推論をインターリーブする。 パラメータスケールの異なる LLM を用いて,Hermes を4つの挑戦的数学的推論ベンチマークで評価する。
• 参考スコア（独自算出の注目度）: 32.234133057592935
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Informal mathematics has been central to modern large language model (LLM) reasoning, offering flexibility and enabling efficient construction of arguments. However, purely informal reasoning is prone to logical gaps and subtle errors that are difficult to detect and correct. In contrast, formal theorem proving provides rigorous, verifiable mathematical reasoning, where each inference step is checked by a trusted compiler in systems such as Lean, but lacks the exploratory freedom of informal problem solving. This mismatch leaves current LLM-based math agents without a principled way to combine the strengths of both paradigms. In this work, we introduce Hermes, the first tool-assisted agent that explicitly interleaves informal reasoning with formally verified proof steps in Lean. The framework performs intermediate formal checking to prevent reasoning drift and employs a memory module that maintains proof continuity across long, multi-step reasoning chains, enabling both exploration and verification within a single workflow. We evaluate Hermes on four challenging mathematical reasoning benchmarks using LLMs of varying parameter scales, from small models to state-of-the-art systems. Across all settings, Hermes reliably improves the reasoning accuracy of base models while substantially reducing token usage and computational cost compared to reward-based approaches. On difficult datasets such as AIME'25, Hermes achieves up to a 67% accuracy improvement while using 80% fewer total inference FLOPs. The implementation and codebase are publicly available at https://github.com/aziksh-ospanov/HERMES.
• Abstract（参考訳）: インフォーマル数学は現代の大言語モデル(LLM)の推論の中心であり、柔軟性を提供し、議論の効率的な構築を可能にしている。 しかし、純粋に非公式な推論は、検出と修正が難しい論理的ギャップと微妙な誤りを引き起こす。 対照的に、形式的定理証明は厳密で検証可能な数学的推論を提供し、それぞれの推論ステップはリーンのようなシステムにおいて信頼できるコンパイラによってチェックされるが、非公式な問題解決の探索的自由は欠いている。 このミスマッチは、両方のパラダイムの強みを結合する原則的な方法のない、現在のLLMベースの数学エージェントを残します。 本研究では,リーンにおける非公式な推論と,正式に証明された証明ステップとを明示的にインターリーブする,最初のツール支援エージェントであるHermesを紹介します。 このフレームワークは、推論のドリフトを防ぐために中間的な形式的なチェックを実行し、長い複数のステップの推論チェーンにわたる証明連続性を維持するメモリモジュールを使用し、単一のワークフロー内での探索と検証を可能にする。 我々は,小モデルから最先端システムまで,パラメータスケールの異なる LLM を用いた4つの挑戦的数学的推論ベンチマークを用いて,Hermes の評価を行った。 すべての設定において、Hermesは、報酬ベースのアプローチと比較してトークンの使用量と計算コストを大幅に削減しながら、ベースモデルの推論精度を確実に改善する。 AIME'25のような難しいデータセットでは、Hermesは最大67%の精度向上を実現し、全体の予測FLOPを80%削減した。 実装とコードベースはhttps://github.com/aziksh-ospanov/HERMESで公開されている。

関連論文リスト

• Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
  現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。 本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-10-29T15:30:31Z)
• Solving Inequality Proofs with Large Language Models [42.667163027148916]
  不等式証明は様々な科学・数学分野において不可欠である。 これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。 我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
  論文  参考訳（メタデータ） (2025-06-09T16:43:38Z)
• Automated Theorem Provers Help Improve Large Language Model Reasoning [0.18416014644193066]
  ニューロシンボリック・アーキテクチャーによっていかに精度が向上できるかを示す。 構文的および意味的エラーカテゴリのフレームワークを定義する。 我々は,構文的および意味的誤りを自動的に修正する機能を備えた手法を拡張した。
  論文  参考訳（メタデータ） (2024-08-07T01:03:56Z)
• Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization [45.439933713342256]
  大規模言語モデル(LLM)は、数学的な量的推論問題を解く能力がますます高まっている。 LLMのトレーニングコーパスが十分に多くの形式数学の例を含むなら、それらが形式的イザベル符号に翻訳するように促すことができるという事実を活用する。 これは、形式化されたバージョンが内部や形式化された問題ステートメントと矛盾するソリューションを自動的に拒否するメカニズムを提供する。
  論文  参考訳（メタデータ） (2024-03-26T22:01:13Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  LLMの複雑な推論には2行のアプローチが採用されている。 1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。 他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。 具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
  論文  参考訳（メタデータ） (2023-11-16T11:26:21Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。