6 posts
Differential testing 讓你在不知道正確答案的情況下找到 bug。問題是，有相關性的錯誤看起來就像一致。以下是找出盲點的方法。
你可以信任 differential testing，即使沒有形式化證明——但前提是你必須清楚知道它會在什麼地方崩潰。 它的弱點叫做 common-mode failure。當一個規格的每個實作都做出同樣的錯誤假設時，它們全部一致通過，你的 test harness 就會標為通過。N-version…
N-version programming 假設你的實作結果一致。我們來看看為什麼測試不夠、SMT solver 如何真正證明等價，以及該在「夠好就好」和「形式化驗證」之間劃下哪條界線。
你建了一個 n-version 系統。同一個關鍵函式的三份獨立實作、一個選出多數結果的 voter，以及一種自己已經搞定單點故障的溫暖感覺。 你並沒有證明這些函式是等價的。你只證明了它們編譯得過。 N-version programming 的概念是：如果其中一個實作有 bug，其他的大概不會有，所以 voter…
並行運行多個 LLM 能抓出任何單一模型都會自信上線的錯誤。以下是如何建立一個真正有效的分歧解決系統。
你把一個 prompt 送給 GPT-4o。它回傳了一個 JSON blob，信心值 0.97。你把同一個 prompt 送給 Claude 3.5 Sonnet。它回傳了另一個 JSON blob，信心值也是 0.97。兩個模型聽起來都篤定不移。兩個都在不同層面上錯了。 這不是假設情境。只要你運行任何非瑣碎的…
N-version programming 聽起來很簡單：跑多個實作，挑最好的答案。但在實務上，「最好」比「最常見」難定義得多。
你有同一個函式的五種實作。三個回傳相同的結果。一個稍有不同。一個拋出例外。哪一個才是對的？ 大多數團隊預設採用多數決。當輸出完全一致且錯誤顯而易見時，這麼做沒問題。但只要你的實作在細微處出現分歧，或每個變體都回傳不同答案時，這套方法就會崩解。N-version programming…
用 LLM 進行 N-version programming 不需要多個模型。只要改變 prompt、角色設定和推理限制，就能從單一模型中產出多樣且正確的實作。
N-version programming 的假設是：多樣性來自不同的作者。對 LLM 來說，這意味著不同的模型、不同的供應商，甚至不同的訓練版本。但這個假設是錯的。只要改變「怎麼問」，而不是「問什麼」，就能從同一個模型中獲得有意義的多樣性。 問題在於：把 temperature 調到 1.0 然後重複跑五次…
N-version programming 曾宣稱獨立團隊會犯下獨立的錯誤。Knight 與 Leveson 在 1986 年的實驗證明了相反的事實，NASA 也默默退出了這條路。
1980 年代初期，NASA 面對一個至今仍困擾著安全關鍵工程領域的問題：你該如何容忍那些還沒被發現的漏洞？他們的答案是 N-version programming。把同一份規格交給三個獨立團隊。同時執行三份程式。對輸出結果進行投票。如果其中一個團隊寫出了漏洞，另外兩個會以多數票壓過它。…