Technical Summary: HERMES – Towards Efficient and Verifiable Mathematical Reasoning in LLMs

1. Problem Statement

Large Language Models (LLMs) have demonstrated significant proficiency in mathematical reasoning through informal methods like Chain-of-Thought (CoT). However, purely informal reasoning is susceptible to logical gaps, subtle errors, and hallucinations, particularly in long reasoning chains. While formal theorem proving systems (e.g., Lean4, Coq) offer rigorous, machine-verifiable reasoning, they often lack the exploratory flexibility and expressiveness of natural language problem-solving. Current approaches attempting to bridge this gap, such as Process Reward Models (PRMs) and Outcome Reward Models (ORMs), rely on black-box evaluators that assign numerical scores without explicit verification of mathematical correctness. Furthermore, these reward-based methods often require substantial human curation and can inherit the stochasticity and biases of the LLMs used as evaluators, leading to misalignment with true stepwise correctness.

The core challenge addressed by this work is the lack of a principled mechanism for LLM-based math agents to combine the flexibility of informal reasoning with the verifiability of formal proofs, specifically in a way that is both efficient and interpretable.

2. Methodology: The Hermes Framework

The authors introduce Hermes (Hybrid AgEnt for Reasoning in Mathematics with NEuro-Symbolic Lean4 verification), a multi-modular, tool-assisted agent designed to interleave informal reasoning with formally verified proofs in Lean4. The framework operates through an iterative inference-time process involving four key modules:

• Reasoning LLM: Generates natural-language reasoning steps. The model is instructed to verify every critical mathematical step contributing to the final proof.
• Formalization Module: Translates the natural-language proof step into a corresponding Lean4 statement. To ensure semantic fidelity, this module employs a two-step verification process:
  1. Compilation Check: The generated Lean code must successfully compile.
  2. Back-Translation: The compiled Lean code is back-translated into natural language. The LLM evaluates the equivalence between the original step and the back-translated version.
     This process is repeated up to a budget $K_f$ to ensure a valid formalization.
• Prover Module: Receives the validated Lean statement and attempts to prove the goal or its negation ($\neg \text{goal}$) using a combination of a whole-proof generation model (e.g., Goedel-Prover-V2) and built-in Lean solvers. This module operates under a sampling budget $K_p$. It returns a binary signal: CORRECT (proof found), INCORRECT (counter-proof found), or VERIFICATION FAILURE (unable to prove or disprove).
• Memory Block: A structured database that stores validated proof steps alongside their vector representations. It utilizes a top-$k$ retrieval mechanism to inject relevant, previously verified context into the current reasoning step, ensuring continuity and preventing error propagation across long reasoning chains.

Feedback Loop: Based on the prover's signal, the LLM either proceeds with the current reasoning path (if verified), revises the step (if a counter-proof is found), or explores alternative approaches. The system is designed to be modular, allowing components like the autoformalizer or prover to be swapped as they improve.

Complexity Analysis: The authors provide a theoretical analysis of token-level inference complexity. They argue that Hermes, which interleaves verification during inference on a subset of critical steps, has a complexity of $O(\tilde{T} K N^2)$, where $\tilde{T}$ is the number of verified steps. This is theoretically bounded by the complexity of PRM-based methods ($O(T K N^2)$) and is significantly more efficient than generating multiple full traces for Best-of-N selection.

3. Key Contributions

The paper claims the following primary contributions:

1. First Tool-Based Lean4 Agent: Hermes is presented as the first tool-based agent that verifies feasible intermediate proof steps during inference, providing LLMs with kernel-based correctness signals derived from a trusted compiler rather than a learned reward model.
2. Lean4-Powered Memory: The introduction of a memory block that accumulates and validates intermediate claims in context, ensuring cross-step consistency and reducing error propagation in long reasoning chains.
3. Efficiency and Accuracy Gains: Empirical evidence demonstrating that Hermes improves reasoning accuracy while substantially reducing token usage and computational cost compared to reward-based approaches.

4. Experimental Results

The framework was evaluated on four challenging mathematical reasoning benchmarks: MATH-500, AIME'25, CollegeMath, and HARDMath2, using LLMs of varying scales (Qwen3-8B, OpenAI o3-mini, DeepSeek-V3.1/V3.2).

• Accuracy Improvements: Across all settings, Hermes consistently outperformed zero-shot CoT, Majority Vote, and various reward-model baselines (ORMs and PRMs).
  • On average, Hermes improved accuracy by 23% across the four benchmarks.
  • On the difficult AIME'25 dataset, Hermes achieved a 40% accuracy improvement over the base model (e.g., DeepSeek-V3.2) while using 80% fewer total inference FLOPs compared to reward-based methods.
  • When scaled at test time (Hermes@5 with Best-of-N sampling), accuracy improved further by an additional 20%.
• Efficiency: Hermes utilized significantly fewer tokens than score-based methods (Safe, ORMs, PRMs). While reward-based methods often required generating 5–60 reasoning traces to achieve competitive accuracy, Hermes achieved superior results with a single trace (@1) or minimal sampling, reducing token budgets by 4–6 times.
• Ablation Studies: Removing the Prover module caused the largest performance drop (e.g., a 25% relative drop on AIME), highlighting the necessity of the proof search engine. Removing the Memory buffer disrupted reasoning continuity, particularly on harder datasets with longer reasoning chains.
• Domain Sensitivity: Performance gains were most pronounced on harder datasets (HARDMath2, AIME) compared to easier ones (MATH-500), suggesting Hermes is particularly effective at correcting errors in advanced reasoning. The system showed strong performance in algebra and equations (where Mathlib is dense) and slightly lower gains in geometry, attributed to the current state of the formal library.

5. Significance and Claims

The authors position Hermes as a significant step toward unifying informal and formal mathematical reasoning. They claim that by integrating formal verification directly into the reasoning loop, the framework offers:

• Interpretability: Unlike black-box reward models, Hermes provides explicit, step-level correctness feedback, revealing why a reasoning path is valid or flawed.
• Scalability and Modularity: The design allows for seamless integration of improved autoformalizers and provers as the field advances, ensuring the system remains relevant beyond current Lean4 capabilities.
• Resource Efficiency: The work demonstrates that high-quality mathematical reasoning does not necessarily require massive computational budgets associated with generating thousands of candidate traces; instead, targeted, verifiable intermediate checks yield superior efficiency and accuracy.

The paper concludes that Hermes represents a move toward scalable, verifiable, and interpretable mathematical reasoning agents, effectively bridging the gap between the flexibility of LLMs and the rigor of formal theorem proving.