立場新聞 Stand News

一幅以數學為主題的畫

2021/4/20 — 17:37

作者繪

作者繪

前排 spring break 得閒,想做點藝術,所以畫了一幅畫(不過應該是漫畫吧?)

問題:大家知道我依據甚麼來畫嗎?這 100 塊石頭上畫了甚麼?而石頭上有七個類似棋子的東西又是甚麼?提示


詳細解答:

廣告

要理解這幅漫畫,需首先釐清漫畫中「Formalizing」一詞的意思。

1. 近十年,人工智能(AI)發展迅速,應用的範疇多不勝數,例如自動駕駛、人臉識別、投資股票、甚至下圍棋、創作音樂、畫畫等等。在愈來愈多的行業、學科都有 AI 的身影。

廣告

那數學呢?AI 可以幫助數學研究嗎?

暫時還未成氣候。為甚麼呢?其中一個原因是,要教懂 AI 做數學研究,證明定理,首先需要大量「訓練材料」,讓它學習。這就像,要教懂 AI 做人臉識別,首先需要大量的人臉照片作為訓練材料。而中國之所以在這領域如此發達,正是因為有 14 億人,加上幾億個無孔不入的 CCTV,讓訓練材料隨手可得,對培訓 AI 無往而不利。

然而,在數學,這些訓練材料仍然缺乏。不要說最前沿的數學研究,就連大學 undergraduate 課程內的東西,都還未齊全,無法訓練 AI。

2. 你或許覺得奇怪,為甚麼呢?我們有教科書,有論文,記載著所有數學知識。我們人類一直都靠閱讀這些來學數學,不能用這些材料訓練 AI 嗎?

不能的,至少不能直接用。簡言之,是因為書本或論文中的數學,都是用人類的語言寫成(英文、中文等等),電腦根本不能真正讀懂它,理解它。然而,數學講求嚴謹性。如果我們夾硬將那些數學材料塞進電腦,讓 AI 囫圇吞棗地接收,然後胡亂訓練一通,那麼最後培植出來的 AI 也將不求甚解,沒有邏輯性或嚴謹性。這樣的 AI,若要來研究數學,是不合格的。

所以,要訓練一個 AI 數學家,必須先將現有的數學教科書、論文中的文字,翻譯成另一種新的語言,讓電腦也能理解。這才是合適的訓練材料。繼而以之訓練 AI。

3. 重點來了!這個所謂「翻譯」過程,正式的名稱,便是一開始提及的「formalize」!

故此,漫畫標題「Formalize 100 Theorems」的含意,便是「把 100 個數學定理翻譯,好讓電腦也能理解」。

那麼,究竟需要翻譯成甚麼語言呢?人類自己之間溝通的語言,肯定是不合適的。至於一般的 programming language(如 C++、Python 等),雖然是人類和電腦的共通語言,但卻仍不合適。因為它們的用途根本不是 formalize 數學,不能做數學嚴格的邏輯推論。

為此,人們需要創造新語言。事實上,這些語言早就有人創造出來,例如 70 年代創造的 Mizar,80 年代的 Isabelle 和 Coq,等等。而最新的一個,是 LEAN,由 Microsoft 在 2013 年創造。每當人們需要 formalize 某些數學定理,便必定是透過這些語言。時至今日,將數學 formalize 的工作仍然有人陸陸續續在做,而且愈來愈多人投入。

4. 有一個網站,列出了 100 個比較基本的數學定理,讓人們去 formalize 它們。這 100 個定理就像是一個目標。它亦像一個比賽:幾批數學家,分別使用不同的 formalization 語言,然後看哪邊人在數量上領先。(現在 HOL Light 和 Isabelle 以 86 個領先)

在我的漫畫中的 100 塊石頭,上面就是畫了這 100 個定理。而那七個棋子,其實是其中七個 formalization 語言的 logo。

這便是漫畫的謎底。

 

作者 Facebook

發表意見