HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs

• AI News Team
• December 1, 2025

​Published on December 1, 2025 10:07 AM GMTIntegrating LLMs with Lean prover scaffolding.Summary provided by Xixidu:Hermes introduces an architecture where a language model is wrapped around an external, high-reliability verifier: the Lean4 proof assistant.Instead of just asking the AI “Does this look right?”, it translates key mathematical steps into Lean4 code and asks a proof engine “Can this be formally proved?” If the autoformalization is accurate and Lean finds a proof, this gives a strong mathematical guarantee for that formalized step.Steps:1. Reasoning (LLM): The model proposes the next logical step of a proof in natural language.2. Translation Module: An autoformalizer converts that step into a Lean4 statement. A back-translation check compares the Lean statement to the original text to ensure they match in meaning.3. Prover Module: A prover, working inside Lean4, attempts to prove the statement (or sometimes its negation). It returns a signal such as “proved”, “disproved” (negation proved), or “not decided / failed”.4. Feedback & Memory:- If the step is proved, it is stored in a Memory Block (a database of verified facts) and can be retrieved to support later reasoning.- If the step is disproved or cannot be justified, the LLM is informed of this outcome and is prompted to revise its reasoning rather than continuing from a shaky premise.In this way, Hermes interleaves informal LLM reasoning with formal Lean4 checking, using the proof assistant as an external source of ground truth for crucial steps.Discuss ​Read More