LEAP – LLM 위에 커스텀 에이전트 하네스를 얹어 수학 문제를 풀게 만든 시스템

구글이 발표한 **LEAP**은 기본 LLM에 **Agent Harness**와 **Lean 검증기**를 결합한다. 에이전트가 문제를 풀고, Lean으로 증명을 검증·수정하는 과정을 반복해 2025년 Putnam 수학 경시대회 문제 12개를 모두 해결했으며, Lean‑IMO‑Bench에서 정답률을 **10% → 70%**로 끌어올렸다. 핵심은 “모델 자체가 아니라, 어떻게 **반복·검증**하도록 설계하느냐”에 있다. 쉬운 설명: 큰 언어 모델에게 “문제 푸는 방법을 알려주는 로봇 손”을 달아, 풀고 틀리면 바로 고치는 작업을 시키는 것. 로봇 손이 계속 학습하면서 결국 모든 문제를 맞춘다. 관련분야: 자동수학 증명, 형식 검증, 에이전트 기반 AI, 대규모 언어 모델(LLM) 원문 보기 →