# HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs

arXiv: https://arxiv.org/abs/2511.18760 · HTML: https://mlsanity.com/paper/2511.18760/

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 23 of its 58 references that are in the map.
- First posted on arXiv 24 Nov 2025.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 23 of 23)

- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [Scaling Laws for Neural Language Models](https://mlsanity.com/paper/2001.08361/) (2020)
- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [ToolLLM: Facilitating Large Language Models to Master 16000+ Real-world APIs](https://mlsanity.com/paper/2307.16789/) (2023)
- [Qwen3 Embedding: Advancing Text Embedding and Reranking Through Foundation Models](https://mlsanity.com/paper/2506.05176/) (2025)
- [DeepSeek-V3 Technical Report](https://mlsanity.com/paper/2412.19437/) (2024)
- [MetaMath: Bootstrap Your Own Mathematical Questions for Large Language Models](https://mlsanity.com/paper/2309.12284/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Skywork-Reward: Bag of Tricks for Reward Modeling in LLMs](https://mlsanity.com/paper/2410.18451/) (2024)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [RLHF Workflow: From Reward Modeling to Online RLHF](https://mlsanity.com/paper/2405.07863/) (2024)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [Winning Gold at IMO 2025 with a Model-Agnostic Verification-and-Refinement Pipeline](https://mlsanity.com/paper/2507.15855/) (2025)
- [R-PRM: Reasoning-Driven Process Reward Modeling](https://mlsanity.com/paper/2503.21295/) (2025)
- [Efficient Tool Use with Chain-of-Abstraction Reasoning](https://mlsanity.com/paper/2401.17464/) (2024)
- [Can LLMs Solve longer Math Word Problems Better?](https://mlsanity.com/paper/2405.14804/) (2024)
- [Mathesis: Towards Formal Theorem Proving from Natural Languages](https://mlsanity.com/paper/2506.07047/) (2025)
- [WTU-EVAL: A Whether-or-Not Tool Usage Evaluation Benchmark for Large Language Models](https://mlsanity.com/paper/2407.12823/) (2024)

## Built on by (most cited first, 11 of 11)

- [From Chatbot to Digital Colleague: The Paradigm Shift Toward Persistent Autonomous AI](https://mlsanity.com/paper/2606.14502/) (2026)
- [Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification](https://mlsanity.com/paper/2601.22642/) (2026)
- [Where to Spend Rollouts: Hit-Utility Optimal Rollout Allocation for Group-Based RLVR](https://mlsanity.com/paper/2605.07114/) (2026)
- [FormalJudge: A Neuro-Symbolic Paradigm for Agentic Oversight](https://mlsanity.com/paper/2602.11136/) (2026)
- [The Neurosymbolic Frontier of Nonuniform Ellipticity: Formalizing Sharp Schauder Theory via Topos-Theoretic Reasoning Models](https://mlsanity.com/paper/2602.10632/) (2026)
- [Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge](https://mlsanity.com/paper/2606.11430/) (2026)
- [Formalize Once, Edit the Rest: Efficient Lean-Based Answer Selection for Math Reasoning](https://mlsanity.com/paper/2606.15972/) (2026)
- [Case study: proving sqrt(2) irrational with LPTP and an LLM](https://mlsanity.com/paper/2607.21187/) (2026)
- [PaperDoctor: Evidence-Grounded and Actionable Feedback for Scientific Papers in Progress](https://mlsanity.com/paper/2609.16995/) (2026)
- [When Does Structured Knowledge Help Neural Theorem Proving?](https://mlsanity.com/paper/2609.34460/) (2026)
- [LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification](https://mlsanity.com/paper/2610.17697/) (2026)

## Abstract (arXiv)

Informal mathematics has been central to modern large language model (LLM) reasoning, offering flexibility and 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, 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 proofs in Lean. The framework performs intermediate formal checking to prevent reasoning drift and a memory module for proof continuity across multi-step reasoning chains, enabling both exploration and verification. 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 reasoning token usage and computational cost compared to reward-based approaches. On difficult datasets such as AIME and HARDMath2, Hermes@1 achieves up to a 40% accuracy improvement while using 80% fewer total inference FLOPs. When scaled at test time, Hermes@5 boosts accuracy further by 20%. The implementation and codebase are publicly available at https://github.com/aziksh-ospanov/HERMES.