타오의 machine assisted proofs 강연을 보고

유투브 알고리즘이 불러온 필즈상 수상자인 테렌스 타오의

Machine assisted proofs 강연!

강연에 사용된 슬라이드는 테렌스 타오의 웹페이지, 여기 (몇몇의 슬라이드는 빠지고 추가 된 듯 싶다) 또 강연의 원고격인 소논문은 여기 에서 받아 볼 수 있다.

컴퓨터가 수학적 증명에 처음 도움을 주었다고 생각하는 문제는 4색 문제가 있다. 엄청 옛날에 스팀잇에 관련 글을 올린 적이 있다. 예전 글 : [수학] 컴퓨터와 수학 // 4색문제와 케플러의 추측.

같은 글에 케플러 추측 문제를 이야기 했고, 이 작업은 2014년에 끝나 증명이 되었고, 여기에 대한 저자 Hales의 회고는 여기; arXiv:2402.08032에서 볼 수 있다. 핵심을 이야기 하자면 Flyspeck(Formal Proof of the Kepler conjecture) 프로젝트를 통해 non-linear inequalities(Hales는 케플러 추측 문제를 planar graph 문제로 바꾸었고, 컴퓨터를 통해 가능한 tame planar graphs를 세고 대응되는 non-linear inequalities들을 찾아내 증명했다.) 들을 확인했고 이를 통해 증명 할 수 있었다.

뭐 예전에 글을 올렸듯이 4색문제나 케플러 문제는 그래프 문제로 회귀되고 그래프 문제들은 조합의 경우의 수가 많아도 유한하기에, 컴퓨터를 이용해서 해당 모든 그래프에 대해 conjecture에 대응되는 조건들을 보이면 되는거니 (이건 그 당시 나도 문헌조사를 통해 알고 있었던 내용) 그럴수 있다고 봤는데, 타오의 소논문과 강연을 통해 추가적으로 알게 된 내용에는 knot theory에 대응되는 다이어그램들을 neural networks를 통해 학습 시켰다는 내용들과 특히 Lean Copilot 과 같은 AI tool과 증명법이 놀라웠다.

홈페이지의 40장 짜리 슬라이드에는 빠져 있는 내용으로, 강연을 들어보면 LLM등의 AI 들의 학습 능력의 평가척도로 IMO 문제 풀이를 하는 AI 들이 있는데, Alphaproof, AlphaGeometry, AlphaZero 이들의 정답률이 꽤나 높다는 것이고 이러한 AI들에 적당한 프롬프트를 사용하여 교과서 처럼 사용하자는 방법론 까지 제시하며 교육과 연구에 LLM들을 잘 사용하자는 이야기는, 정말 AI가 앞으로의 연구 풍토를 꽤나 급진적으로 바꿀수도 있겠다는 생각을 하게 한다.

이번에 GPT 5.0도 나올 예정이고, 올해 정말 많은 LLM 모델들이 나와 강인공지능 혹은 범용인공지능이라 불리는 AGI의 시대가 초래할거다 라고 말을 하는데, 이제 인공지능을 얼마나 잘 활용해서 사용할 수 있느냐가 개인의 능력을, 효율을 최대화하는데 척도가 될 듯 싶어, 기대가 되기도 하지만, 한편으로 인간의 지능의 역할이 줄어드는 것 같아 씁쓸하기도 하다.