AI가 증명할 가치가 있는 수학을 찾도록 가르치기

들어가며

대규모 언어 모델은 고급 수학 문제를 풀고, 기계가 검증할 수 있는 형식 증명을 작성하는 능력을 빠르게 높이고 있다. 그러나 모델이 수많은 명제를 제시하고 증명할 수 있게 되면 새로운 문제가 생긴다. 그중 어떤 결과가 실제로 연구할 가치가 있는지 어떻게 판단할 것인가?

논문 「Learning to Discover Interesting Mathematics」는 증명 성공률만 높이는 대신, 수학적 발견 후보를 순위화할 수 있는 실용적 신호를 제안한다. 목표는 단순히 맞는 명제를 만드는 것이 아니라, 기존 지식을 반복하지 않으면서 구조적이고 잠재적으로 유용한 결과를 찾는 것이다.

핵심 접근법

• 흥미도를 길이의 비율로 정의한다. 연구진은 정리의 내재적 흥미도를 증명 길이를 명제 길이로 나눈 값으로 정의했다. 짧고 간결한 주장에 상대적으로 긴 추론이 필요하다면, 거의 즉시 따라오는 결론보다 더 많은 수학적 구조를 담고 있을 수 있다는 직관이다.
• 전제가 주어졌을 때의 증명 난이도를 예측한다. 후보 정리를 평가하려면 기존 가정과 수학 라이브러리를 활용했을 때 증명이 얼마나 어려운지 알아야 한다. 연구팀은 이를 위해 27B 규모의 모델을 학습했으며, 최첨단 범용 모델보다 조건부 증명 난이도를 더 정확히 예측했다고 보고했다.
• 생성, 선별, 검증을 반복한다. 시스템은 후보 정리를 생성한 뒤 흥미도 기준으로 순위를 매긴다. 검증된 결과는 계속 확장되는 형식 수학 라이브러리에 추가되고, 이후 탐색에서 새로운 전제로 활용된다.

결과와 의미

논문은 제안한 지표를 최적화한 뒤 생성 정리의 흥미도가 4.3배 높아졌다고 보고한다. 또한 Mathlib과 상당 부분 또는 완전히 겹치는 결과의 비율이 91.9%에서 30.6%로 낮아졌다. 이는 시스템이 기존 라이브러리의 단순한 재표현이나 조합을 넘어, 더 분포 밖에 있는 형식 수학을 생성할 가능성을 보여준다.

이 연구의 핵심 기여는 수학에서 자주 인간의 직관에 의존하던 “흥미롭다”는 판단을 학습과 탐색에 사용할 수 있는 신호로 바꾼 데 있다. 다른 수학 영역에서도 이 지표와 실제 활용성 사이의 관계가 확인된다면, 제한된 증명 탐색 자원을 향후 연구로 이어질 가능성이 높은 추측에 집중할 수 있다.

다만 증명이 길다고 해서 수학적으로 중요한 것은 아니다. 형식화가 비효율적이면 단순한 정리도 긴 증명을 요구할 수 있고, 반대로 짧은 증명이 매우 깊은 결과를 나타낼 수도 있다. 따라서 이 지표는 최종적인 가치 평가라기보다 후보를 고르는 보조 기준으로 보는 편이 타당하다. 개념적 의미와 일반성, 실제 활용 가능성을 판단하는 역할은 여전히 수학자에게 남아 있다.

그럼에도 명제 생성, 기계 검증, 후보 평가, 라이브러리 확장을 하나의 순환으로 묶은 구조는 자기 확장형 형식 수학 라이브러리의 가능성을 보여준다. 앞으로의 과제는 단순히 더 어려운 증명을 만드는 데 그치지 않고, 인간 연구자가 이해하고 후속 연구를 이어가고 싶어 하는 수학을 생성하는 것이다.

출처: Hugging Face Daily Papers