AI 스타트업 Axiom, 수학계 미해결 난제 4개 연달아 증명

Executive Summary

• AI 스타트업 Axiom이 자체 개발한 수학 증명 AI 'AxiomProver'로 수년간 미해결 상태였던 4개의 수학 난제를 연달아 증명했다
• 대수기하학의 Chen-Gendron 추측을 비롯해 19세기 인도 수학자 라마누잔의 공식과 관련된 Fel 추측까지 완전 자동화 방식으로 해결했다
• 수학 전문 AI 시스템과 대규모 언어 모델을 결합한 이 기술은 사이버보안 등 상업적 응용 분야로도 확장될 전망이다

Background

수학자들은 수십 년간 복잡한 대수기하학 문제들과 씨름해왔다. 보스턴 대학의 Dawei Chen 교수와 Quentin Gendron은 2021년 미분(differentials) 관련 정리를 연구하던 중 정수론의 특이한 공식에 막혀 증명을 완성하지 못하고 추측으로만 발표해야 했다. Chen 교수는 최근 ChatGPT에 수시간 동안 프롬프트를 입력해봤지만 해결책을 찾지 못했다. 그러던 중 지난달 워싱턴 DC 수학 학회에서 버지니아 대학을 떠나 AI 스타트업 Axiom에 합류한 저명한 수학자 Ken Ono를 만났고, 다음날 아침 AxiomProver가 생성한 증명을 받아들게 됐다.

Impact & Implications

기술적 의미

AxiomProver는 단순한 대규모 언어 모델이 아니다. Lean이라는 수학 전용 형식 언어로 증명을 자체 검증할 수 있어, 기존 문헌 검색을 넘어 진정으로 새로운 해법을 개발할 수 있다. Chen-Gendron 추측의 경우 19세기에 처음 연구된 수론적 현상과의 연결고리를 AI가 스스로 발견했다. 하버드 경영대학원의 Scott Kominers 교수는 "완전 자동화된 방식으로 이런 문제를 풀고 즉시 검증까지 한 것도 놀랍지만, 생성된 수학의 우아함과 아름다움이 더욱 놀랍다"고 평가했다.

산업/시장 영향

Axiom CEO Carina Hong은 "수학은 현실의 시험장이자 샌드박스"라며 높은 상업적 가치를 지닌 활용 사례가 많다고 밝혔다. 특히 코드가 신뢰할 수 있고 안전함을 형식적으로 증명하는 방식의 사이버보안 소프트웨어 개발에 적용될 수 있다. 2024년 구글이 AlphaProof로 유사한 접근법을 시연한 바 있으나, Axiom은 더 발전된 기술을 적용했다고 주장한다.

향후 전망

Ono 교수는 AxiomProver가 수학자들의 연구를 돕는 것을 넘어 새로운 발견이 어떻게 이뤄지는지에 대한 근본적인 통찰을 제공할 것으로 기대한다. Chen 교수는 "계산기가 발명된 후에도 수학자들은 구구단을 잊지 않았다"며 "AI가 수학 연구의 지평을 더 풍요롭고 넓게 열어줄 지능형 파트너가 될 것"이라고 전망했다.

Key Data & Facts

Key Quote

"Even as someone who's been watching the evolution of AI math tools closely for years, and working with them myself, I find this pretty astounding. It's not just that AxiomProver managed to solve a problem like this fully automated, and instantly verified, which on its own is amazing, but also the elegance and beauty of the math it produced."
— Scott Kominers, 하버드 경영대학원 교수