Deep learning을 이용한 상미분방정식 해결 능력이 상용 소프트웨어를 능가하다

MIT tech기사[1]에서 페이스북 소속 연구원들이 발표한 아주 흥미로운 논문[2] 이야기를 들었다.

Mathematica라든지 Matlab 같은 CAS를 많이들 쓰실텐데, Deep learning을 이용하여 상미분방정식을 풀도록 만드니, 그런 상용 소프트웨어들을 능가했다는 흥미로운 주장이었다. 헐?

임의의 적분문제를 생성하는 여러가지 방법이 있는 모양인데, 본인은 처음 들었다. 논문[2]에서는 Forward generation (FWD), Backward generation (BWD), Backward generation with integration by parts (IBP)과 같은 세 가지 방식을 이용했다고 한다.

이렇게 임의로 생성된 적분문제가 주어질 때, 자연어 처리에서 쓰이는 Branching 방식을 수식에 적용하여 트리구조를 만들고, beam search 알고리즘으로 트리를 탐색하고, sequence-to-sequence models (seq2seq)과 같은 자연어 처리를 썼다고 한다. 일전에 seq2seq로 선형문자 B 해독을 시도[3]하던데 은근 잘 나가는 모델인 듯??? 뭐 사실 나도 다 모르는 용어들이지만, 서당개 삼 년이면 풍월을 읊는다고, 나도 블로그개-_- 삼 년을 하니 이름들은 많이 들어봤다.

여하간 BWD로 생성한 미분방정식 500문제를 30초 컷으로 풀게 했더니, 정확도의 결과가 다음과 같았다고 한다.[2;p9] 논문 뒤쪽에 부록 D[2;p23]에 Mathematica를 30초 이상 돌려도 정확도 향상이 거의 없음을 알 수 있는 표도 나오니까, 30초 컷이 나름 합리적인 듯.

헐 근데 내가 좋아하는 Maple의 퍼포먼스가 Mathematica보다 많이 낮네. ㅎㅎㅎ maple은 서로 까고 있을 때[4]가 아닌 듯 하다. ㅋㅋㅋ

뒤쪽으로 Mathematica와 Matlab은 못 푸는데, 자기네 모델로는 풀리는 미분방정식 문제의 사례가 나와 있는데, 다음과 같은 문제들이 제시되어 있다.

혹시나 싶어서, 똑같은 문제를 Maple로도 풀어봤는데, 역시 못 풀었다. 젠장-_-

뭐 여하간 자연어 처리의 여러 기법을 수식을 처리하는데 적용한다는 발상도 재미있지만, 그게 상용 소프트웨어를 능가할 정도니 더욱 인상적인 듯 하다. 일전에 본 Hierarchical Poincaré Embeddings[5] 같은 것도 Facebook AI Research 소속 연구원들이 발표했던데, 페북이 이런 연구는 많이 하는 듯?

.


[1] MIT tech review Facebook has a neural network that can do advanced math Dec 17, 2019
[2] Deep Learning for Symbolic Mathematics, Guillaume Lample, François Charton, (Submitted on 2 Dec 2019) arXiv:1912.01412 [cs.SC]
[3] 내 백과사전 Neural machine translation으로 고대 문자 해독하기 2019년 12월 14일
[4] 내 백과사전 Maple과 Mathematica의 상호비방 2014년 4월 4일
[5] 내 백과사전 음악 추천 알고리즘 : Hierarchical Poincaré Embeddings 2019년 8월 5일

Neural machine translation으로 고대 문자 해독하기

선형문자 B는 고대 그리스의 미케네 문명에서 쓰였던 문자인데, 오랫동안 해독되지 않다가 요절한 천재였던 Michael Ventris에 의해 해독되었다. 선형문자 B의 해독과정을 소개하는 John Chadwick 선생의 책[1]을 예전에 본 적이 있는데, 본인은 고고학과 언어학에 모두 무지해서 좀 읽다가 접었다. 읽기 좀 빡세다-_- 사이먼 싱 선생의 [2]에도 이에 관해 약간의 설명이 있다. 비교적 발굴량이 많았던 선형문자 B와는 달리, 상대적으로 발굴량이 적은 선형문자 A는 아직도 거의 해독되지 않고 있다고 한다.

MIT tech review에서 고대 문자를 sequence-to-sequence (seq2seq) model이나 biredictional-LSTM(아마 bidirectional-LSTM의 오타인 듯) 같은 기계 번역 기법을 동원하여 해독하는 연구[3]를 소개하는 기사[4]를 봤다. 아 근데 지난 7월 기사라서 좀 오래 됐네-_-

근데 논문[3] 내용을 대충보니, 기계번역을 시작하는 시점에서 Linear B가 고대 그리스어라는 걸 이미 확정하고 시작하는 것 같은데, 그 ‘고대 그리스어’라는 정보가 단순해보여도, Ventris가 해독하기 이전까지 고고학자들 사이에서 굉장히 논란인 부분이었다.[1] 과학사를 보면 과학발전이 다 그렇듯이, 지금 당연해 보이는게 과거에도 당연한 건 아닌 케이스가 초 많다. 미지의 문자가 무슨 언어인지 자체가 엄청난 힌트가 되는데, 이걸 베이스로 깔고 기계번역하는게 어떤 도움이 될런지 의문이다. 논문[3]의 저자 세 사람의 과거 논문을 대충보니 인공지능 쪽의 연구자이고, 고고학자는 없는 듯 한데, 화려한 기계번역 기법들이 동원되긴 했지만, 고고학적 난점은 좀 무시된 듯 하다.

샹폴리옹의 고대 히에로글리프 해독[5]이나, 고대 마야어 해독[6]을 보면 알 수 있듯이, 고문자 해독은 언어학과 더불어 당대 문화를 기반으로 추론된 고고학 지식을 전반적으로 완전히 통합해야 겨우 나오는 결과인데, 단순히 문자들간의 비교로 얼마나 유의미한 결과를 얻을 수 있을지는 의문이다. 일전에 Voynich manuscript를 해독하려는 시도[7]도 그렇듯이, 기계번역을 연구하는 사람들이 고고학에 대해 좀 순진한 환상(?)같은 걸 가지고 있는 듯 하다. ㅎ

.


[1] 선형문자 B의 세계 – 문자로 살펴본 고대 그리스 문명의 발자취 존 채드윅 (지은이),김형주,김운한 (옮긴이) 사람과책 2012-04-13
[2] 비밀의 언어 – 암호의 역사와 과학 사이먼 싱 (지은이),이현경 (옮긴이) 인사이트 2015-12-06 원제 : The Code Book: The Science of Secrecy from Ancient Egypt to Quantum Cryptography (1000년)
[3] Neural Decipherment via Minimum-Cost Flow: from Ugaritic to Linear B, Jiaming Luo, Yuan Cao, Regina Barzilay (Submitted on 16 Jun 2019) arXiv:1906.06718 [cs.CL]
[4] MIT tech review Machine learning has been used to automatically translate long-lost languages Jul 1, 2019
[5] 내 백과사전 [서평] 문자를 향한 열정 : 세계 최초로 로제타석을 해독한 샹폴리옹 이야기 2012년 7월 14일
[6] 내 백과사전 고대 마야어 해독 과정 2014년 9월 12일
[7] 내 백과사전 자연어 처리로 Voynich manuscript를 해독하기 2018년 9월 13일

Deep Learning을 이용한 쿠즈시지 OCR

페이스북의 ‘월간 자연어 처리’ 페이지에서 흥미로운 이야기[1]를 들었다.

쿠즈시지(崩し字)라는 일본 전통 필기체가 있는 줄 처음 알았다. ㅎㅎㅎ 천년 이상 많은 고문서에서 쓰였던 모양인데, 현대 문자와 모양이 많이 달라서인지 훈련을 받지 않은 현대 일본인들도 읽을 수 없다고 한다. 일본 고전문학 전공하는 사람들이 많이 공부하는 듯. KuLA라고 하는 쿠즈시지 학습을 돕기위한 앱[2,3]도 있다. 오사카 대학에서 만든 앱이라고 한다.[4]

여하간 이 쿠즈시지 문자를 Deep Learning을 이용하여 OCR을 하려는 시도[5]가 있는 듯 하다. KuroNet이라고 이름도 붙인 듯. ㅎㅎ

검색해보니 이미 웹상에서 KuroNet을 시험해 볼 수 있는 서비스[6]가 있는 듯 하다. 회원등록을 해야 하는 듯. 근데 나에게 쿠즈시지 문서가 없어서 시험해 볼 수는 없구만-_- 그 밖에 detexify[7]처럼 필기인식을 지원하는 사이트[8]도 있는 듯 하다. 이 사이트[8]는 AI를 이용한다고는 돼 있는데, 어느 알고리즘을 쓰는지는 명확하게 밝히지 않고 있다. 개인이 운영한다고 한다.

여하간 KuroNet의 정확도가 꽤나 궁금해지는데, 논문[5]을 대충 봤다. F1 score라는 말이 나오던데, 이게 뭔 말인지 처음 알았다-_- 어느 블로그[9]에서 잘 설명해주고 있다. 여하간 높으면 좋은 것 같구만-_- 논문의 table 1에 책 별로 F1 score가 나와 있던데, 대부분의 책이 0.7~0.8 근처다. 애매하게 정확한데-_- 이걸 일일이 사람이 검토해야 된다면, 그냥 사람이 하는 것에 비해 효율이 좋지는 않을 듯 하다.

내 생각에는, 일전에 키보드 치는 소리로 패스워드를 빼내는 해킹을 하는 연구[10]가 생각나는데, 거기처럼 빈도분석법 + 철자교정 콤보를 쓰면 정확도가 꽤 많이 올라가지 않을까 싶기도 하다.

일반적인 상용 OCR 성능도 그럭저럭 쓸만하던데, 내 짐작으로는 그냥 텍스트만 있는 문서면 아마 F1 score가 0.7이상은 될 것 같다. 꼭 쿠즈시지가 아니더라도 상용 OCR과 딥 러닝을 활용한 OCR 사이의 성능격차가 유의미해야 이런 접근법이 의미가 있지 않을까 싶기도 하다.

.


[1] https://www.facebook.com/monthly.nlp/videos/474009179914214/
[2] くずし字学習支援アプリKuLA (app store)
[3] くずし字学習支援アプリKuLA (google playstore)
[4] Learning Japanese ancient characters with your smartphone (resou.osaka-u.ac.jp)
[5] “KuroNet: Pre-Modern Japanese Kuzushiji Character Recognition with Deep Learning”, Tarin Clanuwat, Alex Lamb, Asanobu Kitamoto, arXiv:1910.09433 [cs.CV]
[6] KuroNetくずし字認識サービス (mp.ex.nii.ac.jp)
[7] Detexify (detexify.kirelabs.org)
[8] AI 手書きくずし字検索 (ai-kuzushiji.net)
[9] 분류모델 (Classification)의 성능 평가 (bcho.tistory.com)
[10] “Keyboard acoustic emanations revisited.” L. Zhuang, F. Zhou, and J. D. Tygar. ACM Transactions on Information and Systems Security, 13:1, October 2009, pp 3:1-3:26 doi 10.1145/1609956.1609959

수학 증명 언어 Lean과 Buzzard 선생이 꿈꾸는 수학의 미래

해커뉴스[1]를 보니, 일전에 이야기한 수학 매거진 chalkdust[2]에 Kevin Buzzard 선생이 기고한 글[3]이 올라와 있던데, 아무래도 본인의 글이다보니 일전에 본 기사[4]보다는 좀 더 자세한 내용이 있다. waffiic님의 말 대로, 진짜 Buzzard 선생은 ZFC에서 와일즈-테일러 정리까지의 검증을 원하는 듯 하다. 참고로 Buzzard 선생이 블로그[5]를 하는 줄은 몰랐다. 팔로우해 볼만할 듯 하다. ㅎㅎㅎ

기고된 글[3]은 전반적으로 마이크로소프트에서 개발한 수학증명을 위한 프로그래밍 언어인 Lean을 소개하는 글 같은데, 재미있는 내용은 글의 뒷부분에 있다. 부르바키의 책 Topologie Générale의 챕터 2, 3을 게임으로 만들었다는 언급이 있던데, 이 게임 함 해볼 수 있나??? 싶어서 검색을 해봤는데, 공개되지는 않은 듯?? 상대성 이론 게임[6]보다 재미있으려나? ㅋㅋㅋ 나는 염불보다 잿밥에 더 관심이 있다. ㅋㅋ

(a+b)^3 = a^3 + 3a^2 b + 3ab^2 +b^3이 ring의 axiom으로부터 유도하는게 깜짝 놀랄정도로 어렵다고 나와 있던데, 과정은 귀찮아도 어렵지는 않을 듯 한데 좀 이상한 언급이다.

Peter Scholze 선생이 만들었다는 Perfectoid space 이야기는 처음 들었는데, 새로운 structure를 갖는 space인 줄은 알겠는데, 왜 중요한지는 잘 모르겠지만 뭔가 신박한 듯? -_-

유튜브에 Buzzard 선생의 강연[7]이 있던데, 길어서 다 보지는 않았지만 그가 상상하는 수학의 미래가 어떤 건지 대충 감이 온다. 진짜 옛날에 공상과학 영화에서 나오는 일상의 문제가 자동화 되어 해결되는 그런 머신스러운 세상의 수학버전인 듯 한 느낌이다. 어쩌면 삼위일체의 세상[8]이 올런지도 모르지. ㅎㅎ

.


2019.11.1
아참 그러고보니 lean을 이용하여 IMO 문제를 인공지능으로 해결해보려는 시도가 있는 듯.[9] 이거 이야기 하려는 거 깜빡했네. ㅋㅋ

.


[1] Can Computers Prove Theorems? (hacker news)
[2] 내 백과사전 수학적 호기심을 위한 매거진 : chalkdust 2017년 12월 16일
[3] chalkdust Can computers prove theorems? 23 October 2019
[4] 내 백과사전 참이라고 알려진 많은 수학 정리들이 거짓으로 판정될 가능성에 대해 2019년 9월 29일
[5] https://xenaproject.wordpress.com
[6] 내 백과사전 느린 광속 게임 A Slower Speed of Light 2012년 11월 8일
[7] The Future of Mathematics? (youtube 1시간 14분 47초)
[8] 내 백과사전 계산 삼위일체론 computational trinitarianism 2019년 6월 6일
[9] IMO Grand Challenge (imo-grand-challenge.github.io)

음악 추천 알고리즘 : Hierarchical Poincaré Embeddings

해커 뉴스[1]에서 Hierarchical Poincaré Embeddings를 이용하여 음악 추천을 하는 이야기를 봤는데, 뭔 소리인지는 잘 모르겠지만-_- 기록차 남겨둠. 나는 이렇게 이해했는데, 아무래도 이 포스트는 오류를 포함하고 있을 가능성이 매우 높다. ㅋㅋ

일전에 Matrix factorization 이야기[2]를 했는데, 뭐 잘 모르지만 꽤나 광범위하게 쓰이는 추천 알고리즘 같다.

기계 학습을 시킬 때 학습대상의 특징을 뽑아내서 분류하고 학습하는 방식을 많이 쓰는 모양인데, 이 때 neighbor를 판정하는 방법으로 그냥 Euclidean space를 많이 쓰는 듯 하다. Matrix factorization도 오류 판정을 root mean squared를 일반적으로 쓰는 듯 한데, 이것도 일종의 Euclidean이라 봐야 할 듯 하다.

그런데 페이스북 소속 연구원 2명이 계층적 구조를 가진 데이터를 학습할 때 Euclidean 대신 Poincaré ball을 쓰면 더 나은 결과가 될 듯 하다는 주장을 하는 듯한-_- 글[3]을 대충 봤다. 아무래도 실제 회사들의 데이터들에서는 Zipf’s law처럼 값들이 한쪽에 쏠려있는 경우도 많으니까 그런 듯?

iHeartRadio라는 인터넷 라디오 방송 플랫폼이 있다고 한다. 나는 처음 들었는데 나름 꽤 큰 회사인 듯? 이 iHeartRadio 소속 4명의 연구원들이 Poincaré ball이 낫다는 주장[3]을 보고, 음악 추천에 시험해 본 듯 하다.[4] 음악의 메타데이터가 ‘장르-아티스트-곡명’ 과 같은 계층적 데이터라서 적용가능한 듯?

예를 들어 Matrix factorization으로 추천 목록을 만들면

The Shins – September
Lilly Hiatt – Jesus Would’ve Let Me Pick
METRIK – We Got It
Matrix & Futurebound – Magnetic Eyes
Dads – Dads (feat. Berried Alive & Lucas Mann)
Ugly Casanova – Spilled Milk Factory
Cursive – Ouroboros
Reggie and the Full Effect – Your Girlfriends
Hey Mercedes – What You’re Up Against
The Blood Brothers – Laser Life

와 같은 곡들이 추천되고, Poincaré 모델로 추천하면

The Strokes – Taken for a Fool
Arctic Monkeys – Brianstorm
The Strokes – 12:51
The Fratellis – Tell Me A Lie
Kings of Leon – Crawl
The Strokes – Is This It
Franz Ferdinand – Ulysses
Cage the Elephant – Shake Me Down (Unpeeled)
Death Cab for Cutie – Stay Young, Go Dancing
Kings of Leon – Notion

와 같은 곡들이 추천된다고 한다. 딱 봐도 완전 판이한 결과가 나온다. 근데 아는 아티스트가 하나도 없네-_- 요새는 맨날 아이돌 마스터 음악만 들어서…-_-

여하간 iHeartRadio에서는 사용자를 두 그룹으로 나누어 한 쪽은 푸앵카레 모델에 기반한 음악을 추천하고(treatment 그룹), 다른 한 쪽은 기존의 행렬 인수분해 기법에 기반한 음악을 추천하였더니(control 그룹), 평균 음악을 듣는 시간이 다음과 같게 나왔다고 한다.[4;p5]

헐.. 여러모로 월등히 우월하네. 현재 iHeartRadio에서는 푸앵카레 모델에 기반하여 디폴트 플레이리스트 생성기가 작동된다고 한다.

Matrix factorization을 이용한 학습 추천 시스템이 나름 꽤 널리 쓰인다고 들었는데, 산업의 종류에 따라서는 Poincaré model로 학습해서 추천하는 걸로 빠르게 바뀌지 않을까 싶은 생각도 든다. ㅎㅎ

.


[1] Music Recommendations in Hyperbolic Space (hacker news)
[2] 내 백과사전 영화 추천 알고리즘 : Matrix factorization 2019년 8월 4일
[3] “Poincaré Embeddings for Learning Hierarchical Representations”, Maximilian Nickel, Douwe Kiela arXiv:1705.08039 [cs.AI]
[4] “Music Recommendations in Hyperbolic Space: An Application of Empirical Bayes and Hierarchical Poincaré Embeddings”, Tim Schmeier, Sam Garrett, Joseph Chisari, Brett Vintch arXiv:1907.12378 [cs.IR]

node.js로 자작 스마트 스피커 만들기

스마트 스피커로 음악을 좀 듣고 싶은데, 본인이 듣는 음악의 절대다수는 국내에서 발매되지 않는다. 시판되는 상용 스마트 스피커들은 스트리밍 판매수익 때문에, 애석하게도 개인이 가지고 있는 mp3파일을 재생하는 기능이 없다. (물론 블루투스 스피커로 쓰면 되긴 된다.) 내가 말하는 음악을 재생해주는 스피커를 만들 수 없을까 궁리를 좀 해봤다.

일전에 만든 스마트 거울[1]은 크롬에서 https 사이트가 아니면 마이크 인식이 안 되도록 보안 업데이트를 하는 바람에 annyang이 더 이상 작동하지 않아 음성인식이 되지 않았다.

일전에 메이커스 매거진 부록으로 라즈베리 파이로 만든 스마트 스피커[2]를 어떻게 써먹어 볼 수 없을까 싶었는데, 본인이 node.js를 전혀 할 줄 모르기 때문에 어떻게 손을 댈 수가 없었다. ㅋㅋ 그래도 산 게 왠지 아깝구만 젠장.

뭐 여하간 어찌 되겠지 싶어서, node.js에 대해 검색을 열라게 해 봤다. 진짜 구글링을 일억 번은 한 듯-_-

그래서 어째저째 작동하는 물건을 만들었다. stt와 tts 부분은 일단 KT 서버를 활용한다. 일단 음성을 텍스트화한 후에는 특정 키워드가 들어있으면 그에 해당하는 정보를 쏴 주고, 없으면 KT의 대화서버로 보내서 나온 결과를 쏴 주도록 코드를 작성했다. 근데 node.js에 대해 아는 게 없으니 너무 멘땅에 헤딩 식으로 코딩했다. 이것 때문에 3일이 그냥 날라갔구만-_-

재생시간 1분 21초.

와 요거 만드는데 그 수많은 고생을 하다니-_- 아직 음악 재생 부분은 구현도 못했고, 코드는 100줄 남짓인데 하도 코드 수정을 많이해서 들여쓰기도 엉망이고 주석도 거의 없다-_- 어쨌든 음성인식 결과를 웹브라우저에 쏴 줄 수도 있으니 이런저런 이미지나 다양한 효과는 가능할 듯 하다. 참고로 서버의 데이터를 클라이언트의 웹브라우저에 출력하는 방법은 SSE라는 걸 사용했는데, 이런 게 있는 줄 처음 알았네. ㅎㅎ 어느 친절한 분이 설명[3]을 잘 해 두었으니 참고 바람.

참고로 hotword인 ‘기가지니’는 네 글자인데, 너무 길어서 ‘지니야’로 하니까 자꾸 아이패드의 시리가 반응한다-_- 본인은 아이패드의 siri와 네이버 wave[4]로 mBox[5]를 음성제어하고 있기 때문에 ‘기가지니’를 선택할 수 밖에 없었다.

근데 하드웨어가 안 좋은건지 몰라도, 음성인식률이 너무 떨어져서 실사용은 어려울 것 같다. 아 이걸로 음악 좀 듣고 싶은데, 아무래도 어려울 듯.

.


[1] 내 백과사전 음성인식 스마트 거울 만들기 2016년 11월 2일
[2] 내 백과사전 메이커스 매거진 부록 AI Maker Kit​ 2018년 8월 12일
[3] [웹개발] SSE ( Server-Sent Events) 란 무엇인가 (hamait.tistory.com)
[4] 내 백과사전 네이버 wave 사용 소감 2018년 9월 8일
[5] 내 백과사전 mBox : 음성으로 적외선 리모컨 신호 제어 2018년 12월 8일

한국어 번역 방해기

숙박업자가 숙박 리뷰에 나쁜 평을 삭제하기 때문에, 외국 숙박 리뷰에서 번역기를 회피하는 한국어 사용자 전용 리뷰를 남기는 사람이 있었다.[1,2,3] 이거 제일 처음에 누가 생각한건지 하여튼 잔머리 하나는 끝내주는구만. ㅋㅋ

어떤 사람이 한국어 번역 방해기[4]를 만든 걸 봤는데, 이런 작업을 자동화 해주는 사이트다. 근데 시험삼아 ‘한구거 벉엮 방햬긔’를 구글 번역기로 돌려봤더니[5] ‘Korean translation jammer’라고 정확하게 번역 되어 나온다!!! 구글 번역기 진짜 대단하구만. ㅋㅋㅋ 이거보다 더 높은 레벨의 jammer filter를 사용해야 정상번역이 안 된다.

일전에 본 1픽셀 방해를 하거나[6]나 방안의 코끼리[7]를 두어 이미지 인식 방해를 하는 것처럼, 이것도 문장 인식 방해라는 점에서 일종의 인공지능 fooling이라 생각해도 좋을 듯 하다. 일전에 의료 영상에 악의적 에러를 포함시켜, 인공지능의 오진을 유도하는 공격법에 대한 연구[8,9]를 들은 적이 있는데, 이런 종류의 jammer를 만들고 그것을 회피하는 등의 창과 방패싸움은 끝이 없을 듯 하다.

.


2019.5.13
“한글 번역 방해기”를 소개합니다. (bomdol.tistory.com)

.


2019.7.18

단어우월효과는 한국어에만 있는 현상은 아니라고 함.

.


[1] 조선일보 ‘한국인 전용’ 여행 후기 번역기 돌려보니? 2017.05.22 21:44
[2] 외국 숙박 후기에서 보는 한글의 위대함.jpg (todayhumor.co.kr)
[3] 인사이트 ‘구글 번역기’는 해석 못하지만 우리는 알아듣는 한글의 위대함 2018.10.08 19:23
[4] 한국어 번역 방해기 (xeno.work)
[5] 한구거 벉엮 방햬긔 google 번역 결과 (translate.google.com)
[6] 내 백과사전 1픽셀로 deep neural network를 무력화 하기 2017년 10월 31일
[7] “The Elephant in the Room”, Amir Rosenfeld, Richard Zemel, John K. Tsotsos, (Submitted on 9 Aug 2018) arXiv:1808.03305 [cs.CV]
[8] https://www.facebook.com/yoonsup.choi/posts/2744397698933510
[9] Samuel G. Finlayson, et al. “Adversarial attacks on medical machine learning”, Science 22 Mar 2019: Vol. 363, Issue 6433, pp. 1287-1289, DOI: 10.1126/science.aaw4399

DeepHOL : 딥러닝을 이용한 수학 명제 자동증명 시스템

수리논리학에 대해 아는 건 하나도 없지만-_- 여하간 대충 검색해서 찾아본 내용을 기록함. ㅋㅋㅋㅋ 본인은 초 문외한이므로 그냥 개소리라고 생각하시라. ㅎㅎ

십 몇 년 전에 처음 Automated theorem proving에 대한 개념을 처음 들었을 때, 너무 놀라서 의자에서 떨어지는 줄 알았다-_- 진짜다-_- 위키피디아를 대충 보니 나름 역사가 있는 분야인 듯. ㅎㅎㅎ 증명을 찾아주는 종류의 소프트웨어가 있고, 찾은 증명이 맞는지 확인해주는 종류의 소프트웨어가 있는 듯 하다. 본인은 어느 쪽도 써 본적은 없다.

0차 논리는 변수없이 참/거짓을 판정하는 서술을 말한다. 참/거짓이 변하면 안된다. 명제 논리(propositional logic)라고도 부른다. “지금 비가 내린다” 같은 거다. 고등학교에서 배우는 ‘명제’라고 생각하면 될 듯 하다. 수리논리학의 위키피디아라 할 수 있는 nLab의 설명[1]도 참고하기 바란다.

1차 논리는 술부에 Quantifier로 한정된 변수를 쓰는 것이 허용가능한 논리를 말한다. 위키피디아의 설명에 따르면 1차 논리에서는 ‘소크라테스는 사람이다(Socrates is a man)’는 ‘x는 소크라테스이면서 x는 사람인 x가 존재한다(there exists x such that x is Socrates and x is a man)’로 표현 가능하다. 이게 무슨 개소리지…-_- 여하간 1차 논리에서 참인 모든 명제는 증명 가능하다는 괴델의 완전성 정리가 성립한다. 1차 논리는 술어 논리(predicate logic)라고도 부른다. 마찬가지로 nLab의 설명[2]을 참고바람.

2차 논리는 별 제한없는 논리 같은데, Second-order logic이랑 Higher-order logic이 뭐가 다른지는 잘 모르겠다. nLab의 설명[3,4]을 보니 2차 논리 이후로도 논리의 차수를 확장할 수 있는 듯 한데, 2차 이상의 논리들을 가리키는 듯. 여기서는 참이라도 증명이 안될 수도 있다는 괴델의 불완전성 정리가 성립한다.

위키피디아를 보니 증명이 맞는지 확인해주는 Proof assistant 소프트웨어 중에서 HOL Light라는 게 있다고 한다. 나는 이름을 들어본게 Coq 밖에 없었는데, 위키를 보니 엄청나게 종류가 많은 것 같다. 위키피디아에는 없지만 경북대학교 소속[5]의 정주희 교수가 proofmood[6]라는 소프트웨어를 만들고 있다고 한다. 근데 1차 논리밖에 안 되는 듯?

여하간 구글소속 연구자들이 이 HOL Light를 기반으로 deep learning과 supervised Learning을 이용하여 명제의 증명까지 검색하는 DeepHOL이라는 걸 만든 모양이다.[7] 사실 수학적 명제의 증명이든 바둑[8]이든 간에 데이터를 디지털화만 잘 해 두면, 나머지는 주어진 규칙(연역, 삼단논법 등)을 만족하는 거대한 search space 내에서 올바른 경로를 탐색하는 기법이라서, 둘 다 구글이 잘 할 듯해 보인다. ㅎㅎ

Proof assistant로 증명을 확인한 가장 유명한 사례가 Kepler conjecture인데, 일전에 책[9]을 읽은 적이 있다. 이 논문[7]에서도 언급이 되어 있는데, 아무래도 증명과정의 디지털화가 잘 돼 있어서 선택한 듯 하다.

내가 보기에는 인공지능이 의사를 완전 대체할 것이라는 주장보다는, 인공지능으로 사진판독을 수월하게 하는 등등 의사의 잡무를 줄여 도움을 준다는 주장이 더 설득력이 있어 보인다. 뭐 여하간 이 결과가 수학계에 어떤 영향을 줄런지는 잘 모르겠지만-_- 마찬가지로 인공지능이 수학자를 대체한다기 보다는, 수학자의 업무량을 줄여주지 않을까 하는 망상이 든다. 그런 의미에서 Horgan 선생이 희망을 갖기[10]에는 아직 이르지 않을까 싶다. ㅎㅎㅎㅎ

.


2019.8.4
The Mizar proof system (2017) (hacker news)

.


[1] propositional logic (nLab)
[2] predicate logic (nLab)
[3] second-order logic (nLab)
[4] higher-order logic (nLab)
[5] Joohee Jeong (datamood.com)
[6] proofmood (datamood.com)
[7] “HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version)”, Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, Stewart Wilcox (Submitted on 5 Apr 2019) arXiv:1904.03241 [cs.LO]
[8] 내 백과사전 컴퓨터 바둑개발 현황 2017년 1월 3일
[9] 내 백과사전 [서평] 케플러의 추측 2013년 8월 19일
[10] 내 백과사전 수학적 증명의 종말과 Horgan 선생의 변명 2019년 3월 17일