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

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

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

.


[1] propositional logic (ncatlab.org)
[2] predicate logic (ncatlab.org)
[3] second-order logic (ncatlab.org)
[4] higher-order logic (ncatlab.org)
[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일

Mathcha : 브라우저 기반 수학문서 편집툴

일전에 이야기[1]한 LaTeX으로 수학 노트필기를 한다는 사람이 쓴 두 번째 글[2]을 쓴 것을 해커뉴스[3]에서 봤는데, 그림을 그릴 때 Inkscape[4]를 쓴다고 한다. 나는 쓸 줄 몰라서 답답하던데-_- 이걸 어떻게 그렇게 자유자재로 쓰는 건지 신박하네. ㅋㅋ

여하간 해커뉴스의 댓글[3] 중에서, Mathcha라는 브라우저 기반의 수학문서 편집툴 개발자가 댓글을 달았던데, LaTeX을 몰라도 자유자재로 수학문서를 작성할 수 있는 사이트인 모양이다. 홈페이지[5]에 있는 소개 영상[6]을 봤는데, 보니까 엄청 잘 만든 것 같다. 재생시간 3분 7초

오오 필기 입력으로 deTeXify도 지원하는구만. 대단하구만.

브라우저 기반이니까 파일을 들고 다니거나, OS에 의존적일 일은 없을 것 같다. 물론 LaTeX 소스를 직접 편집할 수도 있다.

브라우저 기반 문서편집이라 하니 일전에 본 CoCalc[7]가 생각나는데, 이쪽은 문서작업뿐만아니라 협력작업을 더 강조하는 툴 같다.

근데 내가 쓸 일이 있으려나-_- 나는 한/글 종속적이라서-_- ㅋㅋㅋ

.


[1] 내 백과사전 수학 수업시간 중에 노트필기를 LaTeX으로 하는 것이 가능한가? 2019년 3월 22일
[2] How I draw figures for my mathematical lecture notes using Inkscape (castel.dev)
[3] I draw figures for my mathematical lecture notes using Inkscape (hacker news)
[4] 내 백과사전 Inkscape – 벡터그래픽 툴 2011년 10월 6일
[5] https://www.mathcha.io
[6] Mathcha.io – Math Editor – Overview (youtube 3분 7초)
[7] 내 백과사전 CoCalc : 웹기반 토탈 수학 관리 플랫폼? 2018년 4월 18일

Mathpix : 수식 이미지를 LaTeX으로 자동변환하는 프로그램

Mathpix[1]라는 프로그램을 봤는데, 종이를 스캔한 수식 몇 개를 변환해 봤다. 초 신박하구만. ㅋㅋ 이런게 해커뉴스에 언급이 안 될 리가 없을 텐데 싶어서 검색해보니, 역시나 나와 있었다.[2] 나온지 꽤 된 프로그램 같은데 왜 여태 몰랐지????

홈페이지[1]에 따르면, 플랫폼으로 맥, 윈도우즈, 우분투만 지원한다고 한다.

ctrl-alt-m을 누르면 스크린 캡쳐를 시작하는데, 드래그로 수식영역을 지정하면 LaTeX로 변환해 준다.

근데 상당히 정확하다. 스캔된 수식이 약간 기울어 있어도 잘 된다. 왠지 틀릴만한 복잡한 수식을 찾아서 일부러 스캔해 봤다.

예를 들어 위와 같은 수식 (약간 기울어져 있다)을 드래그 하면

으로 인식하여 조금 오류가 있다. 뭐 이 정도 빡센 거는 이해해 줄 수 있다. ㅎㅎㅎ

일전에 노트필기를 LaTeX으로 하는 사람 이야기[3]가 생각나는데, Mathpix가 더 발전해서 걍 손으로 줄줄 쓰면 TeX화 되는 프로그램이 나왔으면 좋겠구만. ㅎㅎㅎ

.


[1] https://mathpix.com/
[2] Show HN: Convert screenshots of equations to LaTeX (hacker news)
[3] 내 백과사전 수학 수업시간 중에 노트필기를 LaTeX으로 하는 것이 가능한가? 2019년 3월 22일

Google DeepMind가 중학 수학시험에 떨어지다

futurism 기사[1]를 보니 구글 딥마인드의 인공지능이 영국의 중학 수학시험 문제 풀기에 도전했지만 낙제한 듯 하다. arXiv에도 올라와 있다.[2]

물론 수학 문제는 자연어로 주어지고, 문제를 바탕으로 인공지능이 추론해서 답을 도출하는 형태의 시험을 시도한 듯 하다. 인공지능 모델은 단순 LSTM과 Attentional LSTM과 Transformer model을 썼다고 한다. transformer model은 처음 듣는 용어인데, 이 동네는 자고 일어나면 새로운 용어가 생겨나니 미치겠구만-_-

내 생각으로는 자연어 처리가 잘 되면 자연스럽게 이런 문제도 풀릴 것 같은데, 여하간 일단 완전한 인간 수준의 자연어 처리가 어려워서 국지적 문제에 도전하는 듯 하다.

수학문제가 어떤가 싶어 봤는데, 논문에 16세 수준이라고 언급[1;p4]되어 있다. 근데 Appendix B와 D에 샘플 문제가 있는데, 영국 나이로 16세면 한국의 고등학생 같은데, 문제가 좀 너무 쉬운 수준 아닌가??? 일전에 영국의 중학수학 수준이 내려가고 있다는 이야기[3]를 들었는데, 진짠가 모르겠다.

뭐 자신의 논리적 추론을 스스로 설명도 못하는 애들이 숫자맞추기 게임만 열라게 해대는 한국의 변태적인 선행학습으로 인하여, 내 생각에 편향이 생긴 것일 수도 있다. ㅎㅎㅎ

.


[1] futurism Google’s Best AI Just Flunked a High School Math Test April 6th 2019
[2] David Saxton, et al. “Analysing Mathematical Reasoning Abilities of Neural Models”, (Submitted on 2 Apr 2019) arXiv:1904.01557 [cs.LG]
[3] 내 백과사전 영국의 중학교 수학은 쉬워지는가? 2012년 6월 24일

비트겐슈타인이 수학문제를 생각하며 하는 행위

-_-;;;;;;;;;;;;;;;;;;;;;;;

위 책을 검색해보니 슬라보예 지젝의 저서[1;p51]에 있는 내용이라고 한다. 검색해보니 역서[2]가 있던데, 이미 품절된지 오래 된 듯. 아놔 빨랑 품절걱정이 없는 전자책이 활성화 되어야 한다.

이걸 보니 일전에 수학조크[3]에서 구구단 이야기가 생각난다. 아무래도 비트겐슈타인 이야기가 와전된 게 아닐까 싶다. ㅋㅋㅋㅋㅋ

.


[1] How to Read Lacan (How to Read) Paperback – January 17, 2007 (amazon.com)
[2] HOW TO READ 라캉 슬라보예 지젝 (지은이),박정수 (옮긴이) 웅진지식하우스 2007-05-14 원제 : HOW TO READ Lacan (2005년)
[3] 내 백과사전 수학 조크 2011년 5월 29일

Matthew Weathers 선생의 만우절 수학 강의

Biola 대학 소속의 Matthew Weathers 선생[1]은 해마다 만우절이 되면 프로젝터를 이용한 재미있는 개그를 하는 듯 한데, 예전에 재미있게 본 기억이 있다. 올해도 만우절 기념 강의를 한 듯 한데, 유튜브 영상이 올라왔구만. 재생시간 2분 46초.

이런거 하나 준비하려면 타이밍에 맞추는 거 나름 연습해야 할 듯 한데, 재밌게 사시는 듯. ㅎㅎㅎ

그의 유튜브 채널[2]에서 예전에 했던 다른 만우절 강의도 볼 수 있음.

.


[1] Matthew Weathers (biola.edu)
[2] Matthew Weathers (youtube.com)

이 포스팅의 제목은 거짓말이다

매일 아침마다 알렉사[1]에게 おはよう라고 말하면, 그 날에 해당하는 역사속 사건이나 상식을 알려주는데, 오늘은 뭔가 흥미로운 이야기를 하는 듯 해서 열심히 들으니, 마지막에 만우절 뻥이었습니다-_- 라고 하는게 아닌가!!ㅋㅋㅋ 드디어 스마트 스피커도 구라를 치는 세상이 온 건가-_- ㅋㅋㅋㅋ

그래서 나도 만우절 기념으로 Liar paradox를 함 써 봤음. ㅋ 그나저나 수학기초론을 함 공부해보고 싶은데, 게을러서… -_-

이번 포스트는 내용이 원체 없으니 일전에 이야기했던 만우절 기념 가짜 증명[2]이나 우려먹어야 겠다-_-

.


[1] 내 백과사전 아마존 에코로 선풍기 음성 제어 ㅋㅋ 2018년 4월 7일
[2] 내 백과사전 만우절 기념 가짜 수학증명 2014년 4월 2일