Lean Finder V2는 수학 라이브러리 Mathlib에서 정리를 찾는 의미 검색 프레임워크다. 연구진이 2026년 10월 22일 arXiv에 논문으로 공개했다. 모델 수준의 적대적 학습과 입력 수준의 질의 재작성을 함께 써서 사용자의 모호한 질의를 명확하게 만든다.
연구진은 MathlibQR 벤치마크에서 Lean Finder V2가 기존 최고 수준의 Mathlib 의미 검색 엔진보다 상대적으로 최소 11% 향상된 최고 성능을 냈다고 밝혔다. 이 검색기 위에 최적화한 질의 재작성을 더하면 MathlibQR 검색 결과가 한층 나아졌다고 한다. 사람과 코딩 에이전트의 상호작용에서 나온 정답 표시 없는 질의에서도 가장 강한 시스템으로 평가됐다고 했다.
짧은 질의가 문제인 이유
연구진에 따르면 수학자와 코딩 에이전트는 Mathlib을 검색할 때 자세한 맥락을 거의 적지 않는다. 짧은 성질, 표기법, 별칭, 가설만 입력하고 의도한 수학적 내용의 상당 부분을 암묵적으로 남겨 둔다. 기존 Mathlib 검색 엔진은 맥락이 풍부한 질의를 전제한다는 것이 연구진의 지적이다.
실제 짧은 질의와 정답 Mathlib 문장이 짝지어진 데이터가 드물어 모호성 해소가 어렵다. 연구진은 이를 본질적으로 데이터 문제로 보고, 적대적 학습으로 정답이 붙은 짧고 모호한 질의를 대량으로 만들었다. 이 데이터로 모델의 미세 조정 단계와 입력 단계의 질의 재작성에서 모호함을 푸는 방법을 학습시켰다.
Claude Code에 Lean Finder V2를 연결하면 정리 증명 과제의 증명 성공률이 올라간다고 연구진은 밝혔다.
출처
이 기사는 아래 자료를 바탕으로 정리했습니다. 제목을 누르면 원문이 새 창으로 열립니다.