중국 AI 모델, 3차원 기스 추측 증명 지원…린으로 수학적 검증

1995년 수학 문제가 새로운 이정표에 도달하다

1995년에 제기된 수학적 추측이 수학자들과 상하이 AI 연구소의 Intern-S2 모델의 협업으로 복소 차원 3까지 아우르는 증명을 얻었다. 이어 베이징대 연구팀은 논문의 주요 정리 네 가지를 린(Lean)으로 검증할 수 있는 증명으로 옮겼다. 린은 수학적 추론을 검증하도록 설계된 컴퓨터 시스템이다.

상하이 AI 연구소는 2026년 10월 15일 이 성과를 발표하며, 그레이트베이대 교수이자 연구소 방문학자인 쉬디성 교수가 이끈 연구팀에 공을 돌렸다. 연구 논문 「코차원 1 정칙 아노소프 미분동형사상」의 단독 저자는 스웨덴 왕립공과대(KTH)의 장제쑹이다.

이번 결과는 프랑스 수학자 에티엔 기스의 추측에서 코차원 1인 경우를 해결했으며, 복소 차원 3인 경우도 포함한다. 이 문제는 운동과 형태 사이의 흥미로운 관계를 다룬다. 특정한 종류의 혼돈스러운 운동을 뒷받침하는 공간이 그 자체로 고도로 질서 잡힌 수학적 구조를 가져야 하는지가 핵심이다.

Intern-S2는 연구자들과 거듭 의견을 주고받으며 아이디어와 논증을 발전시키는 데 도움을 줬다. 장제쑹은 AI 사용에 관한 선언에서 모든 수학적 내용을 독립적으로 검증했다고 밝혔다. 이번 협업은 기계의 탐색, 인간의 판단, 별도의 형식 검증 절차를 결합했다.

연구소는 이번 성과를 이 정도 수준의 수학 문제 해결에 중국 AI 모델이 활용된 첫 사례라고 설명했다. 구체적인 결과물은 분류 정리이며, 공개 프리프린트와 공개된 형식화 코드도 함께 나왔다.

증명이 말하는 운동과 형태

기스의 추측은 복소 동역학 분야에 속한다. 복소 동역학은 좌표가 복소수의 규칙을 따를 때 수학적 시스템이 어떻게 변하는지 연구한다. 복소수에는 두 개의 실수 성분이 있으므로 복소 차원 3은 국소적으로 실수 차원 6에 해당한다. 여기서 다루는 대상은 방 안에서 움직이는 일상적인 물체보다 훨씬 추상적이다.

아노소프 시스템은 늘림과 압축이 정밀하게 결합된 구조를 갖는다. 운동을 반복하면 어떤 방향은 수축하고 다른 방향은 팽창한다. 출발점이 서로 가까운 점들도 빠르게 멀어질 수 있어, 매 단계의 규칙은 정확한데도 혼돈스러운 거동이 나타난다.

형태를 늘이고 접는 과정을 반복하는 모습을 떠올리면 이해에 도움이 된다. 여기서 연구한 수학적 시스템은 훨씬 더 엄격한 조건을 따른다. 늘임과 수축이 균일한 조건을 만족해야 하고, 운동은 복소 좌표가 부여하는 구조를 보존해야 한다.

기스는 콤팩트 복소 다양체 위의 이런 시스템이 표준적인 대수적 묘사를 가져야 한다고 추측했다. 다양체란 전체 형태가 복잡하더라도 작은 근방에서는 단순하게 보이는 공간이다. 여기서 콤팩트성은 공간이 무한히 뻗어나가지 않게 하는 수학적 조건이다.

장제쑹의 정리에 따르면 콤팩트 연결 복소 다양체 위의 모든 코차원 1 정칙 아노소프 미분동형사상은 복소 토러스의 쌍곡적 자기동형사상과 쌍정칙 켤레다. 쉽게 말해, 복소 구조를 보존하는 가역 좌표 변환을 적용하면 그 운동은 매우 규칙적인 공간 위의 표준 대수 변환으로 바뀐다.

복소 토러스는 복소 공간에서 반복되는 격자의 원소만큼 차이가 나는 점들을 서로 동일시해 만들 수 있다. 이번 성과의 핵심은 복잡한 동역학이 이런 질서 정연한 기하학적 묘사를 강제한다는 점이다.

정확한 적용 범위가 중요한 이유

이 논문은 코차원 1인 경우를 다룬다. 이 시스템에서는 수축하는 부분이나 팽창하는 부분 가운데 하나의 복소 차원이 1이라는 뜻이다. 정리는 이 제한된 계열을 일반적으로 포괄하고, 복소 차원 3에서는 추측을 해결한다.

기스의 더 포괄적인 추측은 더 넓은 범위의 복소 다양체에 걸친 정칙 아노소프 시스템을 다루며, 복소 인프라-닐 다양체라고 불리는 공간 위의 표준 대수 모형으로 이들을 설명한다. 장제쑹의 결과는 이번 연구 대상인 경우에 특히 강한 결론을 제시한다. 즉, 복소 토러스와 쌍곡적 자기동형사상으로 설명할 수 있다는 것이다.

이 문제를 연구하는 수학자들에게 이번 정리는 미지의 공간과 운동을 규명하는 문제를 표준 모형을 연구하는 문제로 바꿔준다. 좌표 변환은 복소 기하를 보존하면서 원래 시스템과 그 모형을 연결한다.

쉬디성은 수년간 이 문제를 연구해 왔다. 그는 이전에 지도교수였던 필즈상 수상자 아르투르 아빌라와 함께 3차원인 경우를 연구했다. 이후 쉬와 장은 관련 부분 결과를 얻어 《유럽수학회지》에 발표했다. 이번 연구는 같은 수학적 질문을 꾸준히 탐구해 온 작업을 바탕으로 한다.

올림피아드 시험에서 연구 협력까지

Intern-S2의 역할에 앞서 2025년 중국 수학 올림피아드에서 Intern-S1이 성과를 냈다. 중국수학회 중등수학경시대회위원회는 그해 AI 시험을 도입해 중국 모델 세 종을 초청하고, 인간 참가자와 같은 시간 안에 문제를 풀도록 했다.

Intern-S1은 동일한 채점 기준에서 102점을 받아 참가 모델 세 종 가운데 1위를 차지했다. 금메달 기준점은 78점으로, Intern-S1의 점수는 기준보다 24점, 약 31% 높았다.

쉬는 이 모델 계열을 연구 수학에 활용할 가능성을 봤고, 상하이 AI 연구소는 경시 문제에서 미해결 문제로 적용 범위를 넓히려 했다. 양측의 협업은 2026년 초 시작됐으며, 모델의 작업과 연구자들과의 의견 교환을 체계화하는 하니스(Harness)라는 소프트웨어 시스템 구축도 포함됐다.

주요 진행 과정은 다음과 같다:

• 1995년: 에티엔 기스가 추측을 제기했다.
• 2025년: Intern-S1이 중국 수학 올림피아드 AI 시험에서 102점을 받았다.
• 2026년 초: 쉬와 상하이 AI 연구소가 모델 훈련 협업을 시작했다.
• 2026년 3월: 쉬가 연구소 방문학자로 부임했다.
• 2026년 8월: 내부 개발한 Intern-S2 버전과 지원 시스템이 집중적인 수학 탐구에 활용되는 단계에 도달했다.
• 9월 29일: 장제쑹의 논문이 arXiv에 게시됐고, 10월 13일 수정본이 올라왔다.
• 2026년 10월 15일: 성과가 공식 발표됐다.

수학자들은 AI를 어떻게 이끌었나

Intern-S2가 처음 문제를 탐색해 작성한 유도 보고서는 약 400쪽에 달했다. 쉬는 자신의 옛 제자이자 KTH 박사후연구원인 장제쑹에게 방문학자로 합류해 달라고 요청했다. 장은 박사과정 때부터 기스의 추측을 연구해 왔다.

쉬와 장은 모델이 제안한 내용을 검토하고, 가능성이 높은 출발점을 찾아 이후 탐색을 이끌 피드백을 제공했다. 기계는 추론의 갈래를 탐색하고 논증을 생성했으며, 수학자들은 더 연구할 방향을 결정하고 최종 증명을 구성하는 데 힘을 보탰다.

연구소는 추론을 이어간 과정을 일곱 차례의 배치로 설명한다. 이 과정에서 모델의 문제 그래프는 노드 15개에서 389개로 늘었고, 누적 출력은 약 1,000쪽에 이르렀으며 제안된 접근법도 수십 가지 나왔다.

문제 그래프는 더 작은 수학적 과제와 그 연결 관계를 나타낸 지도다. 한 노드는 중간 명제를, 다른 노드는 그 명제를 증명하는 데 필요한 결과를 나타낼 수 있다. 보고된 증가는 시스템이 문제를 얼마나 광범위하게 나누고 탐색했는지를 보여준다.

장제쑹의 AI 사용 선언은 최종 수학적 결과에 대한 책임을 직접 설명한다. 내부 버전의 Intern-S2가 여러 차례 대화를 통해 아이디어와 논증을 발전시키는 데 도움을 줬으며, 장은 수학적 내용을 독립적으로 검증했다. 논문은 쉬와 지속적으로 토론한 데 대해서도 감사를 표한다.

지원 소프트웨어가 기여한 점

상하이 AI 연구소는 긴 추론 과정과 반복적인 인간 피드백을 관리하도록 설계한 소프트웨어와 모델을 결합했다. 이 시스템은 어려운 질문을 작은 과제로 나누고, 여러 방향을 탐색한 뒤 연구자들이 평가할 결과를 돌려줄 수 있었다.

훈련 방식은 폭넓은 과학 지식에 연구 수학을 겨냥한 자료를 더했다. 여기에는 수학 논문에서 가져온 어려운 문제와 제안된 해법을 검증하는 방법이 포함됐다. 연구소는 검증 가능한 보상을 활용한 강화학습도 설명한다. 이는 성공적이고 검증 가능한 추론이 훈련 신호로 쓰일 수 있다는 뜻이다.

이후 연구자들은 지원 시스템을 통해 얻은 경험을 바탕으로 모델 자체를 개선했다. 실제 목표는 중간 결과를 추적하고 새로운 논증이 발전하는 과정에서 오류를 바로잡으면서 긴 연구 과정 내내 유의미한 진전을 이어가는 것이었다.

연구소는 수학적 추론에 초점을 둔 평가인 IMO-Proof와 AdvancedMathBench의 결과도 언급했다. 기스 프로젝트에서 시스템 작동 방식을 가장 상세히 보여주는 근거는 방대한 유도 과정, 전문가 피드백, 완성된 논문, 이어진 형식 검증의 연속 과정이다.

베이징대는 증명을 어떻게 검증했나

둥빈과 류뤄촨이 이끄는 베이징대 연구팀은 SHEAF 프레임워크를 사용해 장제쑹의 논문에 나온 주요 정리 네 가지를 모두 형식화했다. 논증의 토대가 된 기스의 결과도 작업에 포함됐다.

형식화란 수학적 정의와 가정, 추론을 컴퓨터가 검증할 수 있는 언어로 옮기는 작업이다. 일반적인 논문에서는 훈련된 독자가 익숙한 단계를 채워 넣을 수 있다. 린에서는 이런 단계를 정밀한 명제와 허용된 논리 연산으로 표현해야 한다.

연구팀의 장제둥과 우빈은 최대 100개의 AI 에이전트가 병렬로 작동한 가운데 작업에 약 5일이 걸렸다고 밝혔다. 그 결과 린 코드 약 55만 줄이 만들어졌다. 전문가들은 형식화된 명제가 논문의 주요 정리가 뜻하는 수학적 내용과 일치하는지도 확인했다.

SHEAF는 정의와 명제, 의존 관계를 방향성 그래프로 구성해 작업을 관리했다. 이에 따라 여러 에이전트가 서로 연결된 부분을 나눠 맡는 동안, 연구팀은 어떤 명제가 증명됐고 어떤 명제에 추가 작업이 필요한지 추적할 수 있었다.

형식화 작업은 최종 논증을 옮기는 데 그치지 않았다. 동역학 분야의 일부 보조 결과가 기존 수학 형식화 라이브러리에 없었다. 연구팀은 그 토대를 마련하거나 이미 이용 가능한 결과를 활용할 방법을 찾아야 했고, 이후 각각의 결과를 연결해 완전한 증명으로 구성했다.

논문은 arXiv 프리프린트로 공개됐으며, 형식화 코드는 GitHub에 공개됐다. 발표에서는 학술지 게재나 동료 심사 결과를 언급하지 않았다.

두 단계가 함께 필요한 이유

Intern-S2와 SHEAF는 서로 다른 역할을 맡았다. 앞의 시스템은 수학적 아이디어와 논증을 찾는 과정을 지원했다. 뒤의 시스템은 린이 검증할 수 있는 형식 증명을 구성하는 데 도움을 줬다. 수학자들은 탐색을 이끌고, 도출된 수학적 내용을 검토했으며, 형식화된 명제가 의도한 정리를 제대로 담았는지 평가했다.

작업 규모를 보면 역할 분담이 구체적으로 드러난다. 탐색 과정에서 나온 약 1,000쪽의 출력물이 연구 논문으로 이어졌고, 이후 검증 과정에서는 형식 코드 약 55만 줄이 생성됐다. 각 단계는 서로 다른 과업에 맞춰 작업 결과를 다른 형태로 바꿨다.

앞으로 연구자들은 공개 논문에서 수학적 논증을 확인하고, 공개 코드를 통해 형식 증명의 구조를 살펴볼 수 있다. 형식화 과정에서 추가된 정의와 결과도 같은 분야 후속 연구의 출발점이 될 수 있다.

다음 단계는 재사용 가능한 검증 모듈

상하이 AI 연구소는 이 작업 흐름을 수학 검증 모듈로 묶어 과학적 발견 플랫폼인 Intern Duanyan에 탑재할 계획이다. 이후 연구에서도 모델 탐색, 전문가 피드백, 형식 검증의 결합을 재사용할 수 있도록 하는 것이 목표다.

연구소는 이번 프로젝트를 통해 발전시킨 추론 역량을 관련 수학적 구조가 있는 다른 학문 분야에도 적용할 계획이다. 제안된 순환 구조는 연구 문제를 해결하고, 유용한 방법을 재사용 가능한 소프트웨어로 만든 뒤, 이를 다른 연구에 적용하는 것이다.

쉬에게 이번 성과는 그레이트베이대와 상하이 AI 연구소, KTH, 베이징대의 협업을 통해 오랫동안 이어온 연구 관심을 확장한 결과다. 더 넓은 수학계에는 새로운 분류 결과와 함께 AI가 인간의 지휘 아래 연구에 참여한 상세한 사례를 제공한다.

핵심 내용

• 새 증명은 기스 추측의 코차원 1인 경우를 해결했으며, 복소 차원 3도 포함한다.
• 연구 논문의 단독 저자는 장제쑹이며, 모든 수학적 내용을 독립적으로 검증했다고 밝혔다.
• 쉬디성과 장제쑹은 반복적인 탐색과 피드백을 통해 Intern-S2를 이끌었다.
• 모델의 문제 그래프는 노드 15개에서 389개로 늘었고, 유도 과정은 약 1,000쪽에 달했다.
• 베이징대의 SHEAF 프레임워크는 린으로 주요 정리 네 가지와 보조 결과를 형식화하는 데 도움을 줬다.
• 검증 작업은 약 5일이 걸렸으며 코드 약 55만 줄이 생성된 것으로 알려졌다.
• 연구소는 작업 흐름을 재사용 가능한 수학 검증 모듈로 만들 계획이다.