LLM이 발굴한 수학 정리의 '가치'를 판단하는 방법

핵심 요약

• LLM은 수십 년간 미결된 수학 문제를 풀 수 있게 됐지만, 생성된 정리가 실제로 흥미롭거나 유용한지는 불명확하다.
• 연구팀은 정리의 '내재적 흥미도'를 정의했다: 증명의 길이를 명제의 길이로 나눈 비율로, 정리의 실제 유용성과 강한 상관관계가 있다.
• 증명 난이도를 주어진 전제 조건 하에서 예측하는 것이 흥미도와 유용성 지표를 계산하는 핵심 원시값임을 확인했다.
• 27B 규모의 증명 난이도 예측 모델을 학습시켜 기존의 최첨단 범용 모델보다 정확하게 난이도를 판단할 수 있게 했다.
• 흥미도 지표로 최적화한 결과, 수학 표준 라이브러리 Mathlib과의 중복률이 91.9%에서 30.6%로 감소해 더 새로운 수학이 생성됐다.
• 시스템은 후보 정리를 생성하고, 가장 흥미로운 것을 선택한 후, 자가 확장하는 수학 라이브러리를 반복적으로 구축할 수 있다.
• 이 지표들은 정형 수학 라이브러리 내에서 추측식을 순위 매기고 증명 탐색을 안내하는 실용적이고 정량화 가능한 신호를 제공한다.
• 연구 프레임워크는 인간의 목표 공급에 의존하지 않고 가치 있는 명제를 선택할 수 있는 자가 확장형 기계 검증 수학 라이브러리의 가능성을 보여준다.