1. 문제 정의 (Problem)

최근 대규모 언어 모델 (LLM) 은 자연어 기반의 복잡한 추론 능력을 크게 향상시켰으나, 형식적 정리 증명 (Formal Theorem Proving) 과 같은 엄격한 논리적 검증이 필요한 작업에서는 여전히 한계를 보입니다.

• 형식 언어의 엄격성: Lean4 와 같은 형식 언어는 자연어와 달리 오류가 없어야 하며, 논리적 진행이 엄격하게 검증되어야 합니다.
• 기존 접근법의 한계: 기존 연구들은 주로 피드백을 통해 코드를 수정하는 방식에 집중했으나, Lean4 는 단순한 스크립트가 아니라 논리 자체를 표현하는 언어이므로, 기존 도구 통합 추론 (TIR) 을 직접 적용하기 어렵습니다.
• 핵심 과제: 모델이 특수한 아키텍처 변경 없이도 형식 연산자를 활용해 복잡한 추론 과제를 해결할 수 있는 네이티브 형식 추론 능력을 갖추는 것입니다.

2. 방법론 (Methodology)

LongCat-Flash-Prover 는 5600 억 파라미터 (약 270 억 활성 파라미터) 의 혼합 전문가 (Mixture-of-Experts, MoE) 모델로, 다음과 같은 세 가지 핵심 혁신을 통해 네이티브 형식 추론을 구현했습니다.

2.1. 네이티브 형식 추론의 3 단계 분해

형식 추론 작업을 세 가지 독립적인 능력으로 분해하여 전문화된 에이전트 (Expert) 로 처리합니다.

1. 자동 형식화 (Auto-Formalization): 자연어 문제를 검증된 Lean4 형식 명세로 변환.
2. 스케치 생성 (Sketching): 주어진 명세를 바탕으로 보조 정리 (Lemma) 를 포함한 전체 증명 구조 (Lemma-style sketch) 를 생성.
3. 증명 (Proving): 전체 증명 (Whole-proof) 을 생성하거나, 스케치를 기반으로 보조 정리를 증명하여 최종 정리를 완성.

2.2. 하이브리드 전문가 반복 프레임워크 (Hybrid-Experts Iteration Framework)

고품질의 학습 데이터 (Trajectories) 를 생성하기 위한 프레임워크입니다.

• 전문가 모델: 자동 형식화, 스케치, 증명에 특화된 세 가지 전문가 모델을 순차적으로 최적화합니다.
• 도구 통합 합성 (Tool-Integration Synthesis): Lean4 컴파일러 및 검증 도구를 사용하여 생성된 명세와 증명의 문법적 정확성 (Syntax) 및 의미적 일관성 (Semantic Consistency) 을 검증합니다.
• 커리큘럼 학습: 단순한 1 회 상호작용 (Single-turn) 에서 시작하여 도구 피드백이 필요한 다중 턴 (Multi-turn) 작업으로 점진적으로 난이도를 높이며 데이터를 합성합니다.

2.3. 계층적 중요도 샘플링 정책 최적화 (HisPO)

MoE 모델의 장기간 작업 (Long-horizon tasks) 학습 안정성을 보장하기 위해 제안된 새로운 강화학습 (RL) 알고리즘입니다.

• 문제점: 비동기 학습 환경에서 훈련 엔진과 추론 엔진 간의 불일치 (Train-Inference Discrepancy) 및 정책의 노후화 (Staleness) 로 인해 중요도 샘플링 (Importance Sampling) 비율 계산이 불안정해집니다.
• 해결책:
  • 계층적 그라디언트 마스킹: 시퀀스 수준과 토큰 수준에서 훈련 - 추론 불일치가 큰 경우 그라디언트 기여도를 차단합니다.
  • 불법성 탐지 (Legality Detection): 모델이 Lean4 서버를 속이거나 정의된 정리 조건을 위반하는 '해킹 (Reward Hacking)' 증명을 생성하는 것을 방지하기 위해 AST(추상 구문 트리) 기반의 엄격한 일관성 검사를 수행합니다.

3. 주요 기여 (Key Contributions)

1. 네이티브 형식 추론 패러다임 제시: 모델이 별도의 구조 변경 없이도 형식 언어 연산자를 활용해 추론할 수 있는 능력을 정립했습니다.
2. 고품질 데이터 합성 프레임워크: 검증 도구를 활용한 반복적인 전문가 모델 최적화를 통해 고품질의 형식 추론 데이터 (Trajectories) 를 대량으로 생성했습니다.
3. MoE 기반 안정적 강화학습: HisPO 알고리즘을 통해 긴 시퀀스 작업에서의 MoE 모델 학습 불안정성을 해결하고, 보상 해킹을 방지하는 메커니즘을 도입했습니다.
4. 오픈소스 SOTA 달성: 자동 형식화 및 정리 증명 분야에서 기존 오픈소스 및 상용 모델을 능가하는 성능을 달성했습니다.

4. 실험 결과 (Results)

다양한 벤치마크에서 LongCat-Flash-Prover 는 기존 모델들을 압도하는 성능을 보였습니다.

• 자동 형식화 (Auto-Formalization):

  • MiniF2F-Test: 99.2% (TIR 사용 시 100%), ProofNet: 87.1% (TIR 사용 시 97.9%) 등 모든 벤치마크에서 SOTA 기록.
  • TIR 전략을 통해 최대 14% 의 성능 향상을 달성했습니다.

• 정리 증명 (Theorem Proving):

  • MiniF2F-Test: 72 번의 시도 (Inference Budget) 만으로 97.1% 통과율을 기록 (기존 오픈소스 모델들은 1024 번 이상의 시도가 필요하거나 더 낮은 성능).
  • PutnamBench: 220 번 시도 내 41.5% 통과율 (기존 오픈소스 모델 대비 현저히 높은 성능).
  • MathOlympiad-Bench: Pass@32 기준 35.8% (TIR 사용 시) 로 기존 모델 대비 25.5% 향상.

• 일반 추론 능력 유지:

  • 형식 추론 학습으로 인해 일반 추론 (수학, 코딩, 논리 등) 능력이 일부 감소했으나, LongCat-Flash-Thinking-2601 과 비교해 수용 가능한 수준을 유지했습니다.

• 샘플 효율성:

  • 제한된 추론 예산 (Inference Budget) 으로도 높은 정확도를 달성하여 계산 자원의 효율성이 매우 뛰어남을 입증했습니다.

5. 의의 및 결론 (Significance)

LongCat-Flash-Prover 는 오픈소스 커뮤니티에서 형식적 추론 (Formal Reasoning) 과 일반적 추론 (Informal Reasoning) 을 통합한 새로운 기준을 제시했습니다.

• 과학적 진보: Lean4 와 같은 형식 도구를 활용한 자동 증명 기술의 한계를 확장하여, 복잡한 수학 문제 해결 및 소프트웨어 검증 분야에서 AI 의 활용 가능성을 크게 높였습니다.
• 기술적 혁신: MoE 아키텍처와 강화학습의 결합, 그리고 도구 통합 추론 (TIR) 을 통한 안정적 학습 방법론은 향후 대규모 언어 모델의 에이전트 능력 개발에 중요한 통찰을 제공합니다.
• 오픈소스 생태계 기여: 고품질의 오픈소스 모델과 데이터 전략을 공개함으로써, 연구자들이 형식 추론 분야에서 더 빠른 발전을 이룰 수 있는 기반을 마련했습니다.

이 모델은 AI 가 복잡한 논리적 문제를 해결하는 데 있어 형식 언어의 엄격함과 자연어의 유연성을 동시에 활용할 수 있는 가능성을 보여주었습니다.