這項由伊利諾伊大學厄巴納-香檳分校與獨立研究者聯合開展的研究，於2026年6月以預印本形式發布，論文編號為arXiv:2606.06523，有興趣深入了解的讀者可通過該編號查詢完整論文。
研究的起點，是一個困擾了整個AI行業很久的難題：大語言模型（就是ChatGPT這類能對話的AI）在幫我們做複雜任務的時候，怎麼才能保證它按照我們期望的方式一步步走下去，而不是在某個環節悄悄出錯，最後交給我們一個看似完整實則一塌糊塗的結果？
現有的AI系統大多依靠"感覺"來評估自己的工作——要麼讓另一個AI來評分，要麼由人工檢查。這兩種方式都有明顯的軟肋。AI評分容易自我感覺良好，在長達數十步的複雜任務中尤其容易出現幻覺；人工檢查則耗時費力，根本跟不上實際需求。
這個問題在數學界早就遇到過，而且有了成熟的解決方案。數學家在證明複雜定理時，也面臨同樣的困境：自然語言描述的證明過程，越長越容易出錯，越難驗證。於是他們發展出了"形式化語言"——一種嚴格到不能有任何歧義的數學語言，可以讓電腦自動檢查每一步邏輯是否正確。Lean4就是這樣一種語言，被數學界廣泛用於證明驗證。
研究團隊由此受到啟發：能不能把這套方法搬到AI工作流的驗證上來？由此誕生了這項研究的核心框架——**Lean4Agent**。簡單來說，這是第一個用形式化數學語言來給AI工作流"做體檢"的系統，能在AI執行任務之前，就幫你發現工作流設計中隱藏的邏輯漏洞；在執行過程中，還能精確定位哪一步出了問題。
一、AI工作流究竟是什麼，為什麼它需要被"體檢"
要理解這項研究，先得弄清楚"工作流"是什麼意思。把AI完成一個複雜任務的過程，比作一個工廠的生產流水線：流水線的每一道工序都有固定的輸入原料和輸出產品，工序之間有明確的先後順序，有些工序可以並行，有些需要循環重複，還有些需要根據情況做分支判斷。AI工作流就是這樣一條"生產線"——它規定了AI應該先做什麼、再做什麼、用哪些資訊、產出什麼結果。
研究團隊將工作流正式定義為一張"異構圖"，圖中的每個節點代表一個執行步驟，節點之間的連線代表步驟的先後關係或數據流向。每個節點有四個要素：它讀取哪些變量、寫入哪些變量、用自然語言寫成的執行指令，以及它的執行類型。執行類型這個概念很關鍵——比如有的步驟是"step"類型，會帶著整個對話歷史來執行；有的是"task"類型，每次都是全新的獨立執行，沒有記憶。這個區別聽起來小，但在實際運行中會導致截然不同的結果，也是工作流設計中非常容易出錯的地方。
與此同時，AI的實際執行過程被定義為"執行軌跡"——就像工廠流水線運轉時留下的生產日誌，記錄了每一道工序執行前後的狀態、用了什麼指令、產出了什麼內容。研究的目標就是：既要在流水線運轉之前檢查設計圖是否合理，也要在運轉過程中盯住每一步是否按照設計圖執行。
二、三層體檢機制：從結構到語義，再到實際運行
Lean4Agent的核心組件叫做**FormalAgentLib**，這是一個用Lean4語言編寫的形式化庫，目前包含151個類型定義、611個函數，以及41個已經過嚴格驗證的定理。整個體檢過程分為三個層次，就像醫院體檢時先做基礎檢查、再做功能檢查、最後做應激測試一樣。
第一層檢查的是工作流的"骨架"是否完整，稱為結構驗證。這一層不管AI的智能水平高低，只看流程圖畫得對不對。研究團隊在Lean4中定義了一套基礎類型系統，其中最重要的是變量類型（BaseType）和步驟類型（StepType）。BaseType涵蓋了字符串、整數、浮點數、布爾值、JSON格式數據、列表、字典、集合等常見數據類型，還有一個特別的"TUnknown"類型用於處理類型不確定的情況，支持漸進式類型檢查。StepType則區分了十幾種不同的步驟類別，包括帶歷史記憶的step、不帶記憶的task、結構化輸出的discover、質量評分的evaluate、條件判斷的validate、循環控制的forEachLoop和whileLoop等等。
結構驗證能發現的典型錯誤，是論文中一個生動的案例：一個工作流使用了parallel步驟，讓四個AI分支並行搜索，分別產生了results_q1、results_q2、results_q3、results_q4四個結果。然而設計者忘記了，parallel分支內部的變量有自己的"作用域"——就像工廠里幾條並行的小生產線，線上產出的產品沒有被匯集到主幹線。結果後續的合併步驟想讀取這四個變量時，系統發現根本找不到這些數據的來源，直接報錯：allReadResolvable = false。這種問題在人工審查時極容易被忽視，但Lean4的native_decide機制（一種自動判定機制）可以立刻發現。
第二層檢查的是工作流的"語義"是否自洽，稱為靜態語義驗證。這一層要回答的問題是：每一步AI任務的執行，有沒有足夠的"前提條件"，能不能產出預期的"後置條件"？這裡借鑑了電腦科學中一個經典的思想框架——霍爾邏輯（Hoare Logic），簡單來說就是：在執行某個操作之前，某些條件必須成立；操作執行之後，另一些條件應當成立。
為了讓這套邏輯能處理AI的模糊性，研究團隊設計了一套謂詞系統（Predicate System）。謂詞就是關於變量的可驗證性質描述，比如"這個變量是非空字符串"、"這個變量是合法的JSON格式"、"這個變量符合某個特定的JSON模式"、"這個文件路徑是有效的"等等。這些謂詞被實現為Lean4中的歸納類型PredicateType，每個謂詞都有一個toProp函數，能把謂詞轉化為可驗證的Lean命題。系統還支持用戶自定義謂詞（通過ext和custom類型），不需要修改核心代碼就能擴展。
更精妙的地方在於"隱式變量"的處理。不是所有的語義要求都體現在明面上的變量里——比如"上下文流暢性"這個性質，描述的是某個步驟能不能看到之前執行的對話歷史，這不是一個具體的變量，而是整個執行圖上的結構性質。資訊流謂詞追蹤每個步驟消耗了什麼資訊、產出了什麼資訊；上下文管理謂詞則規定了哪些步驟可以看到哪些歷史記錄。這些圖級別的謂詞能夠捕捉到那些即使是人工審查也容易錯過的隱性設計缺陷。
整個語義驗證的基石是一個叫做**LLMExec**的假設。這個假設說的是：如果一個AI步驟在滿足前提條件的情況下被執行，那麼它能夠產出滿足後置條件的結果。這聽起來像是在說廢話，但其實非常重要——它把對整個複雜工作流的驗證，分解成了對每一個單獨步驟的驗證。每個步驟的語義規格由LLM自動標註，而標註的合理性建立在"LLM能夠正確執行短期、局部的任務"這一經驗性觀察之上。多倫多大學等機構的研究也支持這一點：大語言模型在短小、明確的任務上表現可靠，問題通常出在跨步驟的資訊傳遞和長鏈推理上。
有了LLMExec假設，驗證過程就變成了一個謂詞傳播過程：從工作流的初始參數出發，把每個步驟已知的前置謂詞收集起來，判斷下一個步驟所需要的前置條件是否已經被滿足，再把該步驟產出的後置謂詞加入到謂詞庫中，如此傳播下去。如果在某個步驟發現它所需要的某個謂詞沒有任何前驅節點建立過，那就說明這個工作流存在語義缺口。
論文中展示了一個非常典型的語義錯誤案例：一個用於回答學術論文問題的工作流，其中find_evidence步驟產出了evidence_pack變量，JSON格式包含"snippets"欄位，每個snippet有"text"和"source"兩個子欄位。然而後續的compose_answer步驟卻期望evidence_pack包含"passages"欄位（每個passage有"quote"和"page"兩個子欄位）以及一個"summary"欄位——這些欄位壓根沒有任何前驅步驟建立過。這種JSON欄位不匹配的問題，在運行時會悄無聲息地導致答案生成失敗，但Lean4驗證在運行前就能精確指出：Node compose_answer (ID 3): missing predicate matchesJsonSchema(...) for variable 'evidence_pack'。
第三層檢查在實際運行之後進行，針對的是具體的執行軌跡，稱為軌跡驗證。這一層的目標是驗證LLMExec假設在特定一次執行中是否真的成立，從而精確定位是哪一步的執行出了問題。對於有精確定義的謂詞（比如JSON格式驗證），直接用Lean命題來判斷；對於需要網路連接才能驗證的謂詞（比如URL有效性檢查），調用外部Python驗證器；對於只有自然語言描述的模糊謂詞，則調用LLM-as-judge模組進行判斷。LLM法官還可以利用任務執行環境產生的反饋資訊，比如軟體工程任務中單元測試的錯誤資訊，來輔助判斷。
三、讓工作流"自我進化"的LeanEvolve機制
發現了問題只是第一步，更有價值的是能夠修復問題，甚至讓工作流自動變得更好。建立在FormalAgentLib之上的**LeanEvolve**，就是這樣一套工作流進化機制。
LeanEvolve的工作場景是這樣的：一個工作流通過了第二層的語義驗證，說明它的設計在邏輯上是自洽的；但在某次實際執行中，它沒有產出正確的結果。這時候LeanEvolve登場，利用第三層軌跡驗證的結果，找到那個讓整個任務失敗的關鍵步驟，以及它違反了哪些謂詞條件，然後把這些診斷資訊提供給一個LLM代理，讓它有針對性地修改那個步驟的指令描述。修改完成後，用修改後的工作流重新執行同一個問題，看看能不能解決。
這種"有根據的修改"被稱為formal-guided evolve（形式化引導進化）。與之對比的是pure-LLM evolve（純LLM進化）——後者不用任何形式化分析，直接把執行軌跡和任何可用的環境反饋丟給LLM，讓它憑感覺改工作流。實驗結果清楚地顯示了兩者的差距，但這裡先按下不表，留到實驗部分一併講述。
對於像軟體工程這樣有豐富測試反饋的任務，LeanEvolve還可以開啟"純LLM進化"附加模式，作為形式化引導進化的補充。這個模式不依賴形式化分析，而是做更大範圍的探索性修改，適合處理一些"走偏路"才能解決的問題。兩種模式結合，形成了一個更全面的進化機制。
四、在真實任務上的測試：數字背後的故事
研究團隊在兩類完全不同的任務上測試了Lean4Agent，這個選擇本身就很有意思：軟體工程任務（SWE）代表了"LLM密集型"任務——工作流設計相對簡單，但需要AI大量自主探索、調試和修改代碼；AI論文理解任務代表了"工作流密集型"任務——工作流的精細設計直接決定了效果好壞，AI的發揮空間相對受限。
軟體工程任務使用的是SWE-Bench-Verified這個基準，它收集了真實的GitHub問題，每個問題都有單元測試可以客觀判定是否解決。研究團隊從中挑選了50個"硬題"——那些通常需要人類工程師超過一小時才能解決的問題。論文理解任務使用的是ELAIP-Bench，包含從最新AI論文中提取的403道多項選擇題，研究團隊隨機選取了100道進行實驗。
實驗的設計方式是：讓一個強大的AI（Claude-Opus-4.6）生成40個候選工作流，過濾掉格式不合規的，然後對通過格式檢查的工作流進行第二層語義驗證，隨機選取3個通過驗證的和3個未通過驗證的，分別用於五個主流大模型（GPT-5.2、GLM-5、Kimi-K2.5、Gemma-4-31B、Qwen-3.5-27B）在兩個基準上的測試。這樣的設計可以分離工作流質量的影響，也能測試結論是否跨模型穩定。
結果令人信服。在軟體工程任務上，通過驗證的工作流平均正確率為58.27%，未通過驗證的工作流平均正確率僅為43.47%，差距達到14.80%。更重要的是，這個差距在統計上顯著，95%的自舉置信區間為[10.00%, 19.60%]，完全不包含零。在論文理解任務上，通過驗證的工作流平均得分36.60%，未通過的27.53%，差距9.07%，置信區間[5.66%, 13.07%]同樣在零以上（除了Qwen-3.5-27B這一個模型在該任務上的結果置信區間跨越了零，可能因為這個模型在此任務上基線就較強）。
一個有趣的觀察是：對於參數量較小的模型，驗證帶來的提升效果更大。比如Gemma-4-31B在軟體工程任務上，通過驗證的工作流比未通過的高出了27.33%。這說明工作流質量對能力相對較弱的AI更加重要——工作流設計得好，能在一定程度上彌補模型本身能力的不足。
研究團隊還額外測試了Claude 4.5 Opus，結果顯示通過驗證的工作流準確率67.33%，未通過的56.67%，絕對提升10.67%，證明結論能夠跨不同來源的模型推廣。
在LeanEvolve的效果上，五個模型在軟體工程任務上平均額外解決了7.47%的問題，將綜合準確率從56.93%提升到64.40%。其中Qwen-3.5-27B提升最大（10.67%），GPT-5.2次之（8.00%），GLM-5提升相對最小（4.67%）。在論文理解任務上，對比形式化引導進化和純LLM進化的直接效果：五個模型平均而言，形式化引導的方式比純LLM方式多解決了7.00%的初始失敗案例，充分說明有了精確的錯誤定位，修改才更有的放矢。
五、細節揭秘：那些容易被人忽視的隱性錯誤
論文花了相當篇幅介紹兩個具體的錯誤案例，這兩個案例很好地說明了為什麼形式化驗證能捕捉到人工審查容易遺漏的問題。
第一個案例來自軟體工程任務。有一個工作流由五個步驟組成：setup_and_explore（探索代碼庫）、reproduce_issue（復現問題）、implement_fix（實現修復）、verify_fix（驗證修復）、submit_patch（提交補丁）。這五個步驟全都是task類型，也就是說每個步驟執行時都沒有對話歷史的記憶。然而verify_fix步驟的指令里寫道，要根據之前實現的修復來驗證效果——但task類型根本看不到"之前"，每次都是全新開始。FormalAgentLib通過隱式變量的資訊流謂詞系統發現了這個問題：verify_fix步驟需要fix_implementation_evidence這個謂詞，但因為沒有對話歷史，這個證據實際上並不在當前的執行上下文中。解決方法很簡單：把task類型改成step類型，讓步驟能看到歷史記錄。改完之後，GPT-5.2在50道硬題上的準確率從52%提升到62%。
第二個案例來自論文理解任務。有一個工作流設計了evaluate_A、evaluate_B、evaluate_C、evaluate_D四個步驟，分別獨立評判四個答案選項，聽起來非常合理——獨立評判能避免先入為主。然而這四個步驟使用的是step類型，也就是說每個步驟都能看到之前步驟的對話歷史！這意味著evaluate_B執行時，已經看到了evaluate_A的評判過程，獨立性根本無法保證。FormalAgentLib的evaluateChoicesIndependent謂詞捕捉到了這個矛盾：工作流設計的意圖是獨立評判，但step類型的上下文共享機制破壞了這一意圖。
第三個案例是LeanEvolve在軟體工程任務django_15098上的表現。原始工作流在執行中，AI只看到了錯誤的表面症狀，沒有追溯到import鏈中的根本原因，修複方案錯誤，單元測試失敗。第三層軌跡驗證精確定位到verify_fix步驟：Lean驗證確認fix_verification_evidence變量存在（非空字符串），但外部工具驗證發現兩個單元測試最終失敗，LLM法官也確認了測試失敗這一事實。診斷資訊進一步指出：工作流錯誤地把修復當成已驗證的，儘管失敗的測試仍然存在。基於這個診斷，LeanEvolve修改了verify_fix步驟的指令，要求AI追蹤完整的錯誤調用鏈，使用精確的FAIL_TO_PASS測試路徑來驗證，而不是遇到表面上的"修復成功"就停止。修改後的工作流在下一次執行中通過了測試。
六、消融實驗：拆解各個組件的貢獻
為了弄清楚是哪些部分真正起了作用，研究團隊還做了消融實驗。第一個消融實驗是去掉第二層驗證中的圖級別謂詞，只保留針對單個變量的謂詞。在論文理解任務的40個工作流中，原本有21個未通過完整的第二層驗證；去掉圖級別謂詞後，只有8個仍然失敗，說明有13個工作流的錯誤完全依靠圖級別謂詞才能被檢測到。最常見的違反謂詞是makeUnifiedJudgement和unifiedLoopBack，這些都是只有從整個工作流圖的視角才能看到的一致性要求，單看某個節點是發現不了的。這個實驗有力地證明了圖級別謂詞的不可替代性。
第二個消融實驗是在軟體工程任務上去掉LeanEvolve中的純LLM進化附加模式，只保留形式化引導進化。結果顯示，去掉純LLM進化後，平均提升從7.47%降到5.07%，減少了2.40%。說明純LLM進化確實貢獻了一部分價值，主要是在需要探索性修改或非常規解法時；但形式化引導進化才是主要驅動力，貢獻了絕大部分提升。
研究團隊還對比了Lean形式化驗證與"LLM-as-judge"（用另一個AI來評判工作流質量）的效果。在工作流質量相對容易判斷的論文理解任務上，LLM法官的評分與Lean驗證結果大體吻合；但在判斷標準更模糊、依賴實際執行的軟體工程任務上，LLM法官的評分與Lean驗證結果幾乎毫不相干，而且與實際執行效果的關聯也很弱。檢查發現，LLM法官通常只能看到工作流的顯式行為，對隱式資訊流、上下文可見性、圖級別謂詞等深層次問題視而不見——恰恰是這些深層次問題，才是形式化驗證真正能發揮作用的地方。
七、研究的局限性與未來的路
研究團隊坦誠地列出了幾個局限性，這讓整項研究顯得更為可信。大語言模型的內部行為是黑箱，無法被完全檢視；Lean4Agent的方式是把它分解成可驗證的步驟，並對每個步驟的語義做出假設，但這些假設本身也可能不完全準確。其次，工作流的謂詞標註是由另一個LLM（Claude-Opus-4.6）自動完成的，LLM有時會標註出錯誤的謂詞，儘管標註完成後的Lean驗證是嚴格的，但錯誤標註會導致驗證基礎出現偏差。此外，現代大語言模型生成的工作流很少出現明顯的結構性錯誤，這使得第一層結構驗證的效果難以通過大規模定量實驗來評估，目前主要靠案例研究來展示。
從更宏觀的視角看，這項研究開闢了一個新方向：用具有表達能力的依賴類型形式化語言來建模和驗證AI代理系統。時序邏輯等傳統形式化方法無法處理數據依賴的屬性；SMT（可滿足性模理論）方法難以表達高階推理；而Lean4作為一種依賴類型語言，能夠同時表達數據類型依賴的性質、高階邏輯和複雜推理鏈，是目前已知表達能力最強的形式化驗證工具之一。將這種工具引入AI代理驗證領域，是這項研究最具開創性的貢獻。
說到底，這項研究告訴我們一件頗為反直覺的事：給AI"打草稿"的工作流，比AI本身更值得仔細雕琢。一個邏輯自洽、資訊流清晰的工作流，能讓即使能力相對一般的AI也發揮出遠超預期的水平；而一個充滿隱性矛盾的工作流，則會讓再強大的AI也頻繁犯錯。研究團隊用數學證明的嚴格性，給這個樸素的觀察找到了一個可量化、可操作的實現路徑。下一次當你設計一個多步驟的AI應用，也許真正值得思考的問題不只是"用哪個模型"，而是"這個工作流的邏輯真的通順嗎"。
---
Q&A
Q1：Lean4Agent驗證的是什麼，和普通測試有什麼區別？
A：Lean4Agent使用形式化數學語言Lean4對AI工作流進行三層驗證：結構層檢查變量讀寫是否一致、流程圖是否合法；語義層檢查每個步驟的前置條件是否能被滿足、後置條件是否會被建立；軌跡層在實際執行後檢查LLM是否真的按照規格執行了。普通測試只能發現已經發生的錯誤，而這套方法能在運行前就發現邏輯缺陷，並能精確定位問題所在的步驟。
Q2：FormalAgentLib檢測到的錯誤，人工審查能發現嗎？
A：論文展示的案例說明，很多錯誤人工審查很難發現。比如把task步驟誤用在需要歷史上下文的場景中，或者評判選項的步驟因為使用了step類型而失去了獨立性——這些錯誤不看執行類型的底層語義就很難察覺。實驗中LLM法官（用GPT-5.5來評判工作流質量）在軟體工程任務上和實際執行效果幾乎沒有關聯，說明這類深層次的隱性矛盾確實超出了一般評審的感知範圍。
Q3：LeanEvolve是如何自動修復工作流的，它每次都有效嗎？
A：LeanEvolve利用第三層軌跡驗證的結果，找到具體失敗的步驟和違反的謂詞，把這些診斷資訊交給LLM來修改那個步驟的指令，然後重新執行。它不是每次都有效，實驗顯示平均額外解決了7.47%的問題，對於需要追蹤完整錯誤鏈或跨文件修改的情況效果最好。對於那些需要非常規探索才能解決的問題，LeanEvolve中附加的純LLM進化模式會補充更廣泛的修改嘗試，兩者結合比任何一種單獨使用效果都更好。
