9 posts
Cleanroom 驗證需要生成並消除證明義務（proof obligations）。以下說明 LLM 如何自動化註解與驗證條件（VC）的生成，讓你能專注於真正困難的證明工作。
Cleanroom 軟體工程要求你在編譯程式碼之前，先證明它是正確的。這聽起來很高尚，直到你花了三個小時為一個只排序十個整數的函式撰寫迴圈不變式（loop invariant）為止。 瓶頸不在證明本身，而在於那些繁瑣的樣板程式碼。生成驗證條件（verification…
我花了30天時間，在向LLM索取程式碼之前先撰寫設計說明。結果改變了我對rubber-ducking的看法。
大多數開發者把LLM用反了。我們用五個詞描述需求，拿回200行程式碼，然後花下一個小時除錯模型做出的假設。 我花了三個月時間執行相反的流程：在索取哪怕一行程式碼之前，先寫一份完整的設計說明。結果程式碼缺陷更少了，但真正的進步在於我自己的理解。 Donald Knuth在1984年提出了「literate…
LLM 對話包含意圖、被拒絕的替代方案以及可執行的程式碼。這正是文件應該包含的內容。以下是將 ephemeral chat 轉換為持久、可搜尋的文件，同時不遺失敘事的方法。
你花了 45 分鐘和 Claude 設計一個 retry circuit。你解釋了 failure modes，因為 exponential backoff 會掩蓋 cascading pressure 而拒絕了它，確定了 token-bucket rate limiting with…
費根審查需要四到六個人、兩小時才能審完250行程式碼。大型語言模型可以透過承擔準備工作與檢查清單的執行來削減這部分成本，但它無法取代人類角色去發現最昂貴的缺陷。
一次完整的費根審查需要一名主持人、一名朗讀員、兩到四名審查員，以及作者本人。團隊以每小時125行的速度，花費兩小時審查大約250行程式碼。這意味著一次小小的改動就要消耗八到十二人時。 大型語言模型可以在不到一秒內讀完250行程式碼。它可以執行檢查清單、標記可疑模式，並在任何人開啟檔案之前就產生一份結構化的缺陷紀錄。…
大型語言模型能寫出品質驚人的Rust程式碼，但當你要求形式化證明時，它們會幻覺出不變量，並編造出沒有任何驗證器接受的語法。本文介紹它們真正做對了什麼、在哪裡崩潰，以及如何善用牠們。
LLM能寫出可以編譯甚至通過的Rust程式碼。但牠們目前還無法可靠地寫出形式化證明，來證實程式碼對所有可能的輸入都是正確的。…
LLM 會對語法產生幻覺，因為它們以機率方式採樣 token。語法約束解碼在每一步過濾詞表，只輸出保持語法有效性的 token。
讓 LLM 產生一個 JSON 物件，它最終一定會輸出一個末尾逗號、字串裡未轉義的換行符，或者在一個本該有引號鍵的位置輸出 bare word。這個錯誤不是模型的 bug。它是自迴歸採樣工作方式的必然結果：在每一步，模型都會把自己的詞表裡每個 token 都當作候選，包括那些會讓部分輸出在語法上 invalid 的…
你可以從簡單的英語描述中生成設計令牌，但前提是將該描述視為帶有模式契約和snapshot test的限界上下文DSL。
是的，你可以用英語描述一個主題，並得到一個可用的設計系統。關鍵在於，這段英語描述不是提示詞。它是源檔案。和任何源檔案一樣，它需要編譯器、類型系統和測試。…
並行運行多個 LLM 能抓出任何單一模型都會自信上線的錯誤。以下是如何建立一個真正有效的分歧解決系統。
你把一個 prompt 送給 GPT-4o。它回傳了一個 JSON blob，信心值 0.97。你把同一個 prompt 送給 Claude 3.5 Sonnet。它回傳了另一個 JSON blob，信心值也是 0.97。兩個模型聽起來都篤定不移。兩個都在不同層面上錯了。 這不是假設情境。只要你運行任何非瑣碎的…
用 LLM 進行 N-version programming 不需要多個模型。只要改變 prompt、角色設定和推理限制，就能從單一模型中產出多樣且正確的實作。
N-version programming 的假設是：多樣性來自不同的作者。對 LLM 來說，這意味著不同的模型、不同的供應商，甚至不同的訓練版本。但這個假設是錯的。只要改變「怎麼問」，而不是「問什麼」，就能從同一個模型中獲得有意義的多樣性。 問題在於：把 temperature 調到 1.0 然後重複跑五次…