30년 된 추측, 중국 모델, 그리고 기계 검증된 증명

30년 된 추측, 중국 모델, 그리고 기계 검증된 증명

10월 15일, Shanghai AI Laboratory(상하이 인공지능 연구소)는 한 연구팀이 Ghys 추측의 3차원 경우를 증명했다고 발표했다. 이는 1995년부터 미해결로 남아 있던 동역학계의 공개 문제다. 연구는 연구소 자체 모델인 Intern-S2로 진행되었고, 완성된 증명은 Peking University(베이징대학교) 팀이 Lean에서 형식적으로 검증했다.

중요한 것은 어려운 문제 하나가 풀렸다는 점만이 아니다. 이번 발표가 어떤 숫자가 아니라 과정을 중심으로 구성되었다는 점이다. 모델이 유도를 만들어내고, 연구자들이 어느 공격 경로에 주의를 쏟을지 결정하고, 증명 보조기가 모든 단계를 인증한다. 이 조합은 업계가 2년 동안 약속해 온 것이며, 이제 논문까지 붙었다.

이 추측이 묻는 것

Étienne Ghys가 이 문제를 제기한 것은 1995년이다. 대략적으로 말해, 카오스 동역학계의 거동이 그 기하학적 분류를 결정할 수 있는지, 다시 말해 운동이 그것이 일어나는 공간의 모양을 알려줄 수 있는지를 묻는다.

풀린 것은 일반적인 문제가 아니다. 팀이 증명한 것은 여차원 1 경우, 즉 3차원 설정이며, 이는 30년 동안 미해결로 남아 있었다. 이 구분은 주장을 정직하게 읽는 데 중요하다. 추측 전체는 여전히 더 넓지만, 지금까지 아무도 돌파하지 못한 특정 경우는 이제 정리되었다.

첫 시도에서 400페이지가 나왔다

협업의 작동 방식은 결과보다 더 흥미롭다. 인간과 AI 연구가 분 단위로 실제로 어떤 모습인지 보여주기 때문이다.

Intern-S2가 이 문제를 처음 탐색했을 때 약 400페이지 분량의 유도 보고서를 만들어냈다. 그것은 답이 아니다. 후보 추론의 더미이며, 어떤 것은 유용하고 어떤 것은 그렇지 않다. 알려진 것을 회상하게 하는 대신 진정으로 미해결인 문제를 생각하도록 모델에 요청할 때 나오는 바로 그 형태의 출력이다.

거기서부터 작업은 7차례의 연속 추론을 거쳤다. 문제 그래프, 즉 하위 명제와 그것들이 서로 어떻게 의존하는지의 지도는 15개 노드에서 389개로 커졌다. 누적된 출력은 약 1000페이지에 달했고 수십 가지 서로 다른 접근을 포함했다. 각 단계에서 수학자들은 모델이 스스로 할 수 없는 일을 했다. 제안을 살펴보고, 어떤 돌파구가 유망한지 판단하고, 다음 차례를 이끌었다.

연구소의 방문 학자이자 Greater Bay University 교수인 Xu Disheng과, 박사 과정 때부터 이 추측을 추적해 온 박사후 연구원 Zhang Jiesong이 그 판단을 제공했다. Zhang의 논문은 9월 29일 arXiv에 게시되었고 10월 13일 개정되었다. 단독 저자 논문이며 AI 사용 선언이 붙어 있다. 모델이 여러 차례 대화를 통해 아이디어와 논증 발전을 도왔고, 그는 수학적 부분을 독립적으로 검증했다는 내용이다.

이것을 단순한 이야기 이상으로 만드는 부분

AI가 수학을 풀었다는 주장은 값싸다. 이번에 무게가 실리는 이유는 증명이 형식화되었다는 점이다.

Bin Dong과 Ruochuan Liu가 이끄는 Peking University 팀은 자체 SHEAF 프레임워크를 사용해 네 가지 주요 정리와, 논증이 의존하는 Ghys의 보조적 결과를 모두 형식화했다. 형식화란 정의, 가정, 추론을 컴퓨터가 검사할 수 있는 언어로 번역하는 것을 뜻하며, 작성자의 논증 모든 단계를 훈련된 독자가 채우도록 남겨두지 않고 명시적으로 적어야 한다.

이 작업에는 약 5일이 걸렸고 최대 100개의 에이전트가 병렬로 일했으며 약 55만 줄의 Lean 코드를 만들어냈다. Lean은 대화형 정리 증명기다. 누가 얼마나 확신하는지는 관심이 없다. 논리를 검사하고 증명을 받아들이거나 받아들이지 않을 뿐이다.

SHEAF는 작업을 정의, 명제, 의존 관계로 이루어진 방향 그래프로 조직해 서로 다른 에이전트가 연결된 조각을 맡을 수 있게 했고, 팀이 어느 진술에 증명이 있고 어느 것이 아직 필요한지 추적할 수 있게 했다. 이는 진정으로 새로운 종류의 분업이며, 이 프레임워크는 기존 동역학계 형식 라이브러리의 빈틈도 메워야 했다. 이 증명에 필요한 도구가 당시에는 아예 없었기 때문이다.

인간과 모델, 서로 다른 일

연구소가 설명한 이 분업은 액면 그대로 받아들일 가치가 있다. 어느 쪽에도 듣기 좋은 버전이 아니기 때문이다.

모델은 문헌을 훑고, 명제를 조각으로 나누고, 증명 분기를 병렬로 탐색하고, 논리 단계를 검사하고, 수많은 아이디어를 빠르게 시험했다. 인간은 방향을 정하고, 어떤 접근이 추구할 가치가 있는지 판단하고, 다음 차례의 노력을 어디에 쓸지 결정하는 판단을 내렸다.

두 절반은 서로 닮지 않았다. 모델의 기여는 규모와 지구력이다. 수십 개의 막다른 길을 기억에 담고도 낙담하지 않는다. 인간의 기여는 안목이며, 이는 100페이지의 그럴듯한 추론을 보고 어떤 세 문단이 중요한지 아는 능력이다.

중국 언론이 크게 다룬 일화도 붙어 있다. 국내 모델이 풀었다는 소식을 듣고 동역학계 전문가 한 명이 호기심에 같은 문제를 GPT-6에 던졌는데 도달하지 못했다고 한다. 좁게 읽으면 한 문제에 대한 두 시스템의 비교일 뿐이라 별로 증명하는 것이 없다. 경쟁 구도에 대한 신호로 읽으면 투자를 움직이는 종류의 세부다.

형식 검증이 판돈을 바꾸는 이유

지난 2년 대부분 동안 AI 지원 수학의 병목은 후보 논증의 생성이 아니었다. 모델은 그럴듯한 추론을 잘 만들어낸다. 병목은 그중 무엇이 옳은지 아는 것이었다. 증명 검사는 느리고, 전문가가 필요하며, 병렬화가 잘 되지 않기 때문이다.

Lean은 이것을 뒤집는다. 어떤 진술이 형식화되고 나면 검증은 저렴하고 빠르며, 신뢰할 수 있다. 사회적인 것이 아니라 기계적이기 때문이다. 55만 줄이 비싼 부분이고, 팀과 100개의 에이전트가 5일 만에 그것을 만들어낼 수 있었다는 사실이 여기서 진짜 진보다. 생성 쪽 병목이 이미 느슨했던 것처럼 검증 쪽 병목도 느슨해지고 있을 수 있음을 시사한다.

연구소는 이 워크플로를 자체 과학 발견 플랫폼에서 재사용 가능한 수학 검증 모듈로 패키징해 모델, 에이전트, 데이터, 실험 장비를 연결하겠다고 밝혔다. 또한 Wuhan University(우한대학교) 팀이 이 플랫폼을 사용해 전기화학 합성의 개발 주기를 5년에서 10년에서 1년에서 2년으로 단축한 이전 결과도 언급했다.

여기서 무엇을 얻을 것인가

정직한 요약은 이렇다. 이것은 진짜 결과이고 진짜 증명을 동반하며, 그것을 만들어낸 워크플로는 여전히 매우 사람에 의존적이다. 전문가의 7차례 조종은 모델이 혼자 달리는 것이 아니다. AI 사용 선언이 붙은 단독 저자 논문은 모델이 공을 주장하는 것이 아니다.

달라진 것은 루프가 이제 닫힌다는 점이다. 모델은 아무도 풀지 못한 문제에서 의미를 가질 만큼의 추론을 만들어낼 수 있고, 인간은 그것을 이끌 수 있으며, 증명 보조기는 누구도 요약을 믿을 필요 없이 결과를 인증할 수 있다. 이것은 파이프라인이지 데모가 아니다. 그리고 능력을 실천으로 바꾸는 것은 파이프라인이다.

다음 질문은 이것이 형식화가 애초에 가능한 경우를 넘어 일반화되는지다. 기하와 동역학에는 기계 검사에 맞는 구조가 얼마간 있다. 과학의 나머지 대부분에는 그것이 없다. 그리고 AI가 연구 조수로서의 약속을 실제로 시험받는 곳은 생물학, 재료, 의학 같은 더 지저분한 영역이다. Ghys의 결과는 이 도구가 작동할 수 있다고 말한다. 얼마나 자주인지는 아직 말하지 않는다.