본 논문은 Lean4 정리 증명을 위한 포괄적인 프레임워크인 MA-LoT(Model-CollAboration Lean-based Long Chain-of-Thought)를 제안합니다. MA-LoT는 전체 증명 생성과 증명 수정을 위한 오류 분석이라는 인지 과제를 모델 협업 방식으로 분리하여, LLM과 Lean4 검증기의 구조적 상호 작용을 Long CoT(Long Chain of Thought)를 통해 수행합니다. 특히, LLM에 Long CoT 사고 능력을 부여하기 위해 특별한 데이터 주석 없이도 가능한 새로운 LoT-Transfer Learning 학습-추론 파이프라인을 제안합니다. MiniF2F-Test 데이터셋(Lean4 버전)에서 61.07%의 정확도를 달성하여 기존의 DeepSeek-V3, InternLM-Step-Prover, Godel-Prover 등의 성능을 능가함을 실험적으로 보여줍니다.
시사점, 한계점
•
시사점:
◦
Long CoT와 형식적 검증의 결합을 통해 더욱 통찰력 있는 생성이 가능함을 보여줍니다.
◦
LLM과 형식적 검증 시스템의 협업을 통한 정리 증명 성능 향상 가능성을 제시합니다.
◦
특별한 데이터 주석 없이 Long CoT 능력을 LLM에 부여하는 새로운 학습-추론 파이프라인을 제시합니다.
◦
MiniF2F-Test 데이터셋에서 기존 최고 성능 모델들을 상당히 능가하는 성능을 달성했습니다.
•
한계점:
◦
MiniF2F-Test 데이터셋에 대한 성능 평가만 제시되어 다른 데이터셋에 대한 일반화 성능은 불확실합니다.
◦
제안된 프레임워크의 확장성 및 복잡한 정리 증명 문제에 대한 적용 가능성에 대한 추가적인 연구가 필요합니다.
◦
LoT-Transfer Learning 파이프라인의 상세한 구현 및 성능 분석이 부족합니다.
