인공지능을 이용한 정리 증명: GPT-f

지난번 일반적 대화 인공지능 GPT-3에 대한 글을 두 개나 포스팅 한 적 있다[1,2].이번에는 해당 모델 (GPT)를 이용해 수학 정리 증명을 하는 인공지능을 만들었다는 소식이 들려온다[3,4]! 논문[5]을 아주아주 간단히 훑어보고 정리해본다 ㅋ

당연하게도/아쉽게도 논문에서 생성하는 증명은 우리가 생각하는 수학 증명을 완성하는 프로그램은 아니다. 논문의 목표는 컴퓨터가 이해하고 검증할 수 있는 증명을 작성하는 프로그램으로, metamath [6]라는 환경의, 특히 set.mm이라는 라이브러리를 기반으로 학습하고 증명을 작성한 듯 하다.

set.mm의 장점은 현대수학에 가까운 올림피아드 문제나 학부수준의 문제들이 formal language로 정리되어 있다고. 한 예를 들면, 다음과 같은 IMO 1972 B2번 (현재의 5번에 해당하는듯)을 생각할 수 있다.

실함수 f,g:\mathbb R\rightarrow \mathbb Rf(x+y)+f(x-y)=2f(x)g(y)를 만족한다고 하자.
이 때, f가 0함수가 아니면서 |f(x)|\le 1을 모든 x에 대해 만족한다면 모든 x에 대해 |g(x)|\le 1도 성립함을 증명하여라.

증명은 아주 간단하다. |g(y)|>1인 y가 하나 존재한다고 가정하고, |f|의 상한 M을 잡으면

2M\ge |f(x+y)+f(x-y)| = 2|g(y)||f(x)|>2|f(x)|

에서 |f(x)|<M이 모든 x에 대해 성립하므로 모순. 하지만 이걸 metamath의 언어로 옮기면, 링크에 따르면 문제는

가 되고, 풀이의 앞부분 약간은 아래와 같고, 111줄까지 이어진다. -_-…… 확신은 안가지만, 상위 페이지를 보면 같은 항목에 정리가 수십개 있는데 이게 다 필요할지도 모른다 -_-.

여튼 논문의 주장으로는 인공지능을 이용해서 기존의 증명들보다 짧은 증명을 찾아서 라이브러리에 기여를 했고, 이게 딥러닝 기반 정리 증명으로 해당 증명 학회에 기여를 한 최초의 사례라고. DeepHOL등의 사례를 Zariski님 페에지 [7]에서 본 적이 있는데, 이건 딱히 기여를 한게 없나? 전혀 모르겠다 -_-

논문의 주장을 조금만 살펴보면,

  • arXiv등의 수학적 데이터를 사전학습(pre-training)하는게 일반적인 텍스트를 학습하는 것보다 결과를 훨씬 좋게 만든다고 한다. 아니 arXiv등의 텍스트가 formal proof를 하는데 향상을 시킨다니 -_- 믿기지 않는군.
  • 모델의 사이즈가 결과와 양의 상관관계를 갖는다.
  • 스스로 생성한 증명을 반복해서 학습함으로 결과가 점점 나아진다는 듯 하다.
  • n자리수 연산이나 Ring 연산등을 잘 학습한 듯 하다. 다음은 논문에 제시된 생성된 Ring 항등식의 예시들.
  • 23개의 알려진 증명을 더 짧게 만들었다고 한다. 논문 내에 Metamath 커뮤니티의 찬사를 넣어놓았는데, 논문에 이런걸 넣기도 하나 ㅋㅋㅋ

[1] GPT-3 자연어 처리 모델, Pseudorandom Things
[2] GPT-3는 생각하지 않는다, Pseudorandom Things
[3] 인공지능 GPT-f가 생성한 수학 증명, 공식 수학커뮤니티에서 채택, AI타임즈
[4] OpenAI ‘GPT-f’ Delivers SOTA Performance in Automated Mathematical Theorem Proving, Synced
[5] Generative Language Modeling for Automated Theorem Proving, arxiv
[6] http://us.metamath.org/index.html
[7] DeepHOL : 딥러닝을 이용한 수학 명제 자동증명 시스템, 내 백과사전

답글 남기기

아래 항목을 채우거나 오른쪽 아이콘 중 하나를 클릭하여 로그 인 하세요:

WordPress.com 로고

WordPress.com의 계정을 사용하여 댓글을 남깁니다. 로그아웃 /  변경 )

Google photo

Google의 계정을 사용하여 댓글을 남깁니다. 로그아웃 /  변경 )

Twitter 사진

Twitter의 계정을 사용하여 댓글을 남깁니다. 로그아웃 /  변경 )

Facebook 사진

Facebook의 계정을 사용하여 댓글을 남깁니다. 로그아웃 /  변경 )

%s에 연결하는 중