Research map / Large language models / Reasoning and chain of thought

HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs

ICML 2026 · Large language models › Reasoning and chain of thought · approach: Efficient and adaptive thinking · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Introduces HERMES, a tool-augmented agent that interleaves LLM informal reasoning with Lean4 formal verification (autoformalizer + prover + memory) to improve accuracy and token efficiency on math benchmarks.

Problem

Informal LLM mathematical reasoning suffers from logical gaps and hallucinated steps that are hard to detect, while reward-model best-of-N selection is token-expensive and relies on LLM-based judgment; formal provers are rigorous but inflexible.

Approach

A Lean4-driven agent where the reasoning LLM calls a verify tool on critical steps; the step is autoformalized (with back-formalization equivalence check), the goal and its negation are attempted by a prover, and the CORRECT/INCORRECT/FAILURE signal plus a retrieval memory of verified steps are fed back into the reasoning chain, yielding a single-trace method rather than sampling many candidates.

Key results

• Hermes@1 improves average accuracy over zero-shot CoT by 23.4% and over reward-based Best-of-5 methods by 5.7% to 14.9% across three reasoning models and four benchmarks.
• On AIME'25 with DeepSeek-V3.1, Hermes@1 reaches 66.7% versus 50.0% for CoT-level performance, with about 80% fewer FLOPs than reward-based methods as reported.
• Reasoning token budget of Hermes is comparable to zero-shot CoT and 4-6x lower than score-based methods such as Safe, ORMs and PRMs.

Surprising findings

• Reward-based Best-of-N can outperform Hermes on Qwen3-8B when given large token budgets (n>=20 exceeds 92% accuracy at roughly 28x tokens).
• Removing the prover module causes the largest accuracy drop on AIME (66.7% to 50.0%).

Limitations

• Formalization and proving success depend on Mathlib coverage; geometry and combinatorics steps often fail to be proven.
• Lean verification failures are common at small formalization budgets (translation failures exceed 60% at K_f=1).
• Evaluation uses a fixed 8,192-token budget and a limited set of benchmarks and base models.

Experimental setup

Datasets: MATH500 AIME'25 CollegeMath HARDMath2

Benchmarks: MATH500 AIME'25 CollegeMath HARDMath2

Metrics: accuracy reasoning tokens TeraFLOPs CoT coverage translation accuracy

Baselines: zero-shot CoT majority vote Skywork-Reward-Llama-3.1-8B ArmoRM-Llama3-8B math-shepherd-mistral-7b-prm RLHFlow PRM Safe Safe*

Builds on: Safe Goedel-Prover-V2 Goedel-Autoformalizer Lean4 REPL Chain-of-Thought

Closest papers by meaning

• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.92)
• Putnam-AXIOM: A Functional & Static Benchmark for Measuring Higher Level Mathematical Reasoning in LLMs (ICML 2025 · similarity 0.89)
• LeanAgent: Lifelong Learning for Formal Theorem Proving (ICLR 2025 · similarity 0.89)
• Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness (NeurIPS 2026 · similarity 0.89)
• UGMathBench: A Diverse and Dynamic Benchmark for Undergraduate-Level Mathematical Reasoning with Large Language Models (ICLR 2025 · similarity 0.89)
• One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs (ICML 2025 · similarity 0.89)