페이스북의 이미지 메타데이터 추적

페이스북의 사용자 추적은 악명이 높은데, 심지어 어카운트가 없는 사람들까지도 추적하고 있다고 해서 화제가 된 적[1]이 있었다. 이건 아마 쿠키를 추적한 듯 하다.

다른 사례로 언제부터인지 페북에 url을 링크하면 그 url 뒷부분에 fbclid 값을 자동으로 추가하던데, 이를 통해 링크가 어떻게 퍼지고 사람들이 링크를 어떻게 소비하는지 과정을 쉽게 추적할 수 있게 된 것 같다. 물론 본 블로그에서 제공하는 모든 링크들에는 fbclid가 제거되어 있다. ㅎㅎㅎ

오늘 해커 뉴스[2]를 보니 페이스북에 업로드한 이미지에는 페이스북에서 특별히 추적할 수 있는 메타데이터를 자동으로 삽입한다고 하는 트윗[3]이 언급된 것을 봤다. 와 페이스북 이 쉐이들 쫌 똑똑한 것 같다. ㅎㅎㅎ 이미지의 메타데이터 부분에 FBMD로 시작하는 문자 데이터열이 삽입되는 듯 하다.

4년전의 stack overflow 글[4]이 있는 걸 보면 이걸 시작한지는 상당히 오래된 듯. 이 글[4]에서 이미지 메타데이터를 볼 수 있는 Jeffrey’s Image Metadata Viewer라는 사이트[5]를 소개해 놓았던데, 본인도 예전에 받은 페북 이미지를 업로드해서 확인해보니, 역시나 FBMD로 시작하는 메타데이터 문자열이 들어있었다.

일전에 중국의 빅브라더 이야기[6]도 했지만, 원래 기술 대기업들은 사용자의 모든 데이터를 원한다. 요새 뜨는 기술들 중에 안구 추적을 연구하는 종류가 있다고 하던데, 아마 페북 등의 대기업들은 웹서핑 도중에 눈동자가 어디로 돌아가는지 실시간 추적하는데도 관심이 있을 듯. 이를 통해 사람들의 행동양식과 생활패턴을 추적하고, 어느 상황에서 지름신을 영접하고-_- 어느 상황에서 지불에 대한 저항을 갖는지에 대한 추적이 가능할 것 같다.

뭐 어디까지나 내 상상이지만, 각 개인별로 무슨 상황에서 뭘 보면 지갑을 여는지에 대한 궁극의 맞춤 설정 같은게 실현되면, 저축같은 건 아마 점점 더 하기 힘들 듯. ㅎㅎㅎㅎ

여하간 나날이 발전하는 페북의 잔머리에는 언제나 혀를 내두른다. 얼마전에는 Libra라는 걸 만들어서 세계 은행시스템을 통째로 몽땅 건너뛰고 개인-개인 간의 금융거래가 가능한 범세계적 플랫폼을 구축하려는 야심도 선보이던데, 이것 때문에 파월 의장님께서 좀 불편하신듯-_-[7] 앞으로 페북이 세계를 어떻게 바꿀지 흥미진진하다. ㅎㅎㅎ

.


[1] 로이터 Facebook fuels broad privacy debate by tracking non-users APRIL 15, 2018 / 8:04 PM
[2] Facebook is embedding tracking data inside the photos you download (hacker news)
[3] https://twitter.com/oasace/status/1149181539000864769
[4] IPTC metadata automatically added to uploaded images on Facebook (stackoverflow.com)
[5] Jeffrey’s Image Metadata Viewer (exif.regex.info)
[6] 내 백과사전 중국의 신용등급 문화와 빅브라더 2016년 12월 3일
[7] 로이터 Fed chief calls for Facebook to halt Libra project until concerns addressed JULY 10, 2019 / 11:58 PM

[서평] 실리콘밸리의 잘나가는 변호사 레비 씨, 스티브 잡스의 골칫덩이 픽사에 뛰어들다!

실리콘밸리의 잘나가는 변호사 레비 씨, 스티브 잡스의 골칫덩이 픽사에 뛰어들다!
로렌스 레비 (지은이),강유리 (옮긴이) 클레마지크 2017-06-14 원제 : To Pixar and Beyond (2016년)

.


이 책은 저자인 Lawrence Levy씨가 픽사가 무명이던 시절에 CFO로 영입되면서, 픽사가 성공하는 과정을 지켜본 자신의 경험담을 개략적으로 서술한 책이다. 과거 David A. Price의 ‘픽사 이야기'[1]를 읽은 적이 있는데, 그 책은 픽사의 탄생부터 전반적인 3D 애니메이션 기술사를 훑는 책이라면, 이 책은 재무와 경영적 관점에서 저자가 자신의 경험을 서술한 책이라 좀 다른 관점에서 흥미롭게 볼 수 있다.

저자는 처음 픽사를 보았을 때의 인상과 초창기 픽사가 처한 다양한 어려움에 대해 서술하면서 시작하는데, 객관적으로 봤을 때 당시에는 아무리 봐도 절망적인 상태였는 듯 하다. 지나고 봐서야 히트작이 연이어 나왔으니 그의 선택이 좋게 끝났지만, 나 같으면 도저히 픽사에 합류할 결정을 하지 못했을 듯 하다. ㅎㅎ

책 전반적으로 저자가 애니메이션 산업의 특성을 이해하려고 노력하고, 여러모로 계약을 진행하거나, 사람들 사이를 중재하거나, 사업 방향에 대해 모색하는 등 자신이 겪은 난항들에 대해 회고하는 내용으로 되어 있다.

책 제목에 잡스 이름이 있긴 하지만, 사실 잡스는 픽사가 어려울 때 꾸준하게 (투덜대면서-_-) 투자해 준 공로뿐이라 할 수 있을지도 모른다. 다만 일전에 월터 아이작슨잡스 전기[2]에서도 봤듯이 잡스의 면면을 볼 수 있는 일화도 약간 있다. 예를 들어 잡스는 자신의 견해를 고집할 때도 많지만 상대가 프로라고 인정되면 믿고 맡기는 이야기가 전기[2]에 나오는데, 투자자의 스토리에 대한 간섭이 일반화된 산업에서, 픽사 내부의 창작적 결정에 대해 독립성을 유지하게 해 준다.(p256) 이런 것들도 다 지나고나면 쉬워 보여도 당대에는 절대 쉽지 않은 결정이었을 것이라 본다. 어쨌건 잡스는 기술 산업과 엔터테인먼트 산업에 모두 걸친 사람으로서, 훗날 애플이 음악 등의 컨텐츠 사업으로 진출하는데 나름 장점이 되었을 것이다.

p279에 디즈니가 픽사를 인수하는 것이 RJR 내비스코 인수 이래로 두 번째로 큰 인수합병이라는 언급이 있는데, 이에 관해서 유명한 [3]이 있다. 이 책[3]이 엄청 재밌으니 일독을 권한다. ㅎㅎㅎ

저자는 픽사에서 10년 이상 일을 했다고 하는데, 책의 2/3 정도 분량은 픽사에 합류한 후 2년 정도의 기간에 할당하고 있다. 아무래도 픽사 초창기에 가장 위험했고 다이내믹한 기간이라 그런 듯 하다.

원제가 ‘To Pixar and Beyond: My Unlikely Journey with Steve Jobs to Make Entertainment History’라고 하는데, 원제보다는 역서 제목이 조금 더 적절한 듯 하여 마음에 든다. ㅎㅎ

텍스트의 분량이 약간 있긴 하지만, 전반적으로 평이한 내용이라 술술 읽힌다. 집중하면 한 나절에 완독할 수 있을 듯 하다.

.


[1] 내 백과사전 [서평] 픽사 이야기 PIXAR TOUCH : 시대를 뒤흔든 창조산업의 산실, 픽사의 끝없는 도전과 성공 2011년 5월 26일
[2] 내 백과사전 [서평] 스티브 잡스 2011년 11월 21일
[3] 내 백과사전 [서평] 문앞의 야만인들 : RJR내비스코의 몰락 2011년 5월 3일

라즈베리 파이를 어떻게 활용하십니까?

얼마전에 라즈베리 파이4가 판매시작 된 모양이다.[1] 스펙이 꽤 올라간 듯 한데, 하나 사고 싶지만 본인은 라즈베리 파이를 너무 많이 사 놔서 ㅋㅋㅋ 안 쓰는 게 몇 개 남아도는 마당에 또 사기는 좀 그렇구만. ㅎㅎㅎ

해커뉴스[2]에서 라즈베리 파이를 어떻게 활용하는가에 대한 이야기가 꽤 화제던데, 세상에 똑똑한 사람들이 많다. 재밌는 사례 중에, 몬트리올에 사는 어떤 사람이 버스 gps를 받아서, 창밖쪽으로 27인치 모니터를 달아서 버스 도착 예정시간을 보여주는 공공 서비스를 제공하는 사례가 있었다. 이건 뭐 한국에서는 이미 대도시 버스 정류장마다 버스 도착 패널이 달려있으니, 그리 적용할만데가 많지 않을 듯 하다.

식물에 자동으로 물을 주고, 식물 영상을 유튜브에 자동 업로드를 해서 식물관찰을 원격으로 하는 사람도 있던데, 이거 원거리에서 소규모 농장 하는 사람들은 나름 유용할 듯. ㅎㅎ

홈 오토메이션으로 쓰는 사람도 있고, VPN이나 옛날 머신의 와이파이 수신기로 쓰는 사람도 있는 듯. 세상에 똑똑한 사람 많다. ㅎㅎ 뭐 이걸로 NASA 해킹하는 사람[3]도 있더만. ㅋ

많은 사람들이 여러 개를 사서 각기 여러 용도로 쓰고 있던데, 본인도 몇 개를 돌리고 있다. 한 개는 스마트 거울[4]인데, 음성인식은 이제 안 되지만, 장중에는 코스피와 내가 홀딩하고 있는 회사의 주요뉴스들 타이틀이 거울에 디스플레이 되고, 장 마감 이후에는 일기예보가 디스플레이 되도록 만들었다. 여태까지 만든 것들 중에 이게 제일 유용하다. ㅎㅎㅎ

다른 하나는 오렌지 파이 제로[5]인데, ftp 및 웹서버로 쓰고 있어서 원격으로 간단한 기록이나 북마크 및 파일 전송/저장에 쓰고 있다. 사무실에 설치해 놨는데-_- 크기가 원체 작으니 아무도 존재를 눈치채지 못하고 있다. ㅋㅋㅋㅋ 이것도 상당히 유용함.

또 다른 하나는 집에 samba 및 토렌트 서버[6]를 설치한 것데, 망가져도 상관없는 계륵같은 저장장치들을 몽땅 합쳐서 대용량 디스크로 쓰고 있다.

라즈베리 파이 제로에 prota pi를 깔아서 마이크로봇 제어[7]에 쓰고 있다. 사정상 WOL을 쓰지 못하는 컴퓨터를 원격부팅할 때 쓰고 있음. 근데 prota pi는 서버가 죽을 때가 너무 많아서 불편하다.

일전에 구입한 메이커스의 스마트 스피커[8]는 node js 코딩 연습으로 쓰고 있었는데, 요새는 귀찮아서 걍 꺼 놓고 있다-_-

.


[1] Raspberry Pi 4 on sale now from $35 (raspberrypi.org)
[2] Ask HN: What do you do with your Raspberry Pi? (hacker news)
[3] cnet Raspberry Pi hack puts NASA in security jam June 24, 2019 9:49 AM PDT
[4] 내 백과사전 스마트 거울 만들기 2016년 1월 30일
[5] 내 백과사전 오렌지 파이 제로 wifi 연결하기 2017년 3월 16일
[6] 내 백과사전 라즈베리 파이로 RAID 0 만들어서 토렌트 머신 만들기 2017년 10월 15일
[7] 내 백과사전 마이크로봇 푸시 사용 소감 2018년 4월 4일
[8] 내 백과사전 node.js로 자작 스마트 스피커 만들기 2019년 6월 12일

Posted in pi |

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일

계산 삼위일체론 computational trinitarianism

웹서핑을 하다가 흥미로운 개념을 알게 되었는데, 제대로 이해한 건 아니지만 일단 개소리를 써 본다. 사실 이 블로그의 대부분의 내용이 다 헛소리다. ㅋ

삼위일체론은 나도 잘 모르지만-_- 이렇게 이해했다: 신이라고 추정되는 어떤 가상적 존재성과, 인간의 형태로 등장한 예수라는 인물과, 신성한 영혼이라는 개념은 형태가 모두 다르지만 본질이 동일하다는 주장이다.

무신론자인 본인도 과거 피치못할 사정으로 교회에 간 경험이 있는데, (물론 군대-_-) 아마 거기서는 내가 설교를 제일 열심히 들었을 것이다-_- 목사님이 나름 은근히 동방정교회를 디스하는 듯한 발언을 하시던데-_- 나는 여태까지 동방정교회가 삼위일체를 부정하는 줄 알았더니만, 지금 위키피디아를 보니 동방정교회도 삼위일체를 인정하고 있었네??? 아, 설교를 들은지 너무 오래돼서 여호와의 증인이랑 헷갈렸던 것 같다-_- 지금 찾아보니 여호와의 증인은 삼위일체를 부정하는 듯[1]. 개인적으로 중앙아시아사에 관심이 좀 있는데, 네스토리우스파도 삼위일체를 부정한다고 들었다. 중앙아시아사에 대한 저작물을 몇 개[2,3]보면 은근 네스토리우스파 이야기가 꽤 등장한다. 몽케 칸이 각종 종교지도자들을 불러 모아 놓고, 종교 토론 배틀-_-을 시켰다는 이야기[2]를 들은 적이 있는데, 거기서도 네스토리우스파도 당당한 일원으로 등장한다.

뭐 여하간 카네기 멜론 대학의 Robert Harper 선생의 블로그에 computational trinitarianism에 대한 설명[4]이 잘 돼 있다. nLab의 설명[5]도 참고하시기 바란다. 대충 검색해보니 ‘computational trinitarianism’을 번역한 사이트가 없길래 내 맘대로 ‘계산 삼위일체론’이라 번역했다-_- 이거 뭘로 번역해야 되지-_-

여하간 명제의 증명(proofs of propositions), 자료형의 프로그램(programs of a type), 구조의 사상(mappings between structure)이 모두 동일한 개념의 다른 표현이라는 이야기라고 한다. 세 가지는 각각 논리학, (프로그래밍) 언어론, 범주론에서 중요하게 다루는 부분이다. 논리학에서 어떤 명제가 존재하고 무엇이 증명을 이루는가를 다루고, 언어론에서 어떤 자료 유형(type)이 존재하고 어떻게 프로그램을 구성하는가를 다루며, 범주론에서 어떤 수학적 구조가 존재하고 무엇이 그들 사이의 map을 이루는가를 다룬다.

이후로 Harper 선생이 axiom으로부터 명제의 증명, 프로그램에서 변수로부터의 유형판단, 범주론에서 mapping의 유사성에 대한 설명을 하는데, 뭐 본인은 잘 모르지만 뭔가 좀 신박하다. 논리학, 프로그래밍, 수학이 모두 대통일 된다는 이야기 아닌가. 모든 증명은 프로그램이고, 모든 프로그램은 mapping이고 모든 mapping은 증명이 된다. 궁극적으로 수학적 추론과 프로그램의 실행이 합치하게 된다!!! 일전에 본 DeepHOL[6]은 아무것도 아니구만-_-

경제학에서는 고정환율제도, 자본 이동의 자유화, 통화정책의 독립성이 동시에 달성될 수 없다는 Unholy Trinity가 있는데, 수학/컴퓨터공학에서는 holy trinity가 될 듯하다. 증명, 실행, 사상(mapping)이 한 몸임을 믿습니까?? ㅋㅋㅋㅋㅋ

.


[1] NEWSM 궁금한데 물어볼 수 없었던 ‘삼위일체 교리’ 2010.07.23 14:16
[2] 내 백과사전 [서평] 몽골 제국 기행 – 마르코 폴로의 선구자들 2018년 3월 1일
[3] 내 백과사전 [서평] 신장의 역사 : 유라시아의 교차로 2013년 5월 30일
[4] The Holy Trinity (existentialtype.wordpress.com)
[5] computational trinitarianism (nLab)
[6] 내 백과사전 DeepHOL : 딥러닝을 이용한 수학 명제 자동증명 시스템 2019년 4월 29일

[서평] 역사 속의 소프트웨어 오류 – 부실한 소프트웨어가 초래한 위험천만한 사건 사고들

역사 속의 소프트웨어 오류 – 부실한 소프트웨어가 초래한 위험천만한 사건 사고들 | AcornLoft
김종하 (지은이) 에이콘출판 2014-07-18

.


검색하다가 발견한 블로그의 주인장께서 책을 광고[1]하시길래 한 번 사봤다. 2014년에 나왔으니 나온지는 좀 된 책인데 여태 몰랐네. ㅎㅎ

제목 그대로 소프트웨어 버그로 인하여 발생한 여러가지 사건 사고 케이스를 모아 놓은 책이다. 저자 자신이 소프트웨어 개발자다 보니까 이런데 관심이 생겼는 듯 하다. 무기 오작동이나 항공기 사고 등의 인명사고부터 소소한 게임의 버그까지 사례 중심으로 다양한 이야기가 나온다.

몇몇 케이스는 알고 있는 이야기였지만, 대부분은 거의 몰랐던 사고들이라 재미있다.
p172에 언급된 오염된 피 사건은 게이머들에게 대단히 유명한 사건이다.
p240에 Knight Capital의 유명한 사건[2]이 언급된다. 본 블로그의 내용보다 책의 내용이 좀 더 자세하다.
일전에 패트리어트 미사일의 진법 오차 이야기[3]를 들은 적이 있는데, 이 책의 1장에 좀 더 자세한 정황에 대한 설명이 있다.

전반적으로 저자의 품이 꽤 들어간 글임을 느낄 수 있다. 나도 잘 모르는 분야에 대한 글을 많이 읽는 편이라 생각하는데, 잘 모르는 분야에 대한 글을 읽으면, 간단한 용어 하나라도 의미를 파악하기 위해 상당히 조사를 하는 등의 고생이 심하다. (그리고 영어 울렁증이..-_-) 저자가 광범위하게 조사하여 사건의 앞뒤를 맞추고 재구성하는 스토리를 쭉 보면, 품이 이만저만 들어간게 아닌 듯 하다.

한가지 흠 아닌 흠이 있다면, 책 맨 뒤에 있는 레퍼런스가 전부 url인데, 당연히 이걸 일일이 손으로 쳐서 확인하기 불편하다. 디지털화된 뭔가가 있으면 좋겠다는 생각이 든다. 이런 책일 수록 ebook으로 나와야 맞는게 아닌가 싶기도 하다.

책의 각 장별로 서로 연관성이 적고 텍스트도 많지 않아, 짬을 내서 독서를 하는 사람에게 적당할 듯해 보인다. 시간을 내서 집중하면 1~2일 정도에 완독 가능할 듯? 상식겸 한 번쯤 읽어보는 것도 좋을 듯 하다.

.


[1] 제 책 “역사 속의 소프트웨어 오류”가 출간되었습니다 (story.wisedog.net)
[2] 내 백과사전 45분 동안 4억6천만 달러 손실을 본 Knight Capital의 소프트웨어 버그 2019년 4월 4일
[3] 오차가 인명에 영향을 준 이야기 (udaqueness.blog)

한국어 번역 방해기

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

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

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

.


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

.


[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 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일