LongCat MoE, 공식 수학적 추론 분야 석권
- •5610억 개의 파라미터를 갖춘 LongCat-Flash-Prover MoE 모델이 오픈 웨이트 공식 수학적 추론 분야에서 신기록을 경신했다.
- •에이전트 기반의 도구 통합 강화학습과 Lean4를 활용하여 MiniF2F-Test에서 97.1%의 정확도를 달성했다.
- •새로운 HisPO 알고리즘을 도입하여 복잡하고 긴 호흡이 필요한 정리 증명 과제의 학습 안정성을 확보했다.
연구진은 Lean4 프로그래밍 언어를 활용해 수학적 증명을 마스터하도록 설계된 5,610억 매개변수 규모의 거대 모델, LongCat-Flash-Prover를 공개했다. 이 모델은 단순히 다음 단어를 예측하는 일반적인 AI와 달리, 도구를 능동적으로 사용하고 정리 증명 소프트웨어와 상호작용하며 자신의 논리를 단계별로 검증하는 '에이전트' 방식을 채택했다. 이러한 돌파구는 AI의 확장이 단순히 규모의 문제가 아니라, 모델이 구조화된 규칙과 상호작용하는 방식에 달려 있음을 시사한다.
해당 시스템은 복잡한 정리 증명 과정을 세 단계로 세분화하여 처리한다. 구체적으로는 인간의 언어를 수학 코드로 번역하고, 대략적인 개요를 작성한 뒤, 최종적으로 엄밀한 증명을 완성하는 방식이다. 특히 연구팀은 이토록 거대한 모델을 효율적으로 학습시키기 위해 '계층적 중요도 샘플링 정책 최적화(HisPO)' 알고리즘을 개발했다. 이 기술은 학습 과정에서 모델의 안정성을 유지하며, AI가 실제로 문제를 해결하지 않고 지름길만 찾아 보상을 가로채는 '해킹' 현상을 방지한다.
연구 결과는 매우 고무적이다. 이 모델은 MiniF2F-Test 벤치마크에서 97.1%의 성공률을 기록하며 오픈 웨이트 기술력의 비약적인 발전을 입증했다. 또한 난이도가 매우 높은 PutnamBench 문제의 41.5%를 해결함으로써, AI가 인간의 수학적 추론 능력과의 격차를 빠르게 좁히고 있음을 보여주었다. 해당 모델의 공개는 공식 검증 작업 중 가장 번거로운 부분을 자동화하고자 하는 학생과 연구자들에게 강력한 도구 세트를 제공할 것으로 기대된다.