Lean4Agent：面向智慧體工作流與軌跡的形式化建模與驗證
本文提出Lean4Agent，據我們所知，這是首個使用依賴型別形式語言Lean4來建模和驗證大語言模型智慧體行為的框架。它包含FormalAgentLib庫和LeanEvolve最佳化工具，實驗表明透過驗證的工作流效能平均提升11.94%，LeanEvolve進一步將軟體工程任務效能提升7.47%。
近年來，大語言模型（LLM）在多步工作流執行中的可靠性成為人工智慧領域的核心挑戰。儘管LLM的智慧體能力不斷進步，但大多數智慧體系統仍缺乏用於指定、驗證和除錯工作流及執行軌跡的形式化方法。這一困境與數學中長期存在的問題相似——自然語言的歧義性推動了形式語言的發展。受此啟發，來自多所機構的研究人員提出了Lean4Agent，據我們所知，這是首個使用依賴型別形式語言Lean4來建模和驗證智慧體行為的框架。
Lean4Agent的核心元件是FormalAgentLib，這是一個可擴充套件的Lean4庫，能夠對智慧體工作流進行形式化建模，並在顯式假設下驗證其語義一致性。更重要的是，該庫可以定位執行軌跡中揭示的執行時故障，為開發者提供清晰的除錯方向。基於FormalAgentLib，研究團隊進一步開發了LeanEvolve，該工具利用驗證結果自動修訂工作流，從而增強智慧體的整體能力。
為了評估Lean4Agent的有效性，研究者在SWE-Bench-Verified的困難子集和ELAIP-Bench子集上進行了大量實驗，涉及5種主流LLM，包括GPT-4、Claude等。結果顯示，透過形式化驗證的工作流相比未透過的版本效能平均高出11.94%。此外，應用LeanEvolve進行工作流修訂後，軟體工程任務（SWE）效能平均進一步提升7.47%。這些資料充分證明了形式化方法在智慧體工作流最佳化中的巨大潛力。
Lean4Agent的提出為使用表達能力豐富的依賴型別形式語言來形式化建模和驗證智慧體行為奠定了堅實基礎，開闢了一個全新的研究方向。未來，這一框架有望被擴充套件以處理更復雜的多智慧體協作場景，並與其他形式化工具整合，從而推動可靠AI系統的構建。該論文於2026年6月2日提交至arXiv，標誌著依賴型別形式語言在AI智慧體驗證領域的重要突破。