機器證明

我記得在青少年時期，有人告訴我人工智慧 (AI) 在未來幾年會帶來多麼美好的事物。現在過了數十年，其中一些事情似乎正在發生。最近的勝利是 電腦透過彼此對弈來學習下圍棋，它們的技術迅速變得比任何人都厲害，而且策略是人類專家難以理解的。我們自然會好奇未來幾年會發生什麼事，電腦很快就會比人類更聰明嗎？(根據最近的一些選舉結果，這可能不是太難達到的門檻。)

不過，當我聽到這些消息時，我想起畢卡索在數十年前對電腦的評論：「電腦沒用。它們只能給你答案。」機器學習等技術可以產生的推理，其結果確實令人印象深刻，而且對我們這些軟體使用者和開發人員來說會很有用。但是，答案雖然有用，卻不總是全貌。我在求學初期就學到了這一點 - 只提供數學問題的答案只能得到幾分，要得到滿分，我必須展示我是如何得到答案的。得到答案的推理比結果本身更有價值。這是自學圍棋 AI 的限制之一。雖然它們可以獲勝，但無法解釋自己的策略。

在這個世界中，我認為 AI 面臨的最大挑戰之一是，雖然我們可能已經想出機器學習來教導它們獲得答案，但我們還沒有系統可以對它們的答案進行機器證明。隨著 AI 為我們做出更多判斷，我們會越來越遇到答案不夠用的情況。AI 可能接受過訓練，可以用於裁決法律案件，但如果 AI 無法解釋其推理，我們能接受這樣的判決嗎？

因此，未來我們似乎需要一種新的「程式設計師」，其工作是找出 AI 如何得到答案，並推論出 AI 技能背後的推理。我們可以看到許多領域，AI 做出不透明的判斷，我們可以看出這些判斷是好的，但需要另一種方法才能真正了解其決策背後的理論。

這個問題特別嚴重，因為我們發現這些機器很容易從訓練資料中學習不良行為，例如在評斷信用評分時歧視少數族裔。

與許多人一樣，我認為電腦的許多機會在於與人類合作。善用電腦的關鍵在於了解電腦的優勢（快速執行受限的工作）和人類的優勢，並結合兩者的優點。電腦在最智慧的層面上，是心智的工具。在編程方面，我很樂意依賴編譯器來幫助我找出錯誤或建議替代方案，這是我年輕時作為一名程式設計師被責罵的行為。這兩個領域的最強項之間的界線是流動的，而未來最令人著迷的一點，就是我們如何能善用這種流動性。