린에이전트(LeanAgent) 평생학습 정리 증명: 커리큘럼과 전제 검색으로 155개 새 증명을 만든 방법

핵심 메시지

• 새로운 것을 배우면 이전 것을 잊는 문제는 AI의 오랜 난제이며, 모델이 지나치게 고정되면 아무것도 배우지 못하고 지나치게 유연하면 앞서 배운 것을 잃는다는 양극단 사이의 균형이 핵심이다.
• 연구팀은 대수를 배워야 미적분과 해석학으로 갈 수 있는 수학의 누적적인 성격 때문에, 평생학습을 시험하기 가장 어려운 영역으로 형식 수학을 골랐다.
• 린에이전트는 깃허브에서 린 저장소를 수집해 쉬운 것부터 어려운 것 순으로 커리큘럼을 만들고, 검색기를 한 번만 추가 학습한 뒤 트리 탐색으로 증명을 구성한다.
• 이 방식으로 23개 분야에서 155개의 새로운 형식 증명을 만들었고, 새 분야를 배우자 이전 분야 성능까지 올라가는 역방향 전이가 나타났다.
• 발표자는 누구나 직접 돌려볼 수 있도록 일부러 작은 모델을 썼다고 밝히며, 지금이라면 린을 잘 다루는 최신 오픈소스 모델로 바꿔 볼 만하다고 말했다.

쉽게 이해하기

한 스타트업 액셀러레이터가 연 머신러닝 행사에서, 형식 수학 증명을 다루는 연구가 짧은 대담 형식으로 소개됐다. 발표자는 이 연구를 캘리포니아 공과대학에 있을 때 진행했고 지난해 학회에서 발표했다고 설명했다. 주제는 계속 배우면서도 잊지 않는 이른바 평생학습이다.

평생학습의 어려움은 동전의 양면으로 설명됐다. 모델이 너무 안정적이면 사실상 얼어붙어 새로운 것을 못 배우고, 너무 유연하면 빠르게 배우는 대신 앞서 배운 것을 통째로 잊는다. 발표자는 이 사이의 좁은 지점을 찾는 것이 관건이라고 말했다.

무대는 린이라는 언어로 옮겨간다. 린에서는 증명을 코드처럼 쓰고 컴파일러가 그 증명이 맞는지 검사한다. 화면 오른쪽에는 가정과 남은 목표가 표시되고, 목표가 모두 사라질 때까지 한 줄씩 써 내려간다. 각 줄은 함수 호출에 해당하는 전술과, 이미 증명된 정리나 정의에 해당하는 전제로 이뤄진다.

문제는 수학에 존재하는 전제가 너무 많다는 점이다. 증명의 각 단계에서 필요한 전제를 골라내는 검색이 가장 어려운 과제이고, 새 정리가 계속 쌓이는 상황에서 예전 정리를 잊지 않고 검색하는 일은 더 어렵다. 린에이전트는 깃허브에서 린 저장소를 모아 정리마다 증명 단계 수로 난이도를 매기고, 쉬운 정리가 많은 저장소부터 배우도록 커리큘럼을 만든다. 이 커리큘럼은 정리와 전제, 증명을 담는 동적 데이터베이스로 들어간다.

학습은 의외로 단순하다. 가장 많은 지식을 가진 최신 검색기를 가져와 한 번만 더 학습시키는 것이 안정성과 유연성을 맞추는 가장 좋은 방법이었다는 설명이다. 새로 얻은 검색기가 전제를 찾아오면 전술 생성기가 후보를 만들고, 되짚기와 시간 제한을 곁들인 최선 우선 트리 탐색으로 증명을 완성한다. 새로 만든 증명은 다시 데이터베이스로 돌아가 다음 학습의 재료가 된다.

주요 인사이트

• 증명 단계 수를 지수의 밑으로 삼아 정리의 난이도를 정의하고 저장소 단위로 쉬운 문제 비중을 계산하는 방식은, 사람이 커리큘럼을 짜지 않고도 학습 순서를 자동으로 만들 수 있음을 보여준다.
• 새 분야를 배운 뒤 이전 분야 성적까지 오르는 역방향 전이는, 나중에 얻은 개념이 앞서 배운 개념을 다시 정리해 주는 수학 특유의 구조와 맞닿아 있다.
• 검색기를 딱 한 에포크만 추가 학습시키는 단순한 처방이 망각과 정체 사이의 균형점으로 작동했다는 점은, 평생학습이 반드시 복잡한 장치를 요구하지 않을 수 있음을 시사한다.
• 작은 모델을 의도적으로 선택해 개인 연구자도 직접 돌려볼 수 있게 했다는 설계는, 성능 경쟁과 별개로 연구 재현성과 접근성을 우선한 판단이다.
• 한꺼번에 증명을 생성하거나 추론 시점에 강화학습을 붙이는 접근도 작동하지만 계산 비용이 크다는 평가는, 탐색 기반 접근이 여전히 실용적인 선택지임을 보여준다.

자주 묻는 질문

관련 AI 소식