研究所入學那天，老師照例勉勵新生們。多年後，除了指導老師說的一些事，我只記得這麼一段話：「所謂做研究，就是找個好問題，然後解決它。前者通常比後者難。」
很遺憾，剛到所上誰都不認識的我竟不記得是誰下了這麼一個雋永深刻的評語。
過去兩週試著證明一個演算法的正確性，本希望能在一週內解決，硬是拖了一倍的時間。這時回想起那句話，倒是在小尺度內有了類似的感觸：做我們這種研究，就是找出那個該證的性質，然後證明它。前者通常比後者難。
所謂一個演算法「正確」，指的是其算出的東西符合規格。這當然是我們最後希望證明的性質。但通常這無法直接證。我們得證明該演算法滿足某些不變量 (invariant). 理想上，不變量在設計演算法時就該推導出來。實際上，我們常得要證明別人的演算法，而對方對不變量只有一個籠統模糊的描述；或著我們討論的是還在成形中的演算法。這時只好猜。
於是我們靠感覺和經驗猜：整個演算法如果有效，某個性質要應該成立吧。理想情況是立刻用一個歸納證明漂亮搞定。實際上，一個大定理通常無法整塊一口氣證出來，得拆成幾個輔助定理。怎麼拆呢？照經驗，並靠著對問題的了解。嗯，也許它會對，是因為這個、這個、和那個。拆成三個小性質，把最明顯、應該不會不成立的擱一旁，從問題較大的開始證。
那麼，開始歸納證明囉？硬推幾步後常會發現這樣行不通。為了歸納證明，我們得證一個更廣泛、更強的性質。廣泛化的方法很多種，要挑哪個？只好再靠經驗猜了。這是一個不斷調整的過程：你證的性質得強到可提供足夠的歸納假設，又不至於過強到證不出來。總之，分出幾個 case，推了幾步之後，開始三心二意了。這樣對嗎？
往往事情就是愛捉弄人。好不容易證完第一個補助定理、第二個補助定理，再回頭看當初擱一邊的、覺得很明顯應該會對的那個補助定理，其實是錯的。
啊，只好再重新開始了。追根究底，那是因為我們還不夠了解手上的問題。要正確地把性質切成小塊，我們得對問題有全盤的了解。但全盤的了解又根基於從每個細節的運作中學到的經驗。而人腦能同時處理的問題複雜度有限，於是只好反覆東想、西想，不知該由上往下、還是由下往上？
用 Coq, Agda 之類的證明輔助程式可能讓情況更糟糕。我原以為電腦適合證明有很多 case 的性質，因此把定理放到 Coq 或 Agda 裡，希望靠著問答和填空格就可以糊裡糊塗地把性質證出來。結果我得到的慘痛教訓是：若不先想清楚，證明輔助程式剛好賦予你在錯誤的路上走得更遠的能力。我寫了幾百行的證明，迷失在許多細節裡，才發現此路不通。也許證明還是得先在紙上做一遍吧？
等到終於找到那組對的性質，也終於確定把這問題搞懂了。證明可能不過是十幾分鐘的事情。「就這樣？」這很明顯嘛。怎麼沒早點想通呢？
這就是做我們這行研究呀。
7 Comments
"Finding out something to find out, then finding it out." OUCL 給 research students 的資料好像都很喜歡擺這句呢。不過 research student handbook 裡面也只說是 "someone once described…"。
希望靠著問答和填空格就可以糊裡糊塗地把性質證出來。結果我得到的慘痛教訓是：若不先想清楚，證明輔助程式剛好賦予你在錯誤的路上走得更遠的能力。
我做數學題目的感覺也是這樣，除非題目特別單純，否則「寫下前提試圖亂湊變出結論」註定要失敗的，得先讓直覺導引一下。老師所描述這麼漫長的進攻過程我還沒什麼經驗就是了。
話說理想情況不就是希望遇到問題可以隨便拿個形狀看起來符合的定理套一套就出來？
「就這樣？」這很明顯嘛。怎麼沒早點想通呢？
以隨機客老師的說法就是「說穿了一文不值」XD。
也實在不能說傳統 AI 方法（i.e., search with heuristics）呆，有時候那的確很忠實地模映我們的行為 XD。
『Finding out something to find out, then finding it out.』
其實我已經忘記原文了，也不記得我那年是否有印在某文件上，只記得開學時有人在台上說起。原來原文是很漂亮的句子，那中文要怎麼翻才好哩..
老師所描述這麼漫長的進攻過程我還沒什麼經驗就是了。
說不定你來證的話會快一點哩。
話說理想情況不就是希望遇到問題可以隨便拿個形狀看起來符合的定理套一套就出來？
呴呴… 今年我的另一個體會是：「做」paper 有兩種方法。第一種是找個問題，解它，把中間用到的定理記下來寫成 paper，希望這個定理會有很多應用. 第二種是找一個定理，找三個可以用這個定理解的問題，然後 claim 你發現了一個有廣泛應用的定理，值得寫成 paper.
你說的理想情況通常都只出現在第二種 paper 裡面….
以隨機客老師的說法就是「說穿了一文不值」XD。
啊，最近才和亮廷聊到，Richard Feynman 在他的自傳裡開玩笑說數學家只能證 trivial 的東西。 請找 "A Different Box of Tools" 那段。
補充一下，research student handbook 裡面的原文是
Someone once described research as ‘finding out something to find out, then finding it out’; the first part is often harder than the second.
所以老師的記性非常好…
「找出要找出的東西然後找出那東西」？XD
雖然不是在做研究，但我寫程式也往往有類似的感覺哩…
弄到最後發現走向死路，才忽然驚覺迷失在細節之中。
這時候最好的辦法還是─砍掉重練 :/
畢竟寫程式和寫證明是有道理相通之處的呀。尤其是寫函數語言的話。
我還是沒真正寫過規模很大的程式。那種複雜度就更是難以想像了。
說到這個，最近在看的 Proofs and Refutations 也有類似的情節，先是對一個問題發現一個不嚴謹策略，將問題分成幾個步驟，然後討論每個步驟的可行性，再來對每個步驟找到個別的漏洞或是原始假設的瑕疵，再修正原本問題的描述，再來看證明是否還符合或是有沒有問題，然後然後其實好像也沒有什麼有效率的策略，能夠有條有理的理性探索。:-P
書中討論的是「多面體的滿足 Euler 常數為 2」，現在是知道只有單連通多面體才符合 ，有一個有趣的過程是，有人乾脆放棄證明這個假說，乾脆把符合 Euler 常數為 2 的叫多面體！
老師這句話真的讓我思考很多，雖然已經寫到自己的 blog 上，不過還是有點想法，我花了一個學期才了解這件事就是了。持續的前進與學習吧。