背景

本文探討在大型語言模型（LLM）時代下，如何將其不確定性的輸出轉化為具備決定性（Deterministic）的編程工具。作者藉由數學家利用 Lean 等證明系統來驗證 LLM 生成證明的案例，對比軟體開發中自動化部署與腳本的可靠性，思考如何建立一套能確保程式碼正確性且可重複驗證的開發流程。

社群觀點

針對 LLM 是否具備決定性的討論，社群呈現出技術細節與開發範式轉移兩大層面的辯論。在技術層面上，部分留言者指出 LLM 本質上並非絕對隨機，理論上可以透過固定隨機種子（Seed）與將溫度參數（Temperature）設為零來達成決定性輸出。然而，實務專家反駁指出，現代高效能推論往往依賴批次處理（Batching），這會導致 GPU 運算中的數值行為因併發狀態而產生微小差異，且推理模型（Reasoning Models）的思維鏈過程更增加了輸出的不穩定性，使得完美的決定性在生產環境中極難達成。

在開發範式的轉移上，許多討論者將 LLM 編程類比為「遺傳演算法」。開發者的角色正從編寫邏輯轉向定義「適應度函數」（Fitness Function），亦即透過撰寫精確的測試與規格來篩選 LLM 生成的變體。這種觀點認為，編程的重心已從實作細節移往環境與約束條件的建構，甚至有留言者戲稱這是一種「元編程」（Meta-programming），工程師更像是在指導一名平庸但勤奮的實習生，透過不斷的觀察、行動與驗證循環（OODA Loop）來逼近正確結果。

然而，社群中也存在顯著的質疑聲音。有評論者批評這種依賴測試來補足 LLM 缺陷的做法，本質上只是將問題轉移到測試品質上，若缺乏人類對底層邏輯的深刻理解，LLM 產生的程式碼可能只是看起來正確的「偽證」。特別是在涉及統計分析或無已知結果的開發場景中，LLM 容易產生看似合理實則錯誤的幻覺，此時若無手動編寫的基準真相（Ground Truth），任何自動化驗證工具都將失效。此外，也有人擔憂過度依賴 LLM 會導致開發者思維的「量化」與退化，使程式設計變成一種單純的規格填寫工作。

延伸閱讀

在討論串中，參與者分享了數個實踐決定性編程或結構化開發的工具與理論。其中包括 Mycelium 框架，它嘗試將程式表達為狀態圖，並由工作流引擎驗證節點間的契約；Formulize 則被提及作為尋找數據描述函數的先驅工具。此外，有開發者分享了關於 Recursive Language Models 的部署理論，以及如何透過結構化提示詞與程式碼交織（Co-recursion）來提升開發效率的技術筆記。