人工智能的局限性
有人聽說我想創業，給我提出了一些“忽悠”的辦法。他們說，既然你是程式語言專家，而現在人工智能（AI）又非常熱，那你其實可以搞一個“自動程式設計系統”，号稱可以自動生成程式，取代程式員的工作，節省許許多多的人力支出，這樣就可以趁着“AI 熱”拉到投資。
有人甚至把名字都給我想好了，叫“深度程式員”（DeepCoder = Deep Learning + Coder）。口号是：“有了 DeepCoder，不用 Top Coder！” 還有人給我指出了這方向最新的，吹得神乎其神的研究，比如微軟的 Robust Fill……
我謝謝這些人的關心，然而其實人工智能的能力被嚴重的誇大了。現在我簡單的講一下我的看法。
機器一樣的心
很多人喜歡鼓吹人工智能，自動車，機器人等技術，然而如果你仔細觀察，就會發現這些人不但不了解人類智能是什麼，不了解人工智能有什麼局限性，而且這些“AI 狂人”們的心，已經嚴重的機械化了。他們或多或少的失去了人性，仿佛忘記了自己是一個人，忘記了人最需要的是什麼，忘記了人的價值。這些人就像卓别林在『大獨裁者』最後的演講裡指出的：“機器一樣的人，機器一樣的心。”
每當提到 AI，這些人必然野心勃勃地号稱要“取代人類的工作”，“節省勞動力開銷”。暫且不讨論這些目标能否實作，它們與我的價值觀，從一開頭就是完全沖突的。一個偉大的公司，應該為社會創造實在的，新的價值，而不是想方設法“節省”什麼勞動力開銷，讓人失業！想一下都覺得可怕，我創造一個公司，它最大的貢獻就是讓成千上萬的人失業，為貪得無厭的人節省“勞動力開銷”，讓貧富分化加劇，讓權力集中到極少數人手裡，最後導緻民不聊生，導緻社會的荒蕪甚至崩潰……
我不可想象生活在那樣一個世界，就算那将使我成為世界上最有錢的人，也沒有了意義。世界上有太多錢買不來的東西。如果走在大街上，我看不到人們幸福的笑容，悠閑的步伐，沒有親切的問候，關愛和幽默感，看不見甜蜜浪漫的愛情，反而看見遍地痛不欲生的無家可歸者，鼻孔裡鑽進來他們留下的沖人的尿騷味，走到哪裡都怕有人搶劫，因為人們實在活不下去了，除了偷和搶，沒有别的辦法活……
如果人工智能成功的話，這也許就是最後的結果。幸運的是，有充足的證據顯示，人工智能是永遠不會成功的。
我的人工智能夢
很多人可能不知道，我也曾經是一個“AI 狂熱者”。我也曾經為人工智能瘋狂，把它作為自己的“偉大理想”。我也曾經張口閉口拿“人類”說事，仿佛機器是可以跟人類相提并論，甚至高于人類的。當深藍電腦戰勝卡斯帕羅夫，我也曾經感歎：“啊，我們人類完蛋了！” 我也曾經以為，有了“邏輯”和“學習”這兩個法（kou）寶（hao），機器總有一天會超越人類的智能。可是我沒有想清楚這具體要怎麼實作，也沒有想清楚實作了它到底有什麼意義。
故事要從十多年前講起，那時候人工智能正處于它的冬天。在清華大學的圖書館，我偶然地發現了一本塵封已久的 『Paradigms of Artificial Intelligence Programming』（PAIP），作者是 Peter Norvig。像個考古學家一樣，我開始逐一地琢磨和實作其中的各種經典 AI 算法。PAIP 的算法側重于邏輯和推理，因為在它的年代，很多 AI 研究者都以為人類的智能，歸根結底就是邏輯推理。
他們天真地以為，有了謂詞邏輯，一階邏輯這些東西，可以表達“因為是以不但而且存在所有”，機器就可以擁有智能。于是他們設計了各種基于邏輯的算法，專家系統（expert system），甚至設計了基于邏輯的程式語言 Prolog，把它叫做“第五代程式語言”。最後，他們遇到了無法逾越的障礙，衆多的 AI 公司無法實作他們誇口的目标，各種基于“神經元”的機器無法解決實際的問題，巨額的政府和民間投資化為泡影，人工智能進入了冬天。
我就是在那樣一個冬天遇到了 PAIP。它雖然沒能讓我投身于人工智能領域，卻讓我迷上了 Lisp 和程式語言。也是因為這本書，我第一次輕松而有章法的實作了 A* 等算法。我第一次了解到了程式的“子產品化”是什麼，在代碼例子的引導下，我開始在自己的程式裡使用小的“工具函數”，而不再憂心忡忡于“函數調用開銷”。PAIP 和 SICP 這兩本書，最後導緻了我投身于更加“基礎”的程式語言領域，而不是人工智能。
在 PAIP 之後，我又迷了一陣子機器學習（machine learning），因為有人告訴我，機器學習是人工智能的新篇章。然而我逐漸意識到，所謂的人工智能和機器學習，跟真正的人類智能，關系其實不大。相對于實際的問題，PAIP 裡面的經典算法要麼相當幼稚，要麼複雜度很高，不能解決實際的問題。最重要的問題是，我看不出 PAIP 裡面的算法跟“智能”有什麼關系。而“機器學習”這個名字，基本是一個幌子。很多人都看出來了，機器學習說白了就是統計學裡面的“拟合函數”，換了一個具有迷惑性的名字而已。
人工智能的研究者們總是喜歡擡出“神經元”一類的名詞來吓人，跟你說他們的算法是受了人腦神經元工作原理的啟發。注意了，“啟發”是一個非常模棱兩可的詞，由一個東西啟發得來的結果，可以跟這個東西毫不相幹。比如我也可以說，Yin 語言的設計是受了九 yin 真經的啟發 :P
世界上這麼多 AI 研究者，有幾個真的研究過人腦，解刨過人腦，拿它做過實驗，或者讀過腦科學的研究成果？最後你發現，幾乎沒有 AI 研究者真正做過人腦或者認知科學的研究。著名的認知科學家 Douglas Hofstadter 早就在接受采訪時指出，這幫所謂“AI 專家”，對人腦和意識（mind）是怎麼工作的，其實完全不感興趣，也從來沒有深入研究過，卻号稱要實作“通用人工智能”（Artificial General Intelligence, AGI），這就是為什麼 AI 直到今天都隻是一個虛無的夢想。
識别系統和語言了解
縱觀曆史上機器學習能夠做到的事情，都是一些字元識别（OCR），語音識别，人臉識别一類的，我把這些統稱為“識别系統”。當然，識别系統是很有價值的，OCR 是非常有用的，我經常用手機上的語音輸入法，人臉識别對于公安機關顯然意義重大。然而很多人是以誇口，說我們可以用同樣的方法（機器學習，深度學習），實作“人類級别的智能”，取代所有的人類工作，這就是神話了。
識别系統跟真正了解語言的“人類智能”，其實相去非常遠。說白了，這些識别系統，也就是統計學的拟合函數能做的事情。比如 OCR 和語音識别，就是輸入像素或者音頻，輸出單詞文本。很多人分不清“文字識别”和“語言了解”的差別。OCR 和語音識别系統，雖然能依靠統計的方法，“識别”出你說的是哪些字，它卻不能真正“了解”你在說什麼。
聊一點深入的話題，看不懂的人可以跳過這一段。“識别”和“了解”的差别，就像程式語言裡面“文法”和“語義”的差别。程式語言的文本，首先要經過詞法分析器（lexer），文法分析器（parser），才能送進解釋器（interpreter），隻有解釋器才能實作程式的語義。類比一下，自然語言的語音識别系統，其實隻相當于程式語言的詞法分析器（lexer）。我在之前的文章裡已經指出，詞法分析和文法分析，隻不過是實作一個語言的萬裡長征的“第0步”。
大部分的 AI 系統裡面連文法分析器（parser）都沒有，是以主謂賓，句子結構都分析不清楚，更不要說了解其中的含義了。IBM 的語音識别專家 Frederick Jelinek 曾經開玩笑說：“每當我開掉一個語言學家，識别率就上升了。” 其原因就是語音識别僅相當于一個 lexer，而語言學家研究的是 parser 以及 interpreter。當然了，你們幹的事情太初級了，是以語言學家幫不了你們，但這并不等于語言學家是沒有價值的。
很多人語音識别專家以為文法分析（parser）是沒用的，因為人好像從來沒有 parse 過句子，就了解了它的意義。然而他們沒有察覺到，人其實必須要不知不覺地 parse 有些句子，才能了解它的含義。
舉一個很簡單的例子。如果我對 Siri 說：“我想看一些貓的照片。” 它會給我下圖的回答：“我在網上沒有找到與‘一些貓’有關的資料。”
這說明了什麼呢？很多人可能都發現了，這說明了 Siri 無法了解這個句子，是以它到網上去搜一些關鍵字。可是這還說明一個更深層次的問題，那就是 Siri 裡面并沒有 parser，甚至連一個好的分詞系統都沒有，是以它連該搜什麼關鍵字都不知道。
為什麼 Siri 去網上找關于“一些貓”的資訊，而不是關于“貓”的資訊呢？如果搜尋“貓”和“照片”，它至少能找到一些東西。這是因為 Siri 其實沒有 parser，它裡面根本沒有文法樹。它隻是利用一些普通的 NLP 方法（比如 n-gram），把句子拆成了“我…想…看…一些貓…的…照片”，而不是文法樹對應的“我…想…看…一些…貓…的…照片”。
這個句子的文法樹，按照我之前做過的一種自然語言 parser 的方式，分析出來大概是這個樣子。
具體細節太過技術性，我就不在這裡解釋了。不過有興趣的人可能發現了，根據文法樹，這句話可以簡化為：“我想看照片。” 其中“看照片”是一個從句，它是“我想…”的賓語，也就是所謂賓語從句。多少照片呢？一些。看什麼樣的照片呢？主題是貓的照片。
- 我想看照片
- 我想看一些照片
- 我想看貓的照片
- 我想看一些貓的照片
是不是挺有意思？
Siri 裡面沒有這種文法樹，而且它的 n-gram 居然連“一些”和“貓”都沒分開，這就是為什麼它去找“一些貓”，而不是“貓”。它甚至把“照片”這麼重要的詞都忽略了。是以 Siri 雖然正确的進行了“語音識别”，知道我說了那些字。但由于沒有 parser，沒有文法樹，它不可能正确的了解我到底在說什麼，它甚至不知道我在說“關于什麼”。
制造自然語言的 parser 有多難？很多人可能沒有試過。我做過這事。在 Indiana 的時候，我為了湊足學分，修了一門 NLP 課程，跟幾個同學一起實作了一個英語文法的 parser。它分析出來的文法樹形式，就像上面的那樣。
你可能想不到有多困難，你不僅要深刻了解程式設計語言的 parser 理論（LL，LR，GLR……），還得依靠大量的例子和資料，才能解開人類語言裡的各種歧義。我的合作夥伴是專門研究 NLP 的，把什麼 Haskell，類型系統，category theory，什麼 GLR parsing 之類…… 都弄得很溜。然而就算如此，我們的英語 parser 也隻能處理最簡單的句子，還錯誤百出，最後蒙混過關 :P
經過了文法分析，得到一棵“文法樹”，你才能傳給人腦裡語言的了解中心（類似程式語言的“解釋器”）。解釋器“執行”這個句子，為相關的名字找到對應的“值”，進行計算，才能得到句子的含義。至于人腦如何為句子裡的詞彙賦予“意義”，如何把這些意義組合在一起，形成“思維”，這個問題似乎沒有人很明白。
至少，這需要大量的實際經驗，這些經驗是一個人從生下來就開始積累的。機器完全不具備這些經驗，我們也不知道如何才能讓它獲得經驗。我們甚至不知道這些經驗在人腦裡面是什麼樣的結構，如何組織的。是以機器要真的了解一個句子，真是跟登天一樣難。
這就是為什麼 Hofstadter 說：“一個機器要能了解人說的話，它必須要有腿，能夠走路，去觀察世界，獲得它需要的經驗。它必須能夠跟人一起生活，體驗他們的生活和故事……” 最後你發現，制造這樣一個機器，比養個小孩困難太多了，這不是吃飽了沒事幹是什麼。
機器對話系統和人類客服
各大公司最近叫得最響亮的“AI 技術”，就是 Siri，Cortana，Google Assistant，Amazon Echo 一類含有語音識别功能的工具，叫做“個人助手”。這些東西裡面，到底有多少可以叫做“智能”的東西，我想用過的人都應該明白。我每一次試用 Siri 都被它的愚蠢所折服，可以讓你着急得砸了水果手機。那另外幾個同類，也沒有好到哪裡去。
很多人被“微軟小冰”忽悠過，咋一看這家夥真能了解你說的話呢！然而聊一會你就發現，小冰不過是一個“網絡句子搜尋引擎”。它隻是按照你句子裡的關鍵字，随機搜出網上已有的句子。大部分這類句子出自問答類網站，比如百度知道，知乎。
一個很簡單的實驗，就是反複發送同一個詞給小冰，比如“王垠”，看它傳回什麼内容，然後拿這個内容到 Google 或者百度搜尋，你就會找到那個句子真正的出處。人都喜歡自欺欺人，看到幾個句子回答得挺“俏皮”，就以為它有智能，而其實它是随機搜出一個句子，牛頭不對馬嘴，是以你才感覺“俏皮”。比如，你跟小冰說：“王垠是誰？”，她可能回答：“王垠這是要變段子手麼。”
心想多可愛的妹子，不正面回答你的問題，有幽默感！然後你在百度一搜，發現這句話是某論壇裡面黑我的人說的。
下面是一個确切的例子，它顯示了小冰是如何工作的。圖檔是 2016 年 10 月底抓的，那時候我試了一下跟小冰對話。現在的情況可能稍微有所不同。
這說明小冰的答複，基本是百度問答，知乎一類的地方來的，它似乎隻是對那上面的資料做了一個搜尋。小冰隻是随機搜尋出這句子，至于幽默感，完全是你自己想象出來的。很多人跟小冰對話，喜歡隻把其中“符合邏輯”或者“有趣”的部分截圖下來，然後驚呼：“哇，小冰好聰明好有趣！” 他們沒有告訴你的是，沒貼出來的對話，很多都是雞同鴨講。
IBM 的 Watson 系統在 Jeopardy 遊戲中戰勝了人，很多人就以為 Watson 能了解人類語言，具有人類級别的智能。這些人甚至都不知道 Jeopardy 是怎麼玩的，就盲目做出判斷，以為 Jeopardy 是一種需要了解人類語言才可以玩的遊戲。等你細看，發現 Jeopardy 就是很簡單的“猜謎”遊戲，題目是一句話，答案是一個名詞。比如：“有個歌手去年得了十項格萊美獎，請問他是誰？”
如果你了解了我之前對“識别系統”的分析，就會發現 Watson 也是一種識别系統，它的輸入是一個句子，輸出是一個名詞。一個可以玩 Jeopardy 的識别系統，可以完全不了解句子的意思，而是依靠句子裡出現的關鍵字，依據分析大量語料得到的拟合函數，輸出一個單詞。世界上那麼多的名詞，到哪裡去找這樣的語料呢？這裡我給你一個 Jeopardy 謎題作為提示：“什麼樣的網站，你給它一個名詞，它輸出一些段落和句子，給你解釋這個東西是什麼，并且提供給你各種相關資訊？”
很容易猜吧？就是 Wikipedia 那樣的百科全書！你隻需要把這種網站的内容掉一個頭，制造一個“倒索引”搜尋引擎。你輸入一個句子，它就根據裡面的關鍵字，搜尋到最相關的名詞。這就是一台可以玩 Jeopardy 的機器，而且它很容易超越人類玩家，就像 Google，Yahoo 之類的搜尋引擎很容易超越人查找網頁的能力一樣。可是這裡面基本沒有了解和智能可言。
其實為了驗證 Watson 是否了解人類語言，我早些時候去 Watson 的網站玩過它的“客服 demo”，結果完全是雞同鴨講，大部分時候 Watson 回答：“我不清楚你在說什麼。你是想要……” 然後列出一堆選項，1，2，3……
老闆，你指望拿這樣的東西代替你公司的人類客服嗎？那你的公司就等着倒閉吧 :P
當然，我并不是說這些産品完全沒有價值。我用過 Siri 和 Google Assistant，我發現它們還是有點用處的，特别是在開車的時候。因為開車時操作手機容易出事故，是以我可以利用語音控制。比如我可以對手機說：“導航到最近的加油站。” 然而實作這種語音控制，根本不需要了解語言，你隻需要用語音識别輸入一個函數調用：導航（加油站）。
個人助手在其它時候用處都不大。我不想在家裡和公共場所使用它們，原因很簡單：我懶得說話，或者不友善說話。點選幾下螢幕，我就可以精确地做到我想要的事情，這比說話省力很多，也精确很多。個人助手完全不了解你在說什麼，這種局限性本來無可厚非，可以用就行了，然而各大公司最近卻拿個人助手這類東西來煽風點火，誇大其中的“智能”成分，閉口不提他們的局限性，讓外行們以為人工智能就快實作了，這就是為什麼我必須鄙視一下這種做法。
舉個例子，由于有了這些“個人助手”，有人就号稱類似的技術可以用來制造“機器客服”，使用機器代替人作為客服。他們沒有想清楚的是，客服看似“簡單工作”，跟這些語音控制的玩意比起來，難度卻是天壤之别。客服必須了解公司的業務，必須能夠精确地了解客戶在說什麼，必須形成真正的對話，要能夠為客戶解決真正的問題，而不能隻抓住一些關鍵字進行随機回複。
另外，客服必須能夠從對話資訊，引發現實世界的改變，比如呼叫配送中心停止發貨，向上級請求滿足客戶的特殊要求，拿出退貨政策跟客戶辯論，拒絕他們的退貨要求，抓住客戶心理，向他們推銷新服務等等，各種需要“人類經驗”才能處理的事情。是以機器能不但要能夠形成真正的對話，了解客戶的話，它們還需要現實世界的大量經驗，需要改變現實世界的能力，才可能做客服的工作。由于這些個人助手全都是在忽悠，是以我看不到有任何希望，能夠利用現有的技術實作機器客服。
連客服這麼按部就班的工作，機器都無法取代，就不用說更加複雜的工作了。很多人看到 AlphaGo 的勝利，以為所謂 Deep Learning 終究有一天能夠實作人類級别的智能。在之前的一篇文章裡，我已經指出了這是一個誤區。很多人以為人覺得困難的事情（比如圍棋），就是展現真正人類智能的地方，其實不是那樣的。我問你，心算除法（23423451345 / 729）難不難？這對于人是很難的，然而任何一個傻電腦，都可以在 0.1 秒之内把它算出來。圍棋，國際象棋之類也是一樣的原理。這些機械化的問題，其實不能反應真正的人類智能，它們展現的隻是大量的蠻力。
縱觀人工智能領域發明過的吓人術語，從 Artificial Intelligence 到 Artificial General Intelligence，從 Machine Learning 到 Deep Learning，…… 我總結出這樣一個規律：人工智能的研究者們似乎很喜歡制造吓人的名詞，當人們對一個名詞失去信心，他們就會提出一個不大一樣的，新的名詞，免得人們把對這個名詞的失望，轉移到新的研究上面。然而這些名詞之間，終究是換湯不換藥。因為沒有人真的知道人的智能是什麼，是以也就沒有辦法實作“人工智能”。
生活中的每一天，我這個“前 AI 狂熱者”都在為“人類智能”顯示出來的超凡能力而感到折服。甚至不需要是人，任何高等動物（比如貓）的能力，都讓我感到敬畏。我發自内心的尊重人和動物。我不再有資格拿“人類”來說事，因為面對這個詞彙，任何機器都是如此的渺小。
紀念我的聊天機器人 helloooo
乘着這個熱門話題，現在我來講一下，十多年前我自己做聊天機器人的故事……
如果你看過 PAIP 或者其它的經典人工智能教材，就會發現這些機器對話系統，最初的思想來自一個叫“ELIZA”的 AI 程式。Eliza 被設計為一個心理醫生，跟你對話排憂解難，而它内部其實就是一個類似小冰的句子搜尋引擎，實作方式完全用正規表達式比對搞定。比如，Eliza 的某個規則可以說，當使用者說：“我(.*)”，那麼你就回答：“我也$1……” 其中 $1 代替原句子裡的一部分，造成一種“了解”的效果。比如使用者也許會說：“我好無聊。” Eliza 就可以說：“我也好無聊……” 然後這兩個無聊的人就惺惺相惜，有伴了。
有些清華的老朋友也許還記得，十多年前在清華的時候，我做了一個聊天機器人放在水木清華 BBS，紅極一時，是以我也可以算是網絡聊天機器人的鼻祖了 :) 我的聊天機器人，水木賬号叫 helloooo。helloooo 的性格像蠟筆小新，是一個調皮又好色的小男孩。
它内部采用的就是類似 Eliza 的做法，根本不了解句子，甚至連語料庫都沒有，神經網絡也沒有，裡面就是一堆我事先寫好的正規表達式“句型”而已。你輸入一個句子，它比對之後，從幾種回複之中随機挑一個，是以你反複說同樣的話，helloooo 的回答不會重複，如果你故意反複說同樣的話，最後 helloooo 會對你說：“你怎麼這麼無聊啊？”或者“你有病啊？” 或者轉移話題，或者暫時不理你…… 這樣對方就不會明顯感覺它是一個傻機器。
就是這麼簡單個東西。出乎我意料的是，helloooo 一上網就吸引了很多人。一傳十十傳百，每天都不停地有人發資訊跟他聊。由于我給他設定的正規表達式和回複方式考慮到了人的心理，是以 helloooo 顯得很“俏皮”，有時候還可能裝傻，搗蛋，延遲回複，轉移話題，還可能主動找你聊天，使用超過兩句的小段子，…… 各種花樣都有。最後，這個小色鬼赢得了好多妹子們的喜愛，甚至差點約了幾個出去呢！:P
在這點上，helloooo 可比小冰強很多。小冰的技術含量雖然多一些，資料多很多，然而 helloooo 感覺更像一個人，也更受歡迎。這說明，我們其實不需要很高深的技術，不需要了解自然語言，隻要你設計巧妙，抓住人的心理，就能做出人們喜愛的聊天機器。
後來，helloooo 終于引起了清華大學人智組研究所學生的興趣，來問我：“你這裡面使用的什麼語料庫做分析啊？” 我：“&%&￥@#@#%……”
自動程式設計是不可能的
現在回到有些人最開頭的提議，實作自動程式設計系統。我現在可以很簡單的告訴你，那是不可能實作的。微軟的 Robust Fill 之類，全都是在扯淡。我對微軟最近乘着 AI 熱，各種煽風點火的做法，表示少許鄙視。不過微軟的研究員也許知道這些東西的局限，隻是國内小編在誇大它的功效吧。
你仔細看看他們舉出的例子，就知道那是一個玩具問題。人給出少量例子，想要電腦完全正确的猜出他想做什麼，那顯然是不可能的。很簡單的原因，例子不可能包含足夠的資訊，精确地表達人想要什麼。最最簡單的變換也許可以，然而隻要多出那麼一點點例外情況，你就完全沒法猜出來他想幹什麼。就連人看到這些例子，都不知道另一個人想幹什麼，機器又如何知道？這根本就是想實作“讀心術”。甚至人自己都可以是糊塗的，他根本不知道自己想幹什麼，機器又怎麼猜得出來？是以這比讀心術還要難！
對于如此弱智的問題，都不能 100% 正确的解決，遇到稍微有點邏輯的事情，就更沒有希望了。論文最後還“高瞻遠矚”一下，提到要把這作法擴充到有“控制流”的情況，完全就是瞎扯。是以 RobustFill 所能做的，也就是讓這種極其弱智的玩具問題，達到“接近 92% 的準确率”而已了。另外，這個 92% 是用什麼标準算出來的，也很值得懷疑。
任何一個負責的程式語言專家都會告訴你，自動生成程式是根本不可能的事情。因為“讀心術”是不可能實作的，是以要機器做事，人必須至少告訴機器自己“想要什麼”，然而表達這個“想要什麼”的難度，其實跟程式設計幾乎是一樣的。實際上程式員工作的本質，不就是在告訴電腦自己想要它幹什麼嗎？最困難的工作（資料結構，算法，資料庫系統）已經被固化到了庫代碼裡面，然而表達“想要幹什麼”這個任務，是永遠無法自動完成的，因為隻有程式員自己才知道他想要什麼，甚至他自己都要想很久，才知道自己想要什麼……
有句話說得好：程式設計不過是一門失傳的藝術的别名，這門藝術的名字叫做“思考”。沒有任何機器可以代替人的思考，是以程式員是一種不可被機器取代的工作。雖然好的程式設計工具可以讓程式員工作更加舒心和高效，任何試圖取代程式員工作，節省程式設計勞力開銷，克扣程式員待遇，試圖把他們變成“可替換原件”的做法（比如 Agile，TDD），最終都會倒戈，使得雇主收到适得其反的後果。同樣的原理也适用于其它的創造性工作：廚師，發型師，畫家，……
是以别妄想自動程式設計了。節省程式員開銷唯一的辦法，是邀請優秀的程式員，尊重他們，給他們好的待遇，讓他們開心安逸的生活和工作。同時，開掉那些滿口“Agile”，“Scrum”，“TDD”，“軟體工程”，光說不做的扯淡管理者，他們才是真正浪費公司資源，降低開發效率和軟體品質的禍根。
傻機器的價值
我不反對繼續投資研究那些有實用價值的人工智能（比如人臉識别一類的），然而我覺得不應該過度誇大它的用處，把注意力過分集中在它上面，仿佛那是唯一可以做的事情，仿佛那是一個劃時代的革命，仿佛它将取代一切人類勞動。
我的個人興趣其實不在人工智能上面。那我要怎麼創業呢？很簡單，我覺得大部分人不需要很“智能”的機器，“傻機器”才是對人最有價值的，我們其實遠遠沒有開發完傻機器的潛力。是以設計新的，可靠的，造福于人的傻機器，應該是我創業的目标。當然我這裡所謂的“機器”，包括了硬體和軟體，甚至可以包括雲計算，大資料等内容。
隻舉一個例子，有些 AI 公司想研制“機器傭人”，可以自動打掃衛生做家務。我覺得這問題幾乎不可能解決，還不如直接請真正智能的——阿姨來幫忙。我可以做一個阿姨服務平台，友善需要服務的家庭和阿姨進行牽線搭橋。給阿姨配備更好的工具，通信，日程，支付設施，讓她工作不累收錢又友善。另外給家庭提供關于阿姨工作的回報資訊，讓家庭也省心放心，那豈不是兩全其美？哪裡需要什麼智能機器人，難度又高，又貴又不好用。顯然這樣的阿姨服務平台，結合真正的人的智能，輕而易舉就可以讓那些機器傭人公司死在萌芽之中。
當然我可能不會真去做個阿姨服務平台，隻是舉個例子，說明許許多多對人有用的傻機器，還在等着我們去發明。這些機器設計起來雖然需要靈機一動，然而實作起來難度卻不高，給人帶來便利，經濟上見效也快。這些東西不對人的工作造成競争，反而可能制造更多的就業機會。利用人的智慧，加上機器的蠻力，讓人們又省力又能掙錢，才是最合理的發展方向。
智能合約的形式驗證
在之前一篇關于人工智能的文章裡，我指出了“自動程式設計”的不可能性。今天我想來談談一個相關的話題：智能合約的形式驗證。有些人聲稱要實作基于“深度學習”的，自動的智能合約形式驗證（formal verification），用于確定合約的正确性。然而今天我要告訴你的是，跟自動程式設計一樣，完全自動的合約驗證，也是不可能實作的。
随着區塊鍊技術的愈演愈烈，很多人開始在以太坊的“智能合約語言”上做文章。其中一部分是搞 PL 的人，他們試圖對 Solidity 之類語言寫的智能合約進行形式驗證，号稱要用嚴密的數理邏輯方法，自動的驗證智能合約的正确性。其中一種方法，是用“深度學習”，經過訓練，自動生成 Hoare Logic 的“前條件”和“後條件”。
Hoare Logic
我好像已經把你搞糊塗了…… 我們先來科普一下 Hoare Logic。
Hoare Logic 是一種形式驗證的方法，用于驗證程式的正确性。它的做法是，先給代碼标注一些“前條件”和“後條件”（pre-condition 和 post-condition），然後就可以進行邏輯推理，驗證代碼的某些基本屬性，比如轉賬之後餘額是正确的。
舉一個很簡單的 Hoare Logic 例子：
{x=} x:=x+ {x>}
它的意思是，如果開頭 x 等于 0，那麼 x:=x+1 執行之後，x 應該大于 0。這裡的前條件（pre-condition）是 x=0，後條件（post-condition）是 x > 0。如果 x 開頭是零，執行
x:=x+1
之後，x 就會大于 0，是以這句代碼就驗證通過了。
Hoare Logic 的系統把所有這些前後條件和代碼串接起來，經過邏輯推導驗證，就可以作出這樣的保證：在前條件滿足的情況下，執行代碼之後，後條件一定是成立的。如果所有這些條件都滿足，系統就認為這是“正确的程式”。注意這裡的所謂“正确”，完全是由人來決定的，系統并不知道“正确”是什麼意思。
Hoare Logic 對于程式的安全性，确實可以起到一定的效果，它已經被應用到了一些實際的項目。比如微軟 Windows 的驅動程式代碼裡面，有一種“安全标注語言”，叫做 SAL，其實就是 Hoare Logic 的一個實作。然而前條件和後條件是什麼，你必須自己給代碼加上标注，否則系統就不能工作。
比如上面的例子，系統如何知道我想要“x>0”這個性質呢？隻有我自己把它寫出來。是以要使用 Hoare Logic，必須在代碼上标注很多的 pre-condtion 和 post-condition。這些條件要如何寫，必須要深入了解程式語言和形式邏輯的原理。這個工作需要經過嚴格訓練的專家來完成，而且需要很多的時間。
自動生成标注是不可能的
是以即使有了 Hoare Logic，程式驗證也不是輕松的事情。于是呢就有人乘火打劫，提出一個類似減肥藥的想法，聲稱他們要用“深度學習”，通過對已有标注的代碼進行學習，最後讓機器自動标注這些前後條件。還在“空想”階段呢，卻已經把“自動标注”作為自己的“優勢”寫進了白皮書：“我們的方法是自動的，其他的項目都是手動的……”
很可惜的是，“自動标注”其實跟“自動程式設計”是一樣的空想。自動程式設計的難點在于機器沒法知道你想要做什麼。同理，自動标注的難點在于，機器沒法知道你想要代碼滿足什麼樣的性質（property）。
除非你告訴它，機器永遠無法知道函數參數必須滿足什麼樣的條件（前條件），它也無法知道函數出口應該滿足什麼樣的條件（後條件）。比如上面的那個例子，機器怎麼知道你想要程式執行之後 x 大于零呢？除非你告訴它，它是不可能知道的。
你也許會問，深度學習難道不能幫上忙嗎？想想吧…… 你可以給深度學習系統上千萬行已經标注前後條件的代碼。你可以把整個 Windows 系統，整個 Linux 系統，FireFox 的代碼全都标注好，再加上一些戰鬥機，宇宙飛船的代碼，輸入深度學習系統進行“學習”。現在請問系統，我下面要寫一個新的函數，你知道我想要做什麼嗎？你知道我希望它滿足什麼性質嗎？你仍然不知道啊！隻有我自己才知道：它是用來自動給我的貓鏟屎的 :p
是以，利用深度學習自動标注 Hoare Logic 的前後條件，跟“自動程式設計”一樣，是在試圖實作“讀心術”，那顯然是不可能的。作為資深的 PL 和形式驗證專家，這些人應該知道這是不可能自動實作的。他們提出這樣的想法，并且把它作為相對于其他智能合約項目的優勢，當然隻是為了忽悠外行，為了發币圈錢 ;)
如果真能用深度學習生成前後條件，進而完全自動的驗證程式的正确性，那麼這種辦法應該早就在形式驗證領域炸鍋了。每一個形式驗證專家都希望能夠完全自動的證明程式的正确性，然而他們早就知道那是不可能的。
設計語言來告訴機器我們想要什麼，什麼叫做“正确”，這本身就是 PL 專家和形式驗證專家的工作。設計出了語言，我們還得依靠優秀的程式員來寫這些代碼，告訴機器我們想要做什麼。我們得依靠優秀的安全專家，給代碼加上前後條件标注，告訴機器什麼叫做“正确安全的代碼”…… 這一切都必須是人工完成的，無法靠機器自動完成。
說到這些，我就為這些學者感到悲哀，想不鄙視他們都不行了 :p 很早的時候我就有這種感覺，總是有些 PL 人看到什麼方向有錢就往什麼方向上靠，拿一堆吓人的術語來忽悠外行。管它一個外行設計的語言有多垃圾呢，我們幫它做形式驗證工具，我們為它寫編譯器，寫虛拟機，為它提出“形式化語義”（formal semantics）！給外行打下手，給母豬塗口紅，完全失去作為一個專家的責任感和尊嚴。
現在這種風氣愈演愈烈，随着比特币和以太坊的熱門，他們開始在 Solidity 之類的語言和智能合約上做文章。新瓶子裝老酒，反反複複做同樣的事情。甚至完全失去職業道德，号稱要實作一些早就知道不可能的事情。現在最熱門的兩個投資方向就是人工智能和區塊鍊，現在我用機器學習來驗證區塊鍊智能合約的正确性，兩個熱點都占全了！;)
顯然，我也可以輕而易舉做出對智能合約進行某種“驗證”或者“靜态分析”的工具，然而我深刻的了解數理邏輯對于程式正确性的局限性。很多代碼沒法被證明為正确，但它們确實是正确的。很多代碼有 bug，卻沒有任何工具可以發現它們。這是一個不幸的事實，就像無法實作永動機一樣，沒有任何人能夠改變。
當然，我并沒有排除對智能合約手動加上 Hoare Logic 标記這種做法的可行性，它是有一定價值的。我隻是想提醒大家，這些标記必須是人工來寫的，不可能自動産生。另外，雖然工具可以有一定的輔助作用，但如果寫代碼的人自己不小心，是無法保證程式完全正确的。
如何保證智能合約的正确呢？這跟保證程式的正确性是一樣的問題。隻有懂得如何寫出幹淨簡單的代碼，進行嚴密的思考，才能寫出正确的智能合約。關于如何寫出幹淨，簡單，嚴密可靠的代碼，你可以參考我之前的一些文章。
做智能合約驗證的工作也許能圈到錢，然而卻是非常枯燥而沒有成就感的。為此我拒絕了好幾個有關區塊鍊的合作項目。雖然我對區塊鍊的其它一些想法（比如去中心化的共識機制）是感興趣的，我對智能合約的正确性驗證一點都不看好。
智能合約不可行
實際上，我認為智能合約這整個概念就不靠譜。比特币和以太坊的系統裡面，根本就不應該，而且沒必要存在腳本語言。我認為智能合約系統在目前階段并不可行。
比特币的解鎖腳本執行方式，一開頭就有個低級錯誤，導緻 injection 安全漏洞。使用者可以寫出惡意代碼，導緻節點的運作時系統出錯。我不可想象，在 2009 年仍然有人把兩段代碼以文本方式貼在一起，然後執行。稍微有點經驗的黑客都知道這裡很可能有可攻擊的點。
以太坊的 Solidity 語言一開頭就有低級錯誤，導緻價值五千萬美元的以太币被盜。以太坊的智能合約系統消耗大量的計算資源，還導緻了嚴重的性能問題。可以說比特币和以太坊的作者都是 PL 外行，然而如果是内行來做這些語言，難道就會更好嗎？我并不這麼認為。
如果換做是我設計了比特币，我不會為它設計一種語言。讓使用者可以程式設計是很危險的！不僅是因為極少的使用者能夠寫出正确而可靠的代碼，而且因為語言系統的實作極少可以不出現 bug。語言系統的設計錯誤，會給黑客可乘之機，寫出惡意腳本來進行破壞。從來沒有任何語言和他們的編譯器，運作時系統是一開頭就正确的，都需要很多年才能穩定下來。另外一旦你讓系統來運作這些語言的代碼，又會需要考慮性能的問題。這對于普通的語言問題不大，你不要用它來控制飛機就可以。然而電子貨币系統的語言，幾乎不允許出現這方面的問題。
是以與其提心吊膽的設計這些智能合約語言，還不如幹脆不要這種功能。
而且我們真的需要那些腳本的功能嗎？比特币雖然有腳本語言，可是常用的腳本其實隻有不超過 5 個，直接 hard code 進去就可以了。以太坊的白皮書雖然做了那麼多的應用展望，EVM 上出現過什麼有價值的應用嗎？我并不覺得我們需要這些智能合約。電子貨币隻要做好一件事，能被安全高效的當成錢用，就已經不錯了。
美元，人民币，黃金…… 它們有合約的功能嗎？沒有。為什麼電子貨币一定要捆綁這種功能呢？我覺得這是不夠子產品化的設計。電子貨币就應該像貨币一樣，能夠實作轉賬交換的簡單功能就可以了。合約應該是另外單獨的系統，不應該跟貨币捆綁在一起。
那合約怎麼辦呢？交給律師和會計去辦 :) 你有沒有想過，為什麼世界上的法律系統不是程式控制自動執行的呢？為什麼我們需要律師和法官，而不隻是機器人？這不隻是曆史遺留問題。需要了解法律的本質屬性才會明白，完全不通過人來進行的機械化執法是不可行的。
奢望過多的功能其實是一種過度工程（over-engineering）。花費精力去折騰智能合約系統，将會大大的延緩電子貨币真正被世界接受。實話說嘛，試用了多種電子貨币之後，我發現它們的技術相當有趣，但其實仍然處于玩具和試驗階段，基本無法作為貨币使用。絕大部分電子貨币都在等着被淘汰。它們的發展方向存在着各種迷茫，很多人走向歧途，或者各種忽悠。
待續……
<script>
(function(){
function setArticleH(btnReadmore,posi){
var winH = $(window).height();
var articleBox = $("div.article_content");
var artH = articleBox.height();
if(artH > winH*posi){
articleBox.css({
'height':winH*posi+'px',
'overflow':'hidden'
})
btnReadmore.click(function(){
articleBox.removeAttr("style");
$(this).parent().remove();
})
}else{
btnReadmore.parent().remove();
}
}
var btnReadmore = $("#btn-readmore");
if(btnReadmore.length>0){
if(currentUserName){
setArticleH(btnReadmore,3);
}else{
setArticleH(btnReadmore,1.2);
}
}
})()
</script>
</article>