마이크로소프트 연구진, AI 에이전트 도움으로 31년 된 KLS 추측 증명

왜 지금 이 주제인가

마이크로소프트 리서치는 10월 21일 자사 블로그에 머신러닝·최적화 그룹 소속 Xinzhi Zhang 연구원과 Zhao Song이 1995년 제기된 Kannan-Lovász-Simonovits(KLS) 추측을 증명했다고 발표했습니다. 31년간 풀리지 않던 고차원 확률론의 난제입니다. 이 사례가 눈에 띄는 이유는 “AI가 수학 문제를 풀었다”는 식의 단순한 서사가 아니라, 사람이 방향을 정하고 AI 에이전트가 탐색과 계산을 맡는 구체적인 분업 방식을 공개했기 때문입니다. 최근 몇 달 사이 챗봇을 보조 도구로 쓴 수학 논문 소식이 잇따랐지만, 이번 건은 특정 미해결 난제 하나를 정면으로 겨냥해 100개가 넘는 접근법을 체계적으로 걸러낸 과정을 구체적으로 공개했다는 점에서 결이 다릅니다.

핵심 내용

KLS 추측은 Ravi Kannan, László Lovász, Miklós Simonovits가 1995년 제기한 문제로, 고차원 로그오목(log-concave) 확률분포에서 “가장 좋은 초평면(평면) 절단이, 어떤 형태의 절단을 택하더라도 차원과 무관한 보편 상수 범위 안에서는 그에 못지않다”는 내용을 다룹니다. 이번 논문 “An O(1) Bound for the KLS Constant”는 KLS 상수 ψ_n이 차원 n과 무관한 보편 상수 C로 묶인다는 것(ψ_n ≤ C)을 증명했고, 등방(isotropic) 로그오목 확률측도에 대해서도 같은 형태의 바운드(C_P(μ) ≤ C′)가 성립함을 보였습니다. 논문은 10월 1일 arXiv에 처음 제출됐고 10월 4일 수정판이 올라갔으며, 분량은 140페이지입니다. 마이크로소프트 블로그는 이 추측을 고차원 기하학의 중심 미해결 문제로 소개하면서, 이번 증명이 통계학과 최적화, 이론컴퓨터과학에서 널리 쓰이는 등주 부등식 관련 상수의 신뢰도에 영향을 미친다고 설명했습니다.

마이크로소프트 블로그가 밝힌 연구 과정은 이렇습니다. 연구자들은 구조화된 인간 주도 프로세스 안에서 AI 에이전트를 활용해 100개 이상의 후보 접근법을 탐색했습니다. 이 과정에서 AI는 고차 텐서가 섞인 긴 계산을 대신 수행하고, 원고를 작성하고, 증명 단계를 검증하는 역할을 맡았습니다. 연구자들은 이 중에서 유망한 방향을 골라내는 수학적 판단을 담당했습니다. 핵심 돌파구는 새로운 수학적 기준을 찾아낸 뒤, 그 기준을 같은 논증에 재귀적으로 적용해 각 단계마다 더 타이트한 바운드를 만들어내는 방식으로 마련됐습니다.

여기서 중요한 대조 실험이 하나 있습니다. 연구자들은 비슷한 토큰 예산을 주고 여러 최상위 AI 모델에 문제를 단독으로 맡겨봤는데, 이 경우에는 목표를 달성하지 못했습니다. 즉 AI를 그냥 풀어놓는 것과, 사람이 방향을 통제하며 AI를 탐색·계산 도구로 쓰는 것 사이에는 분명한 차이가 있었다는 뜻입니다. 마이크로소프트 블로그는 이번 작업에 구체적으로 어떤 AI 모델이나 도구를 썼는지는 명시하지 않았습니다.

의미와 한계

이번 결과가 맞다면 고차원 확률론과 최적화, 이론컴퓨터과학 전반에서 참고하는 등주(isoperimetry) 관련 상수가 차원에 관계없이 안정적이라는 점이 확인되는 셈입니다. 더 눈여겨볼 부분은 방법론 쪽입니다. “사람이 방향을 정하고 AI가 탐색·계산을 맡는” 분업이 실제 미해결 난제에서 통한 구체적 사례로 제시됐다는 점이, AI 단독 시도가 실패했다는 대조 실험과 함께 설득력을 더합니다.

다만 한계도 분명합니다. 이 결과는 아직 동료 심사를 거치지 않은 arXiv 프리프린트 단계이고, 마이크로소프트 블로그에 따르면 저자들 스스로도 증명을 단순화하고 Lean 4를 이용한 형식 검증을 확대할 계획이라고 밝혔습니다. 즉 수학계의 표준적인 검증 절차가 아직 끝나지 않았습니다. 또한 이번 방식이 다른 미해결 문제에도 반복적으로 적용될 수 있는 일반적 방법론인지, 아니면 KLS 추측이라는 특정 문제의 구조에서만 통한 것인지는 이 사례만으로는 판단하기 어렵습니다. 이 부분은 추측으로만 남겨 둡니다.

한 줄 정리

사람이 방향을 정하고 AI 에이전트가 탐색과 계산을 맡는 분업으로 31년 묵은 수학 난제가 풀렸지만, 동료 심사와 형식 검증은 아직 남아 있습니다.