HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs

Motivation

• Known: LLM 기반 수학 추론은 Chain-of-Thought를 통해 상당한 발전을 이루었으나 여전히 논리적 비약과 오류에 취약하며, 이를 보완하기 위해 PRM/ORM 같은 reward 기반 방법이나 Lean4/Coq/Isabelle 같은 formal theorem proving 시스템(AlphaProof, AlphaGeometry 등)이 각각 발전해왔다.
• Gap: PRM/ORM은 블랙박스 평가자로서 해석 가능성이 낮고 학습에 많은 human curation과 noisy label이 필요하며, formal theorem proving은 엄밀하지만 informal reasoning의 탐색적 유연성이 부족하여, 두 패러다임의 강점을 원칙적으로 결합하는 방법이 부재했다.
• Why: informal reasoning의 유연성과 formal verification의 엄밀성을 결합하면 LLM 추론의 정확성과 해석 가능성을 동시에 높이면서도 reward model 학습에 드는 비용과 토큰 사용량을 줄일 수 있어, 신뢰할 수 있고 효율적인 수학 문제 해결 agent 구축에 중요하다.
• Approach: Hermes는 LLM이 생성한 중간 추론 단계를 Lean 코드로 formalize하고, back-formalization으로 일관성을 검증한 뒤 prover module로 증명/반증을 시도하며, 그 결과를 feedback으로 LLM에 되돌려주는 4개 모듈(reasoning LLM, formalizer, prover, feedback)로 구성된 multi-modular tool-augmented agent이다.

Achievement

1. 정확도 개선: 네 개의 어려운 수학 벤치마크(MATH500, AIME'25, CollegeMath, HardMath2 등)에서 다양한 파라미터 규모의 LLM에 대해 평균 23%의 정확도 향상을 달성했다.
2. 연산 효율성: AIME'25와 HARDMath2 같은 어려운 데이터셋에서 Hermes@1이 최대 40%의 정확도 향상을 이루면서도 총 inference FLOPs를 80% 절감했다.
3. test-time scaling: Hermes@5로 Best-of-N sampling과 결합 시 정확도를 추가로 20% 향상시켜 확장성을 입증했다.
4. 최초의 Lean4 기반 tool agent: intermediate formal checking과 Lean4 기반 memory block을 갖춘 최초의 tool-based reasoning agent를 제시하여 kernel 기반 정확성 신호를 LLM 추론에 제공한다.

How

• Formalization Module: LLM이 생성한 candidate reasoning step을 자연어에서 Lean4 goal 문장으로 formalize
• back-formalization을 통한 검증: formalize된 Lean 문장을 다시 자연어로 역변환하여 원래 의미와의 일치 여부를 확인함으로써 formalization의 정확성 보장
• Prover Module: 공식화된 goal에 대해 Lean 컴파일러 기반 prover가 증명 또는 반증을 시도하여 kernel 수준의 검증 신호 생성
• Feedback Module: 검증 결과를 다시 reasoning LLM에 전달하여 다음 단계 추론에 반영, reasoning drift를 방지
• Memory Module: 여러 단계에 걸쳐 검증된 중간 claim들을 누적·유지함으로써 multi-step reasoning chain에서 proof continuity를 확보
• 다양한 크기의 LLM(소형 모델부터 SOTA 모델까지)에 프레임워크를 적용해 네 개 벤치마크에서 Hermes@1, Hermes@5(Best-of-N) 성능 및 FLOPs 비교 평가

Originality

• informal LLM reasoning과 Lean4 formal verification을 추론 과정 중간에 명시적으로 interleave하는 최초의 tool-assisted agent를 제안
• 기존 PRM/ORM처럼 블랙박스 스칼라 점수를 주는 대신, Lean 컴파일러의 kernel 기반 검증 신호를 직접 활용해 해석 가능한 step-level correctness feedback을 제공
• back-formalization을 통한 formalization consistency 검증과 Lean4 기반 memory block을 결합해 multi-step reasoning에서의 오류 전파를 억제하는 새로운 설계
• 기존 autoformalization/automatic theorem proving/PRM·ORM 연구들을 하나의 통합된 에이전트 프레임워크로 결합한 최초의 시도

Limitation & Further Study

• 리뷰 발췌 내용에는 formalizer/prover 모듈이 실패하거나 Lean으로 formalize하기 어려운 복잡한 자연어 진술(비형식적이거나 애매한 수학적 주장)에 대한 한계 논의가 명확히 제시되지 않아, formalization 실패율이나 커버리지에 대한 정량적 분석이 필요해 보인다.
• Lean4 prover와 formalizer 자체의 성능에 크게 의존하는 구조이므로, 이들 모듈의 오류나 한계가 전체 agent 성능에 어떻게 영향을 미치는지에 대한 민감도 분석이 추가로 필요하다.
• 네 개 벤치마크에 한정된 평가로, 기하학/조합론 등 Lean으로 formalize하기 어려운 다른 수학 분야로의 일반화 가능성은 추가 검증이 필요하다.
• FLOPs 절감이 강조되지만 Lean compiler 호출에 따른 실제 wall-clock latency나 시스템 복잡도(엔지니어링 오버헤드) 비교는 상대적으로 부족해 보인다.

Evaluation

총평: informal reasoning과 formal verification을 실질적으로 결합한 참신하고 실용적인 agent 설계로, 정확도와 효율성 양 측면에서 인상적인 실험 결과를 보이지만 formalization 실패 사례나 다양한 수학 영역으로의 일반화에 대한 추가 분석이 보완되면 더욱 완성도가 높아질 것이다.