LongCat-Flash-Prover는 5600억 개 매개변수를 가진 오픈소스 Mixture-of-Experts (MoE) 모델로, Lean4 환경에서 원천 형식적 추론(Native Formal Reasoning)​을 크게 발전시켰습니다.

이 모델은 자동 형식화(auto-formalization)​, 스케치(sketching)​, 증명(proving)​의 세 가지 독립된 추론 능력으로 작업을 분해하고, 이를 지원하기 위해 Hybrid-Experts Iteration Framework를 도입하여 고품질 작업 경로를 확장합니다.

또한, 긴 작업 과정에서 안정적인 학습을 위해 계층적 중요도 샘플링 정책 최적화(Hierarchical Importance Sampling Policy Optimization, HisPO) 알고리즘과 그래디언트 마스킹(gradient masking) 기법을 활용하며, 정리 일관성(theorem consistency)​과 합법성 검출(legality detection) 메커니즘으로 보상 조작 문제를 방지합니다.

평가 결과, LongCat-Flash-Prover는 오픈 가중치 모델 중에서 자동 형식화와 정리 증명 분야에서 최첨단 성능을 기록하며, 적은 추론 예산으로도 높은 문제 해결률을 보여 실용적 가치를 입증하였습니다.