논문 요약: Lean4 자동 형식화 개선을 위한 순환 일관성 미세 조정 (Cycle Consistency Fine-tuning)

이 논문은 자연어 수학적 텍스트를 Lean4 같은 형식 증명 언어로 자동 변환하는 자동 형식화 (Autoformalization) 작업의 성능을 향상시키기 위해 제안된 새로운 훈련 방법론을 다룹니다. 저자는 Qwen3.5-2B 모델을 기반으로 LoRA (Low-Rank Adaptation) 를 적용하고, 순환 일관성 (Cycle Consistency) 을 보상 신호로 활용한 강화 학습 (Reinforcement Learning, RL) 기법을 도입하여 기존 지도 학습 (SFT) 의 한계를 극복했습니다.

---

1. 문제 정의 (Problem)

• 배경: Lean4 와 같은 형식 증명 도구는 수학 명제와 증명을 컴파일 가능한 코드로 변환하여 검증할 수 있게 합니다. 그러나 자연어 (NL) 를 형식 언어 (Lean4) 로 변환하는 과정은 여전히 어렵습니다.
• 핵심 과제: 대규모 언어 모델 (LLM) 은 문법적으로 타당하지만 의미적으로 잘못된 Lean4 코드를 생성하는 경향이 있습니다. 즉, 코드는 컴파일되지만 원래 수학 문제의 의도를 제대로 반영하지 못합니다.
• 목표: 자연어에서 Lean4 로의 변환 시, 생성된 코드가 원래 수학 의미와 얼마나 일치하는지 (Semantic Fidelity) 를 보장하는 모델을 개발하는 것입니다.

2. 방법론 (Methodology)

A. 모델 아키텍처 및 데이터

• Base Model: Qwen3.5-2B 모델을 사용하며, LoRA를 적용하여 파라미터 효율성을 높였습니다 (전체 2B 파라미터 중 약 940 만 개만 학습).
• 데이터셋:
  • FineLeanCorpus (FLC): 509,000 개의 자연어/Lean4 쌍 데이터 (난이도 1~10 등급).
  • PutnamBench: 660 개의 고난도 수학 경시대회 문제 (평가용 홀드아웃 데이터).
  • 데이터 전처리: 중복 제거, 컴파일 오류 제거, PutnamBench 와의 유사도 기반 데이터 오염 (Decontamination) 제거.

B. 훈련 파이프라인 (3 단계 접근)

저자는 세 가지 훈련 전략을 비교 분석했습니다:

1. 지도 미세 조정 (SFT) - 커리큘럼 학습: 난이도 1 에서 10 까지 순차적으로 학습.
2. 지도 미세 조정 (SFT) - 무작위 학습: 난이도 순서와 상관없이 섞인 데이터로 학습.
3. 강화 학습 (RL) - GRPO 기반:
   • 알고리즘: Group Relative Policy Optimization (GRPO) 사용.
   • 보상 함수 (Reward): 순환 일관성 (Cycle Consistency) 을 핵심 지표로 사용.
     • 과정: 자연어 ($s$) $\rightarrow$ Lean4 ($\hat{l}$) $\rightarrow$ 자연어 ($s'$, 역변환).
     • 계산: $s$와 $s'$의 문장 임베딩 (Sentence Embedding, all-MiniLM-L6-v2) 코사인 유사도를 보상으로 부여.
     • 목적: 역변환된 자연어가 원문과 의미적으로 유사할 때 높은 보상을 받도록 유도.

C. 평가 지표

• 주요 지표: 평균 순환 일관성 점수 ($\bar{C}$).
• 부수적 지표: 크로스 엔트로피 손실 (Cross-Entropy Loss) 을 통해 언어 모델링 능력의 저하 여부를 확인.

3. 주요 기여 (Key Contributions)

1. LoRA 기반 Lean4 자동 형식화 파이프라인 구축: Qwen3.5-2B 를 FineLeanCorpus 로 미세 조정하고 PutnamBench 데이터 오염을 제거한 체계적인 파이프라인을 제시.
2. 커리큘럼 학습의 무효성 입증: 제한된 모델 규모 (2B) 와 데이터셋에서 난이도 순서대로 학습하는 것이 무작위 학습보다 유의미한 이점을 주지 않음을 실험적으로 증명.
3. 순환 일관성 기반 RL 의 효과 입증: GRPO 를 사용하여 순환 일관성을 보상 신호로 활용했을 때, 기존 SFT 대비 형식화 품질이 크게 향상됨을 보임.

4. 실험 결과 (Results)

A. 성능 비교 (Table 1 및 Figure 2)

• FLC 홀드아웃 데이터:
  • SFT (커리큘럼): 0.513
  • RL (GRPO): 0.669 (SFT 대비 0.156 향상, 통계적 유의성 $p < 10^{-65}$)
• PutnamBench (고난도):
  • SFT (커리큘럼): 0.422
  • RL (GRPO): 0.561 (SFT 대비 0.139 향상, 통계적 유의성 $p < 10^{-56}$)
• 크로스 엔트로피 손실: RL 모델은 SFT 대비 손실이 0.011 nats 만 증가하여 언어 모델링 능력이 크게 저하되지 않음을 확인.

B. 추가 분석

• 난이도별 성능: RL 은 난이도가 낮을수록 더 큰 개선을 보였으나, 난이도가 높아질수록 (7 단계) 개선 폭은 감소함. 이는 고난도 문제에서 역변환 모델이 Lean4 코드를 해석하기 어려워 보상 신호가 노이즈가 되기 때문으로 분석됨.
• 수학 도메인별 성능: 대수학, 정수론 등 이산적 도메인에서 연속적 도메인 (미적분, 해석학) 보다 순환 일관성 점수가 높게 나옴. 이는 Lean4 라이브러리의 구조적 복잡성 차이 때문으로 추정됨.
• 모델 규모 비교: 9B 모델의 SFT 성능은 2B 모델의 SFT 보다 좋지만, 2B 모델의 RL 성능이 9B 모델의 SFT 성능을 능가함 (FLC 기준). 이는 RL 신호가 모델 규모 확장만큼이나 효과적임을 시사.

5. 의의 및 한계 (Significance & Limitations)

의의

• 비용 효율성: 별도의 크리틱 (Critic) 모델 없이 임베딩 기반의 부드러운 보상 (Soft Reward) 만으로 RL 을 성공적으로 수행하여 컴파일러 실행 지연 시간을 줄임.
• 의미 보존: 문법적 정확성뿐만 아니라 수학적 의미의 보존을 직접적으로 최적화하는 새로운 접근법을 제시.
• 확장성: RL 기법이 모델 규모를 늘리는 것보다 더 큰 성능 향상을 가져올 수 있음을 보여줌.

한계 및 미래 과제

• 보상 해킹 (Reward Hacking): 역변환 모델이 생성된 Lean4 코드를 원문과 유사하게 단순히 복사해내는 경우, 실제 형식화 품질이 낮아도 높은 보상을 받는 "보상 해킹" 현상이 발생 가능.
• 의미적 정확성 부재: sorry (증명 생략) 를 사용하는 현재 설정에서는 코드가 컴파일되더라도 수학적으로 올바른지 검증되지 않음.
• 향후 방향: Lean4 컴파일러 피드백을 하드 보상 (Hard Reward) 으로 결합하거나, 더 강력한 의미 등가성 검증 도구를 도입할 필요성 제기.

결론

이 연구는 순환 일관성 (Cycle Consistency) 을 강화 학습의 보상 신호로 활용함으로써, Lean4 자동 형식화 분야에서 기존 지도 학습 (SFT) 의 한계를 극복하고 의미적 정확성을 크게 향상시켰음을 입증했습니다. 특히 소규모 모델 (2B) 에서도 RL 기법을 통해 대규모 모델 (9B) 의 SFT 성능을 능가할 수 있음을 보여주어, 효율적인 수학 AI 연구에 중요한 통찰을 제공합니다.