본 논문은 Lean4 정리 증명을 위한 다중 에이전트 기반 장기 사고 연쇄(Long Chain-of-Thought, LoT) 프레임워크인 MA-LoT를 제안합니다. 기존의 단일 LLM 기반 접근 방식과 달리, MA-LoT는 자연어(NL) 고차원 추론과 형식 언어(FL) 검증 피드백을 구조적으로 결합하여 장기적인 일관성을 유지하며 증명 생성을 수행합니다. LoT 전이 학습 파이프라인을 활용하여 장기 사고 연쇄에서 나타나는 형식적 추론 능력을 활용하며, MiniF2F-Test 데이터셋에서 기존의 GPT-4, 단일 에이전트 트리 탐색, 전체 증명 생성 방식보다 높은 54.51%의 정확도를 달성했습니다.
시사점, 한계점
•
시사점:
◦
다중 에이전트 접근 방식을 통해 자연어 추론과 형식 언어 검증의 효과적인 통합을 제시.
◦
장기 사고 연쇄(LoT)를 활용하여 증명 생성의 장기적 일관성 및 심층적 이해도 향상.
◦
기존 단일 에이전트 방식 대비 향상된 정확도를 실험적으로 검증 (54.51% vs. GPT-4 22.95%, InternLM-Step-Prover 50.70%, DeepSeek-Prover-v1.5 48.36%).
◦
형식 검증과 장기 사고 연쇄의 결합이 증명 생성에 대한 통찰력을 높일 수 있음을 시사.
•
한계점:
◦
제안된 MA-LoT 프레임워크의 일반화 성능 및 다양한 문제 유형에 대한 적용 가능성에 대한 추가적인 연구 필요.
