OpenAI "AI가 ETH 반증", 수학·물리 난제 3건 발표

출처: OpenAI
원문: https://openai.com/index/building-scientific-understanding-with-academic-communities/
작성자: 팔복소프트-김팔복

한눈에 보기

• OpenAI가 내부 모델이 수학, 컴퓨터과학, 물리학에서 오래된 난제 세 건을 풀었다고 2026년 10월 26일 발표했습니다.
• 컴퓨터과학 쪽 주장은 복잡도 이론의 기본 가정으로 쓰여 온 지수 시간 가설(ETH)이 거짓이라는 것이고, 증명은 Lean으로 형식 검증했다고 합니다.
• 수학 쪽은 국소 평활화(local smoothing) 추측을 모든 차원에서 증명했고, 그 결과로 Kakeya 추측과 Stein의 제한 추측도 모든 차원에서 풀린다고 설명합니다.
• 물리 쪽은 QCD(양자색역학)를 포함한 4차원 게이지 이론의 수학적 존재 증명이며, 밀레니엄 문제의 일부인 순수 Yang–Mills 이론의 존재 증명도 들어 있다고 합니다.
• 세 결과 모두 외부 전문가 그룹이 검증과 해설을 맡고, 공개 방식은 분야마다 다르게 정했습니다.
• OpenAI는 이 발견에 대한 학문적 공로를 요구하지 않겠다고 밝혔습니다.
• 아직은 OpenAI의 주장이며, 독립 검증은 이제 시작 단계입니다.

배경

ETH는 "논리식 만족 가능성(SAT) 문제는 어떤 알고리즘을 써도 변수 개수에 대해 지수 시간보다 크게 빨라질 수 없다"는 가정입니다. 증명된 정리는 아니지만 거의 모두가 참이라고 믿었기 때문에, "ETH가 참이면 이 문제는 이보다 빨리 풀 수 없다"는 식의 조건부 하한 결과가 이 가정 위에 쌓여 왔습니다. Lean은 증명을 기계가 한 줄씩 검사하는 증명 보조기(proof assistant)로, AI가 만든 증명의 논리적 빈틈을 사람보다 먼저 걸러 줍니다.

주요 내용

세 가지 결과와 공개 방식

그림 1. 분야별 결과와 외부 전문가 그룹이 정한 공개 방식 (팔복소프트 작성)

ETH 쪽 셰퍼드 구성이 특히 눈에 띕니다. Impagliazzo와 Paturi는 Francis Zane과 함께 ETH를 처음 제안한 사람들이고, Williams는 ETH의 강한 버전을 반증한 이력이 있습니다. 가설을 만든 당사자가 반증을 검증하는 셈입니다. 이 그룹은 원자료 전체 공개와 OpenAI의 학회 후원을 조건으로 걸었고, OpenAI가 받아들였습니다. 다만 OpenAI도 실제로 더 빠른 알고리즘을 찾고 실무 개선으로 연결하려면 상당한 추가 연구가 필요하다고 분명히 적었습니다.

진행 과정

그림 2. AI 증명이 공개되기까지의 단계 (팔복소프트 작성)

ETH 반증은 10월 16일 자연어 증명, 다음 날 Lean 형식화까지 마쳤고 수학 결과도 10월 18일 출력 후 하루 만에 형식화했습니다. 물리 결과는 9월에 증명이 나왔지만 길이와 복잡도 때문에 Lean 형식화가 끝날 때까지 공개를 미뤘습니다.

협업 원칙

외부 그룹과의 협업에는 네 가지 원칙이 붙습니다. 비밀유지계약 없이 협업 사실을 공개하고(투명성), OpenAI는 발견에 대한 학문적 공로를 주장하지 않으며, 해설과 논문을 쓴 그룹이 그에 대한 인정을 받고, 참여는 자발적·무보수이며 그룹은 OpenAI를 대변하지 않습니다(독립성). OpenAI는 첫 셰퍼드를 고르는 일 자체가 누가 먼저 참여하느냐를 정하고 정보 비대칭을 만든다는 한계도 스스로 인정했습니다. 이와 별도로 Simons Foundation에 500만 달러를 기부해 AI가 만든 결과를 연구자가 이해하고 확장하는 워크숍과 학회를 지원한다고 밝혔습니다.

팔복소프트 관점

• "검증됨"의 범위를 구분해야 합니다. Lean 검증은 "주어진 정의에서 결론이 논리적으로 따라 나온다"는 강한 보증이지만, 정의를 제대로 옮겼는지(형식화가 원래 문제를 정확히 표현하는지)는 결국 사람이 확인해야 합니다. 셰퍼드 그룹을 따로 꾸린 이유도 여기에 있으니, 제목만 보고 "증명 끝"으로 받아들이지 않는 게 맞습니다.
• 실무 개발자에게 당장 바뀌는 건 없습니다. ETH 반증은 "더 빠른 알고리즘이 존재할 여지"가 생겼다는 뜻이지, 내일 쓸 수 있는 SAT 솔버가 나왔다는 뜻이 아닙니다. OpenAI 스스로도 실용 알고리즘까지는 먼 길이라고 했습니다. 다만 국내에서도 스케줄링, 경로 최적화, 검증 도구처럼 SAT·제약 충족 문제를 직접 다루는 팀이라면, 공개된 증명에서 어떤 아이디어가 쓰였는지 학계 해설이 나올 때 챙겨 볼 가치가 있습니다.
• ETH를 근거로 한 "더 빨리 못 푼다"는 주장은 다시 봐야 합니다. 원문에 따르면 그래프 이론, 계산생물학, 데이터베이스, 계산기하 등 수백 편의 논문이 ETH를 전제로 하한을 증명했습니다. 사내 기술 문서나 설계 근거에 "ETH에 따르면 불가능"이라고 적어 둔 곳이 있다면 표시해 둘 만합니다. 참고로 이번 발표에는 암호 체계에 대한 언급이 없으니, 이를 곧바로 보안 문제로 연결하는 해석은 경계해야 합니다.
• 더 큰 변화는 "AI 결과를 어떻게 공개하느냐"입니다. AI가 만든 결과물을 "원자료"로 취급하고 해석과 공로는 사람 연구자에게 넘기는 구조는, 사내에서 AI 에이전트가 만든 분석이나 코드를 누가 검증하고 누구 이름으로 남길지 고민하는 팀에게도 참고가 됩니다.

정리

이번 발표의 핵심은 AI가 낸 증명을 Lean으로 먼저 거르고, 해석은 해당 분야의 대표 연구자에게 맡기는 절차를 공식화했다는 점입니다. ETH 반증이 사실로 확인되면 복잡도 이론 교과서가 바뀌겠지만, 개발 현장에 영향이 오려면 학계 해설과 알고리즘 연구가 먼저 쌓여야 합니다. 지금은 셰퍼드 그룹들이 어떤 결론을 내는지 지켜보는 단계입니다.

• OpenAI
• 지수 시간 가설
• Lean
• 계산 복잡도
• AI 수학