LongCat-Flash-Prover: 에이전트 도구 통합 강화학습을 통한 네이티브 형식 추론의 진보

자연어로 된 수학 문제를 컴퓨터가 이해하고 검증할 수 있는 형식 언어인 Lean4로 변환하고 증명하는 과정은 AI에게 매우 도전적인 과제이다. 이 논문은 거대 MoE 모델이 외부 도구와 직접 상호작용하며 스스로 학습하는 프레임워크를 통해 오픈소스 모델 중 세계 최고 수준의 수학적 추론 성능을 증명했다.

기존의 대형 언어 모델은 자연어 수학 문제는 잘 풀지만, 엄격한 논리적 검증이 필요한 Lean4와 같은 형식 언어 환경에서는 오답을 내거나 문법 오류를 범하기 쉽다. 이는 모델이 단순히 텍스트 패턴을 학습할 뿐, 실제 논리 엔진의 피드백을 실시간으로 반영하며 사고를 교정하는 능력이 부족하기 때문이다.

LongCat-Flash-Prover는 이를 해결하기 위해 모델을 하나의 '에이전트'로 설정하고, Lean4 컴파일러를 도구로 활용하게 한다. 모델이 증명 과정을 생성하면 컴파일러가 오류를 지적하고, 모델은 이 피드백을 바탕으로 자신의 논리를 수정한다. 이 과정에서 MoE(Mixture-of-Experts) 구조를 활용해 560B라는 거대 파라미터 중 필요한 전문가들만 활성화하여 효율적으로 복잡한 추론을 수행한다.

특히 학습 과정에서 발생하는 불안정성을 해결하기 위해 HisPO 알고리즘을 도입했다. 이는 강화학습의 중요도 샘플링(Importance Sampling) 과정에서 학습용 엔진과 실제 추론용 엔진 사이의 미세한 연산 차이가 오차를 증폭시키는 것을 막아준다. 결과적으로 모델은 더 긴 논리 전개 과정에서도 길을 잃지 않고 정답에 도달할 수 있는 안정적인 학습 궤적을 유지하게 된다.

전체 시스템은 세 가지 핵심 전문가(Auto-formalizer, Sketcher, Prover)로 구성된 하이브리드 전문가 반복 프레임워크를 기반으로 한다. 자연어 문제를 Lean4 문장으로 바꾸고, 증명의 뼈대를 잡은 뒤, 세부 보조 정리들을 증명하는 단계를 거친다. 각 단계에서 Lean4 Server와 상호작용하며 구문 오류(Syntax Error)와 의미론적 일관성(Semantic Consistency)을 검증받는다.

강화학습 단계에서는 HisPO(Hierarchical Importance Sampling Policy Optimization) 알고리즘을 사용한다. 중요도 샘플링 비율 r(θ)를 계산할 때, 학습-추론 엔진 간의 불일치인 r_dis(θ)와 정책 노후화인 r_stale(θ)를 곱한 형태로 분해한다. [입력 토큰 시퀀스 → 각 엔진의 확률값 계산 → 비율 산출 → 임계값 초과 시 그라디언트 마스크 적용] 순으로 연산하여 최적화 안정성을 확보한다.

리워드 해킹 방지를 위해 AST(Abstract Syntax Tree) 기반의 법적 탐지(Legality Detection)를 수행한다. Lean4 코드를 AST로 변환한 뒤, 원래 문제의 정의를 변조하거나 #exit 명령어로 검증을 우회하는 등의 9가지 부정 패턴을 탐지한다. [생성된 코드 입력 → Lexer/Parser를 통한 AST 변환 → 사전 정의된 부정 패턴 대조 → 위반 시 보상 박탈] 과정을 통해 순수한 논리 증명만을 장려한다.

MiniF2F-Test 벤치마크에서 단 72회의 추론 예산만으로 97.1%의 Pass Rate를 기록하며 오픈소스 모델 중 SOTA를 달성했다. 이는 기존 모델들이 1,000회 이상의 시도를 거쳐 도달했던 수치보다 월등히 높은 샘플 효율성을 보여준다.

고난도 수학 경시 대회 문제인 PutnamBench에서는 41.5%의 정확도를 기록했으며, ProverBench에서는 70.8%를 달성했다. 특히 MathOlympiad-Bench에서는 Pass@32 기준 기존 오픈소스 모델 대비 성능이 25.5% 향상되는 결과를 얻었다.

Ablation Study 결과, TIR(Tool-Integrated Reasoning) 전략을 적용했을 때 자동 형식화 성능이 최대 14% 향상되었으며, HisPO 알고리즘이 MoE 모델의 강화학습 수렴 속도와 안정성을 크게 개선했음이 확인됐다.

LongCat-Flash-Prover는 LongCat Mid-train Base 모델을 기반으로 하며, 총 560B 파라미터 중 약 27B 파라미터가 활성화되는 MoE 구조를 채택했다. 학습은 Cold-start SFT 단계와 Iteration RL 단계로 나뉘며, RL 단계에서는 Dynamic ORchestration for Asynchronous rollout (DORA) 시스템을 활용했다.

강화학습 알고리즘인 HisPO는 GRPO의 변형으로, 계층적 마스킹 행렬 H(θ)를 도입했다. 이는 시퀀스 레벨의 기하 평균 불일치와 토큰 레벨의 불일치를 모두 고려하여 불안정한 그라디언트 기여를 제거한다. 또한 Triplet Clipping Scheme을 적용하여 중요도 샘플링 비율의 분산을 제한함으로써 MoE 모델 특유의 학습 불안정성을 억제했다.

데이터 큐레이션 과정에서는 Curriculum Learning을 도입하여, 처음에는 도구 없이 단일 턴으로 생성하는 쉬운 작업부터 시작해 점차 도구 피드백을 포함한 다중 턴의 복잡한 증명 작업으로 학습 난이도를 높였다.

형식 추론 능력을 강화하는 과정에서 일반적인 자연어 추론 능력이 미세하게 하락하는 현상이 관찰되었다. 또한 매우 복잡하고 긴 증명 과정에서는 여전히 탐색 공간의 한계로 인해 정답을 찾지 못하는 경우가 존재한다.