수학적 컴퓨터 언어인 메타메쓰(Metamath) 사용 23건 채택
오픈AI 연구원 "인공지능이 증명한 식 처음으로 공식 채택"
인공지능 언어 모델 GPT-f가 발견한 수학 증명이 공식 수학 커뮤니티 메타매쓰(Metamath) 라이브러리에 채택됐다. 메타메쓰는 수학적 증거를 보관·검증·연구하는 언어 및 컴퓨터 프로그램.
GPT-f를 만든 오픈AI의 연구원 스태니스라스 포루(Stanislas Polu)와 일리야 수츠케버(Ilya Sutskever)는 "딥러닝 모델이 제출한 수학적 증명이 공식 수학 커뮤니티에 받아들여진 것은 이번이 처음"이라고 전했다.
GPT-f은 트랜스포머 기반의 자동 정리 증명 모델이다. 오픈AI의 GPT-2 및 GPT-3와 비슷한 트랜스포머를 사용한다. 트랜스포머는 구글이 2017년도에 발표한 신경망 모델. 자동 정리 증명은 주어진 정의나 논리를 증명하는 알고리즘이다.
포루 연구원에 따르면 GPT-f는 메타매쓰 라이브러리에서 56.22%의 증명 성공률을 보이며 새로운 SOTA(state-of-the-art, 현재 최고 수준) 결과를 달성했다. GPT-f 등장 전 SOTA 모델이었던 MetaGen-IL의 21.16%에 두배 이상 되는 수치다.
GPT-f는 다양한 크기의 데이터셋으로 사전훈련됐다. 그 중 가장 큰 모델은 36개의 층과 7억 7400만 개의 훈련 가능한 매개변수를 가지고 있다.
한편, GPT-f에 대한 세부적인 작동 방식 및 알고리즘은 두 연구원이 발표한 논문에서 확인할 수 있다. 해당 논문은 7일 (현지 시각) 미 코넬대가 운영하는 논문 서비스인 아카이브(https://arxiv.org/abs/2009.03393)사이트에 등록됐다.
[AI & Tech] 오픈AI, 10월부터 GPT3 API 유료로 배포
무단전재 및 재배포 금지
기사제보 및 보도자료 news@aitimes.com