LLM 추측 생성 vs 증명 검사, 승자는?

두 번째 커피와 세 번째 커피 사이 어딘가에서, 많은 계산복잡도 이론가들이 전혀 예상치 못한 문장을 읽었습니다. 임의의 불리언 식의 만족 할당 개수를 대략 2^(n/√(log n)) 시간에 세는 결정적 알고리즘이 있다는 내용이었죠. 이는 준지수적(sub-exponential) 시간으로, 이 분야의 핵심 가정 중 하나인 지수 시간 가설(ETH)을 정확한 기술적 의미에서 반박하는 결과입니다. 이 주장은 대학 연구팀이 아니라 AI 연구소에서 나왔고, 증명은 대형 언어 모델과의 협업으로 만들어졌습니다. 발표에 대해 어떻게 생각하든, 이 일은 추측 생성, 즉 기계가 수학을 채점하는 데서 나아가 새로운 수학을 제안하는 단계가 데모 수준을 벗어났다는 신호입니다.

연구소는 세 가지 결과를 묶어 발표했습니다. 위의 복잡도 이론 결과, 모든 차원에서의 케이케야 추측(Kakeya conjecture) 증명 주장, 그리고 표준 모형의 “통합 완성”이라고 설명된 물리학 결과인데, 이것은 형식 검증이 끝날 때까지 보류되었습니다. 반응도 익숙한 패턴으로 갈렸습니다. 내용에 대해서는 진심으로 놀라고, 포장 방식에 대해서는 진심으로 짜증을 냈죠. 비판자들은 자전거 제조사가 자전거 경주에서 자기들이 이겼다고 발표하는 것에 비유했습니다. 꽤 적절한 비유입니다. 하지만 내용 자체는 더 천천히 들여다볼 가치가 있습니다. 이 발표에는 언어 모델이 수학에 접근하는 두 가지 아주 다른 방식과, 그중 어느 쪽을 실제로 믿어야 하는지에 대한 중요한 교훈이 담겨 있기 때문입니다.

AI 수학 발표가 실제로 주장하는 내용

가장 명확하게 의미가 큰 복잡도 결과부터 보겠습니다. 지수 시간 가설은 대략 3-SAT을 2^o(n) 시간에 풀 수 없다고 말합니다. 변수 개수에 대해 의미 있게 준지수적인 알고리즘은 존재하지 않는다는 뜻이죠. 매개변수화 복잡도와 세분화 복잡도(fine-grained complexity) 분야의 수백 편 논문이 하한을 증명하기 위해 ETH에 기대고 있습니다. “ETH를 가정하면”으로 시작하는 정리들을 한 경력 전체에 쌓아 올리는 그런 가정이에요. 새 프리프린트는 다항 공간을 사용하고 시간은 2^(n/(log n)^(1/2+o(1)))에 다항 인수를 곱한 정도인 k-CNF 식의 결정적 계수 알고리즘을 설명합니다. 이 지수는 o(n)이고, 바로 ETH가 금지하는 형태입니다. 이 알고리즘은 여전히 극도로 느려서 실제 인스턴스에 돌릴 사람은 없겠지만, 점근적으로는 결정적입니다. 증명이 성립한다면, 지난 20년간 하한 논증을 떠받쳐 온 가설이 그냥 존재하지 않게 되는 셈입니다.

두 번째 주장은 케이케야 추측을 겨냥합니다. 단위 선분이 모든 방향을 향하도록 포함하는 가장 작은 집합에 관한 기하학적 측도론 문제입니다. 3차원 경우는 2025년에야 풀렸는데, Hong Wang과 Joshua Zahl의 주목받은 증명이 그것이었고, 많은 사람이 이를 경력의 정점으로 여겼습니다. 이번 발표는 모든 차원에서의 증명을 주장하는데, 이것이 사실이라면 그 돌파구를 완전히 포함하게 됩니다. 세 번째 결과는 양자장론 분야의 것으로, 셋 중 가장 모호합니다. “표준 모형의 통합 완성”이라고 묘사되지만 아직 공개되지 않았고, 기계 검증 형식화를 기다리는 것으로 보입니다. 티저를 읽은 물리학자들은 이것이 문자 그대로의 만물 이론이라기보다 대통일 이론류의 구성에 가깝다고 의심하고 있으며, 그 표현 방식이 정당한 의심을 받을 만합니다.

발표 진행 방식에서 인정할 만한 점이 두 가지 있습니다. 연구소는 공개 전에 실제 수학자와 물리학자들을 참여시켰습니다. 앞선 서툰 수학 발표에 대한 반발을 의식한 조치이며, 이후 Terence Tao 등이 바로 이런 식의 참여를 공개적으로 요구했습니다. 또 물리학 결과는 형식화가 끝날 때까지 보류되었는데, 이는 올바른 우선순위입니다. 하지만 여전히 답이 없는 어려운 질문들이 있습니다. 외부에서는 컴퓨팅 비용이 얼마인지 아무도 모르고, 같은 돈을 사람 연구자에게 투입했다면 같은 정리가 나왔을지도 알 수 없으며, 영리 기업 연구소가 주주의 투표를 받게 되면 호기심 중심의 연구에 계속 자금을 댈지도 불분명합니다. 또 비판자들이 즉시 지적한 불편한 순환 구조도 있습니다. 이 모델들은 지금 그 결과에 박수를 쳐 달라고 요청받는 바로 그 연구 커뮤니티의 질문, 초안, 포럼 글 등을 부분적으로 학습했습니다.

증명 검사 vs 추측 생성: 서로 다른 두 가지 일

과장을 걷어내면, AI 수학 시스템은 모두 두 가지 일 중 하나를 하고 있습니다. 첫 번째는 증명 검사입니다. 주어진 후보 논증이 유효한지 판단하는 일이죠. 두 번째는 추측 생성입니다. 문제 영역이 주어졌을 때 시도할 가치가 있는 것, 즉 보조정리, 구성, 알고리즘, 반례 등을 제안하는 일입니다. 둘은 같은 기술의 두 반쪽처럼 들리지만 그렇지 않습니다. 서로 다른 계산 문제이고, 서로 다른 오라클, 서로 다른 실패 양상, 완전히 다른 신뢰 프로필을 가집니다. 이 둘을 뭉뚱그리면 보도자료를 과신하거나 실제 진전을 무시하게 됩니다.

검사에는 오라클이 있습니다. Lean으로 쓴 증명은 커널에 대해 컴파일되거나 아니거나 둘 중 하나이고, 커널은 작성자가 얼마나 자신 있게 말했는지 신경 쓰지 않습니다. 검사는 크게 실패합니다. 거부된 tactic 블록은 모호함이 없습니다. 생성에는 오라클이 없습니다. 제안된 추측은 참일 수도, 거짓일 수도, 자명하게 참일 수도, 1987년에 다른 표기로 이미 발표된 참일 수도 있습니다. 생성은 조용히 실패하며, 그 실패 양상은 사회적입니다. 그럴듯하게 들리는 헛소리이거나, 진짜 결과를 새로운 척 포장한 것이죠. 여기서 품질은 중요성과 독창성으로 측정되는데, 이는 어떤 결정 가능한 기준이 아니라 사람의 안목으로 정의되는 속성입니다.

그렇다면 왜 생성이 갑자기 쓸 만해졌을까요? 최신 추론 모델이 단순히 프롬프트로 유도되는 것이 아니라 긴 사고 사슬을 위해 학습되었기 때문입니다. 검증 가능한 보상에 대한 강화학습(주로 답을 기계적으로 확인할 수 있는 수학과 코드)이 이 시스템들이 한 토큰씩 자동완성하는 대신 단계들의 공간을 실제로 탐색하도록 가르쳤습니다. 머릿속에 담아 두셨으면 하는 비유가 있습니다. 증명 검사기는 컴파일러이고, 추측 생성기는 설계자입니다. 둘 다 가치가 있습니다. 하지만 설계자가 자기 작업을 스스로 인증하게 두는 일은 절대, 절대 해서는 안 됩니다.

검증할 수 없는 증명은 설교이고, 테스트할 수 없는 추측은 소문이다.

자동 증명 검사가 이기는 경우

검사기는 형식적 기준이 존재하고 검토 대상이 사람이 한 줄씩 감사하기에는 너무 길거나 지루할 때 이깁니다. Lean 4와 커뮤니티 라이브러리 Mathlib이 이 분야의 사실상 표준 무대가 되었습니다. 정의와 증명을 프로그래밍 언어로 작성하면, 작고 별도로 감사할 수 있는 커널이 모든 추론 단계가 합법인지 판정합니다. 그 위에 세워진 방대한 수학에 비해 신뢰 기반이 아주 작은데, 바로 이런 비대칭이 필요한 것입니다.

실제 루프는 이렇게 돌아갑니다. 모델이 tactic 수준의 증명 단계를 초안으로 작성하면, 커널이 각 단계를 받아들이거나 거부하고, 거부 메시지는 다음 시도의 문맥으로 다시 전달됩니다. 이것이 모델 출력을 엄격한 문법으로 제약하는 것이 즉시 효과를 내는 유일한 환경입니다. 문법적으로 유효한 tactic만 샘플링하므로, 환각의 여러 유형이 구조적으로 불가능해집니다. 최소한의 예시로, 요즘 모델이 몇 초 만에 처리하는 종류의 보조정리를 보겠습니다.

import Mathlib
-- The sum of two even natural numbers is even.
theorem even_add_even {a b : ℕ} (ha : Even a) (hb : Even b) : Even (a + b) := by
rcases ha with ⟨k, rfl⟩   -- a = k + k for some k
rcases hb with ⟨l, rfl⟩   -- b = l + l for some l
exact ⟨k + l, by ring⟩    -- witness k + l; ring closes the algebra

이 예시가 역할 분담에 대해 무엇을 보여주는지 주목하세요. 창의적인 동작은 증인 k + l을 고르는 것이고, 검사 동작은 ring이 대수를 검증하는 것입니다. 사람과 모델은 둘 다 첫 번째에는 꽤 능숙합니다. 두 번째에서 신뢰할 수 있는 것은 커널뿐이고, 커널은 지치지도, 대충 훑지도, 분위기로 채점하지도 않습니다. 발표 전체에서 가장 믿을 만한 요소는 바로 이 관문입니다. 물리학 논문이 Lean 형식화가 끝날 때까지 보류되었다는 주장이 사실이라면, 워크플로가 의도대로 작동한 것입니다. 기계가 제안하고, 기계가 판정하며, 보도자료는 차례를 기다리는 것이죠.

추측 생성이 이기는 경우

생성은 탐색 공간이 조합론적이고 평가가 저렴할 때 이깁니다. DeepMind의 FunSearch가 2023년에 이 틀을 세웠습니다. 언어 모델이 프로그램 형태의 가설을 제안하면, 빠른 평가기가 점수를 매기고, 진화 루프가 최고의 것을 남기는 방식입니다. 이 구조는 cap set에 대한 새로운 구성과, 수십 년간의 수작업 튜닝보다 나은 bin-packing 휴리스틱을 만들어냈습니다. AlphaEvolve는 같은 아이디어를 더 밀어붙여, 여러 결과 중에서도 Strassen 시대 이후 유지되던 4×4 행렬 곱셈 알고리즘에서 곱셈 하나를 줄였습니다. 이 시스템들이 기하학을 이해한다고 주장하는 사람은 없습니다. 그럴 필요도 없습니다. 제안만 하면 되고, 평가기가 정직하기만 하면 됩니다.

ETH 알고리즘은 이 패턴에 거의 의심스러울 만큼 잘 맞습니다. “알고리즘 아이디어”의 공간은 어마어마하고, 사람 연구자들은 강한 사전 지식을 가지고 그 공간을 탐색합니다. 이를 공손하게 말하면 사각지대입니다. 특정 표현 기법과 특정 재귀 구조를 결합해야 하는 구성은 누구의 탐색 경로도 근처를 지나간 적이 없다는 이유만으로 30년 동안 탐색되지 않은 채 남아 있을 수 있습니다. 완전하고, 사전 지식 없이 하고, 약간 멍청하기까지 한 탐색이야말로 기계가 테이블에 가져오는 것입니다. 같은 논리가 생성-반박 루프의 근거이기도 합니다. 추측을 제안하고, 즉시 작은 경우에 대해 반례를 계산으로 찾아 죽여 보는 것이죠. 대부분의 추측은 몇 분 안에 죽는데, 괜찮습니다. 반박 하나하나가 다음 제안을 날카롭게 만들고, 살아남은 것들만 사람이 오후를 투자할 가치가 있습니다.

또 존중할 만한 심리적 비대칭도 있습니다. Wang과 Zahl의 3차원 케이케야 증명은 분야 최정상에서 여러 해의 집중적 노력이 필요했습니다. 모델 보조 탐색이 실제로 모든 차원의 논증을 만들어냈다면, 그것은 거의 확실히 지형을 가로지르는 다른 경로를 찾은 것입니다. 꼭 더 깊은 경로는 아니고, 다른 경로입니다. 다름이야말로 탐색이 하는 일입니다. 위험은 기계가 추측을 만드는 데 있지 않습니다. 뒷받침할 장치 없이 생성된 추측을 누군가 발표하는 데 있습니다. 이것이 여러분이 실제로 만들어야 할 파이프라인 부분으로 이어집니다.

AI가 만든 증명을 위한 검증 루프 구축

AI 생성 수학의 이점을 민망함 없이 누리고 싶다면, 모델보다 워크플로가 더 중요합니다. 제가 돌릴 파이프라인은 다음 순서입니다.

1. 넓고 저렴하게 생성하세요. 이 단계에서는 깊이보다 다양성이 낫습니다. 하나의 다듬어진 시도가 아니라 아이디어 공간의 커버리지가 필요합니다.
2. 문헌과 대조해 중복을 제거하세요. arXiv와 MathOverflow에 대한 검색으로, 가장 흔한 실패를 잡아냅니다. 낯선 표기를 입은 이미 알려진 결과를 “새로운” 추측으로 내놓는 경우죠.
3. 저렴한 실험적 필터를 적용하세요. 작은 경우를 수치적으로 테스트하고, 계산으로 반례를 찾으며, 명백히 거짓인 명제는 빨리 죽게 두세요.
4. 살아남은 것들을 형식화하세요. Lean, Isabelle, Rocq 중 원하는 증명 도구를 고르되, 이것이 비싼 단계이며 자연어 증명은 결과가 아니라 스케치일 뿐임을 이해하세요.
5. 새로움과 표현 방식에 대해 사람이 검토하세요. 이게 중요한가? 명제가 애초에 올바른 것인가? 모델은 증명 가능한 것을 최적화하고, 사람은 증명할 가치가 있는 것을 결정합니다.

발표된 공동 연구도 대략 이 형태를 따랐습니다. 연구자들이 공개 전에 참여해 5단계를 실질적으로 담당한 것이죠. 예전처럼 프리프린트를 던져 놓고 소셜 미디어가 심판을 보게 하던 방식보다 분명 나아진 점입니다. 다만 파이프라인의 비대칭을 주목하세요. 1~3단계는 저렴하고 컴퓨팅에 따라 확장되며, 4단계가 병목이고, 5단계는 전혀 확장되지 않습니다. 이 분야에서 도구를 만든다면, 더 크고 더 자신만만한 생성기가 아니라 병목에 돈을 쓰세요. 더 나은 자동 형식화, 생성기로 되돌아가는 더 나은 오류 피드백 같은 것들이요.

인간 수학자가 여전히 정확성을 지키는 이유

어떤 검증기도 정리가 중요한지는 말해주지 못합니다. 문제 선택은 안목이고, 안목은 수십 년에 걸쳐 쌓인 사회적 기술입니다. 세미나, 심사 보고서, 어떤 질문이 문을 여는지와 어떤 질문이 막다른 길인지에 대한 느린 합의가 그렇습니다. 연구 커뮤니티가 벤더 발표에 보이는 회의는 단지 자기 영역을 지키려는 문지기 노릇이 아닙니다. 면역 체계이며, 면역 체계는 가끔 과잉 반응합니다. 반응이 부족하면 치명적이기 때문입니다.

그다음은 출처 문제입니다. 이 모델들은 커뮤니티 자신의 질문, 초안, 포럼 글로 학습되었고, 이는 칭찬받는 “발견”이 미래의 심사위원들이 쓴 것들의 재조합일 수 있다는 불편한 가능성을 제기합니다. 자기 도구와 경쟁하는 것에 대한 두려움은 편집증이 아니라 데이터 계보 문제입니다. 연구소가 계보를 보여줄 수 있을 때까지는 인간 심사위원이 여전히 제대로 작동하는 유일한 표절 탐지기입니다. 여기에 누가 검증에 초대되는지, 발표문에 누구 이름이 들어가는지, 편애에 대한 비난 같은 공적 인정(credit)의 정치를 더하면 인간의 관문을 없앨 수 없는 이유가 보입니다. 저명한 과학자 다섯 명을 골라 결과를 축복하게 하는 것은 인식론적 행위인 만큼이나 정치적 행위입니다.

리더보드를 연구 능력으로 읽고 싶은 사람들에게 한 가지 더 주의를 드립니다. 경쟁 대회의 금메달은 몇 시간 안에 풀리도록 설계된 문제에서의 성능을 측정합니다. 연구는 정반대의 분포입니다. 아무도 풀 수 있을지 모르기 때문에 선택된 문제들이죠. 소프트웨어 엔지니어링에서 벤치마크가 실제 업무의 대부분을 놓치는 이유와 같습니다. 지표는 다듬어진 문제에 보상을 주지, 지저분한 문제에 주지 않습니다. 올림피아드 문제를 완벽히 푸는 모델은 분명 실재하는 무언가를 보여준 것입니다. 하지만 판단력을 보여준 것은 아닙니다.

권고: 모델이 아니라 루프를 신뢰하라

제 입장을 분명히 말씀드리겠습니다. 추측 생성은 실재하고 유용하며 앞으로 더 나아질 것입니다. 하지만 검증되지 않은 추측 생성은 쓸모가 없고, 형식적 뒷받침이 없는 자연어 증명은 입증될 때까지 마케팅으로 취급해야 합니다. 결과를 믿어야 하는 순간이라면 증명 검사가 매번 이깁니다. 병목이 엄밀성이 아니라 상상력일 때는 생성이 이깁니다. 중요한 발표는 이 둘이 단단히 맞물려 있는 것들입니다.

따라서 모델은 에너지는 무한하지만 판단력은 없는 다작의 주니어 협업자로 다루세요. 모델이 건네는 모든 것은 논문에 들어가기 전에 증명 도구를 거쳐야 하고, 서론에 들어가기 전에는 안목 있는 사람을 거쳐야 합니다. 연구자라면 증명 도구 하나를 제대로 배우세요. 형식화가 병목이고, 그것을 다룰 수 있는 사람들이 곧 아주 바빠질 것입니다. 도구를 만든다면 데모가 아니라 루프를 만드세요. 그리고 다음 큰 발표가 나오면 보도자료는 건너뛰고 프리프린트를 열어 Lean 저장소가 있는지 확인하세요. 살아남는 주장은 이미 기계 검증을 거쳐 도착한 것들입니다.