CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization

자연어 수학 문장을 형식적이고 실행 가능한 코드로 번역하는 것은 자동 정리 증명에서 근본적인 도전 과제입니다. 이전 연구에서는 생성과 컴파일 성공에 초점을 맞추었지만, 생성된 형식화가 원래 문제의 의미적 의도를 진정으로 포착했는지 평가하는 비판 단계에는 거의 주목하지 않았습니다. 본 논문에서는 비판자의 역할을 수동 검증자에서 활동적인 학습 구성 요소로 격상시키는 새로운 비판자 지도 강화 학습 프레임워크인 CriticLean을 소개합니다. 구체적으로, 먼저 감독 학습 미세 조정과 강화 학습을 통해 Lean 4 형식화의 의미적 충실성을 엄밀하게 평가하도록 훈련된 CriticLeanGPT를 제안합니다. 그 다음, 모델이 의미적으로 올바른 형식화와 잘못된 형식화를 구분하는 능력을 측정하기 위해 설계된 CriticLeanBench 벤치마크를 소개하고, 우리 훈련된 CriticLeanGPT 모델이 강력한 오픈 소스 및 클로즈드 소스 기준모델을 크게 능가함을 보여줍니다. CriticLean 프레임워크를 바탕으로, 인간 평가에 따라 다양한 영역, 광범위한 난이도, 높은 정확성을 갖춘 285,000개 이상의 문제로 구성된 FineLeanCorpus 데이터셋을 구축했습니다. 전반적으로 우리의 연구 결과는 비판 단계 최적화가 신뢰할 수 있는 형식화를 생산하는 데 필수적임을 강조하며, 앞으로의 형식적 수학적 추론 발전에 유용한 통찰력을 제공하기를 바랍니다.