AI 정리 증명의 다음 과제, 증명 단축: 린 증명을 사람 시범 없이 절반으로 줄인 MIT 연구

핵심 메시지

• 형식 정리 증명은 컴파일러가 옳고 그름을 100% 판정해 주는 영역이라, 검증된 소프트웨어와 하드웨어처럼 오류를 허용할 수 없는 분야에서 특히 쓸모가 있다.
• 발표자가 참여한 린도조는 방대한 수학 라이브러리에서 정리·전술·전제를 자동으로 뽑아내는 도구다. 코드만으로는 알 수 없는 증명 중간 상태를 실제로 실행해 추출한다는 점이 핵심이다.
• 여기서 만든 리프루버 모델은 2억 9천만 파라미터에 불과하지만, 필요한 보조정리를 먼저 검색해 붙여 주는 방식으로 훨씬 큰 범용 모델을 앞섰다. 특히 학습 때 본 적 없는 보조정리를 써야 하는 문제에서 격차가 컸다.
• 최근 모델들은 어려운 문제를 풀긴 하지만 4천 줄이 넘는 읽을 수 없는 증명을 쏟아낸다. 발표자는 이 문제를 겨냥해, 사람이 만든 정답 시범 없이 증명을 스스로 짧게 다듬는 모델을 훈련했다.
• 이 모델은 특정 벤치마크 증명을 최대 87%까지 줄였고, 국제수학올림피아드 문제의 초장문 증명도 절반가량으로 압축했다. 짧아진 증명은 대체로 실행 속도까지 빨라졌다.

쉽게 이해하기

미쓰비시전기 연구소가 여는 세미나에서 MIT 박사과정 알렉스 구가 형식 수학과 언어모델을 주제로 발표했다. 형식 정리 증명은 가정과 결론을 형식 논리로 적고, 증명 보조기가 한 단계씩 검증하는 방식이다. 그는 최대공약수에 관한 간단한 정리를 예로 들어, 목표를 경우로 쪼개고 정의를 펼치고 이미 증명된 보조정리로 바꿔 쓰는 전술들이 어떻게 하나의 증명 트리를 이루는지 보여 줬다.

발표 전반부는 몇 해 전 공개된 린도조다. 언어모델을 훈련하려면 데이터가 있어야 하는데, 깃허브에 올라온 린 코드에는 각 단계에서 증명이 어떤 상태였는지가 적혀 있지 않다. 린도조는 코드를 구문 트리로 파싱해 전술의 위치를 파악하고, 메타프로그래밍으로 코드를 실제 실행해 각 단계 전후의 상태를 뽑아낸다. 어떤 보조정리가 같은 파일에서 왔고 어떤 것이 다른 파일에서 왔는지까지 기록해, 검색 모델 훈련에 쓸 수 있게 했다.

이 데이터로 훈련한 리프루버는 검색 증강 방식을 쓴다. 현재 증명 상태에서 쓸 수 있는 보조정리들을 인코더로 임베딩해 코사인 유사도로 후보를 고르고, 그 후보들을 상태에 이어 붙여 다음 전술을 생성한다. 인코더 훈련에는 대조 학습을 썼는데, 오답 후보를 아무 데서나 뽑지 않고 정답과 같은 파일에서 골라 일부러 구분하기 어렵게 만든 점이 성능에 기여했다. 이름을 외워서 쓰는 방식으로는 처음 보는 보조정리를 쓸 수 없다는 한계를 검색이 메운 것이다.

후반부 주제는 증명의 품질이다. 발표자는 최신 증명 모델이 국제수학올림피아드 문제에 대해 내놓은 4천 줄이 넘는 증명을 화면에 띄우고, 기계는 통과시키지만 사람은 이해할 수 없고 불필요하게 느린 코드라고 지적했다. 그래서 그는 인턴십 중 동료들과 함께, 사람이 만든 단축 예시를 전혀 주지 않고도 증명을 짧게 다듬는 모델을 만들었다.

데이터는 자동으로 만들었다. 자연어 수학 문제와 풀이를 모아 너무 쉬운 것을 걸러 내고, 모델이 전체 증명 대신 뼈대만 형식화하게 한 뒤, 그 뼈대의 각 단계를 독립된 정리로 떼어 낸다. 한 줄로 끝나는 정리는 다시 걸러 내고 남은 문제들을 대형 증명 모델로 증명하게 해 14만 5천 개 표본을 얻었다. 이 데이터로 두 갈래 훈련을 돌렸는데, 하나는 짧아진 증명만 골라 다시 학습하기를 반복하는 전문가 반복이고 다른 하나는 상대 단축률을 보상으로 주는 강화학습이다.

주요 인사이트

• 증명이 맞는지 확인하는 데는 별도의 채점이 필요 없다. 짧아진 증명을 린 컴파일러에 넣어 통과하면 그것으로 증명이 성립한 것이라, 훈련 신호를 자동으로 얻을 수 있다는 점이 이 접근의 토대다.
• 전문가 반복 모델과 강화학습 모델은 쓰임새가 갈렸다. 여러 번 뽑아 가장 짧은 것을 고르려면 다양성이 살아 있는 전문가 반복 쪽이 낫고, 한 번만 뽑아 쓸 거라면 다양성을 잃는 대신 단일 시도 성적이 좋은 강화학습 쪽이 낫다.
• 짧게 다듬은 증명으로 훈련한 증명 생성 모델은 원본으로 훈련한 모델보다 성적이 조금 더 높았다. 큰 차이는 아니지만, 긴 증명을 그대로 학습시키는 대신 한 번 정리하고 학습시키는 경로에 여지가 있음을 시사한다.
• 증명이 길수록 줄이기 어려웠다. 짧은 증명은 쉽게 압축되지만 수천 줄짜리는 20~40% 정도에 그쳤고, 발표자는 샘플을 늘릴수록 개선이 이어지되 그 속도는 완만해진다고 설명했다.
• 길이를 목표로 삼는 것은 편의적 선택일 뿐이라고 발표자는 선을 그었다. 실제로 원하는 것은 읽기 쉽고 빠르며 라이브러리 관리자가 받아들일 만한 증명이며, 알고리즘 자체는 다른 복잡도 지표에도 그대로 쓸 수 있다.

자주 묻는 질문

관련 AI 소식