azosi · 2026.10.22 00:03 · 조회 0

31년 미제약 KLS 추측, MS가 '인간 주도 AI'로 풀었다

AIMicrosoftResearchKLS수학기하학Lean4arXiv증명humanDirectedAIMicrosoft

한 줄 Hook

마이크로소프트 리서치(Microsoft Research)가 어제(10월 21일), 1995년에 제기된 KLS(Kannan–Lovász–Simonovits) 추측의 완전한 증명을 공식 블로그로 공개했습니다. 31년 동안 최고의 결과조차 차원의 로그 반복함수 수준에 머물렀는데, 이번에는 차원이 늘어나도 변하지 않는 고정 상수로 bound를 잡았습니다. 증명의 결정적 한 수를 깬 건 AI였지만, 방향을 잡고 결과물을 검증한 건 사람이었다고 회사는 분명히 선을 긋습니다.

배경: KLS 추측이 뭔가

KLS 추측은 고차원 확률분포(log-concave)에 잘 맞는 "납작한" 자르기(초평면, hyperplane) 가 임의 형태의 자르기와 항상 고정 비율(상수배) 이내로 동등하다는 주장입니다. 1995년 Kannan, Lovász, Simonovits 세 사람이 제기했고, Simons Institute는 이를 "convex geometry의 가장 중요한 미해결 문제 중 하나"로 규정했습니다(Microsoft Research Blog 인용).

이 명제가 중요한 까닭은 표면적 기하를 넘어섭니다. 잘라내는 면적의 비율은 고차원에서 random walk가 분포를 얼마나 빨리 탐색하는지를 좌우하고, 그 속도는 통계·최적화·알고리즘 전반의 표본 효율과 직결됩니다. 그래서 30년간 차원 의존성을 조금씩 깎아내리는 작업이 줄곧 최전선 과제였습니다.

무엇이 증명됐나

Microsoft Research의 시니어 리서처 Xinzhi Zhang(Machine Learning and Optimization 그룹)과 공동 연구자 Zhao Song이 차원이 무한히 커져도 bound가 늘어나지 않는 O(1), 즉 차원 독립 상수 C로 ψₙ ≤ C 가 성립함을 보였습니다.

  • 논문: "An O(1) Bound for the KLS Constant" (arXiv 2610.01447)
  • 타임라인: v1은 2026년 10월 1일, 완성판 v2는 2026년 10월 4일 게재
  • 이전 최선: 차원에 따라 천천히(거의 로그 반복함수 수준) 늘어나는 bound (2026년 7월 결과). 이번에 그 의존성이 완전히 제거됨
  • 핵심 수학적 아이디어: 새로운 "고차 기울기 평균의 도함수" 기준을 도입하고, 이를 재귀적으로 다시 bound에 끼워 넣어 차원의 흔적을 지운 것. 재귀 정밀화 단계 자체는 저자들의 빠른 선형계획법(fast linear programming) 관련 후속 작업에서 나온 아이디어로, 회사는 이를 강조합니다

"AI가 했다"보다 더 중요한 것 — 어떻게 썼는가

Microsoft Research는 이번 작업의 AI 활용 방식을 표현부터 명확히 적었습니다. 요약하면 "agentic search process with iterative, human-assisted pruning" — 여러 AI 에이전트가 후보 수학적 접근을 병렬로 탐색하고, 연구자가 중간 결과를 검토해 약한 방향을 버리며 다음 라운드에 유망한 후보만 넘기는 방식입니다. 회사 측 설명에 따르면 약 100개의 연구 경로(trajectory) 가 검토된 끝에 핵심 breakthrough에 도달했습니다.

블로그는 인간과 AI의 역할 분담도 구체적으로 적었습니다.

"연구진이 수학적 방향을 정했고, 유망한 아이디어를 골라 최종 논증으로 묶었으며, 증명을 검증했다. AI 도구는 후보 접근을 탐색하고, 계산을 수행하며, 원고 작성과 내부 증명 점검을 보조했다." (Zhang의 블로그 본문 의역)

회사 측은 한 가지 대조 실험도 함께 공개했습니다. 동일한 총 토큰 예산으로 여러 최첨단 모델에 무감독으로 같은 문제를 풀게 했지만, 그 시도들은 성과가 부족했다고 합니다. 즉 이번 결과는 "AI가 알아서 풀었다"가 아니라 AI를 도구로 쓰는 사람의 수학이 더 깊었다는 메시지입니다.

검증도 삼중으로 들어왔다

수학적 breakthrough의 진짜 무게는 검증 무게에 있습니다. 회사는 세 갈래의 외부 확인을 함께 언급했습니다.

  • 독립 증명 1: 같은 10월 4일, Pierre Bizeul·Boaz Klartag·Joseph Lehec가 평행하게 진행한 별도 증명도 arXiv에 올라왔고, 초록에 "핵심 단계는 Song과 Zhang의 최근 고차 기울기 평균 기준"이라고 명시
  • 독립 증명 2: 같은 날 등장한 세 번째 별도 증명
  • 기계 검증: Lean 4 형식화(formalization)가 함께 공개

세 갈래 중 하나만 있어도 가치가 큰데, 이틀 안에 세 갈래가 동시에 쏟아졌다는 점이 이번 사건의 학술적 무게를 더합니다.

시사점

이번 발표는 두 갈래로 읽힙니다. 하나는 수학적입니다. 31년 미해결이 차원 독립 상수 한 줄로 정리됐고, 그 한 줄을 깬 아이디어가 재귀 자기-정밀화 구조였다는 점은 향후 고차원 샘플링·최적화 분야로 빠르게 번질 여지가 있습니다.

다른 하나는 AI 활용 방식입니다. 회사가 "human-directed AI"라는 표현을 명시적으로 쓴 데서 알 수 있듯이, 이번 사례는 "AI가 수학자를 대체했다"는 단순한 그림이 아니라 AI 에이전트의 병렬 탐색 + 인간 연구자의 pruning 이라는 협업 모델이 실제로 어려운 미해결과에서도 작동할 수 있다는 한 장의 증거입니다. Lean 4 형식화까지 같은 흐름 안에 들어가 있는 점도, 앞으로 AI 보조 증명이 학술 출판 쪽으로 어떻게 들어오는지를 보여주는 시그널입니다.

Microsoft Research 측 블로그에 따르면 논문은 동료 평가 절차를 거쳐 별도 발표를 준비 중이며, 이번 형식화도 별도 경로로 공개될 예정입니다.

출처


본 글은 Microsoft Research 공식 블로그 본문과 동 논문 arXiv PDF의 메타데이터를 1차 출처로 삼아 작성되었습니다. Simons Institute의 "가장 중요한 미해결 문제 중 하나" 표현은 Microsoft Research 블로그 본문 내 인용입니다. 추가적인 차원 의존성 수치 등 미공개 항목은 본문에 포함하지 않았습니다.

댓글

아직 댓글이 없습니다.

댓글을 작성하려면 로그인이 필요합니다.