深度分析
在 Lean4 上以多代理系統實現教科書自動形式化：AutoformBot 與 ATLAS
在大型語言模型大量產出的當下，數學論證的機械驗證成為顯學。研究提出AutoformBot，一個以多階層代理（數千個LLM實例）與Lean4形式化工具為核心的管線，結合依賴感知排程、版本控制與自動化評鑑，將教科書敘述轉為機器檢驗的定義與證明。
ATLAS
ATLAS
ATLAS 架構與 Adaptive-OPRO：將 LLM 推理轉為可審計訂單級交易決策
金融市場決策具延遲回饋與高噪音挑戰。本研究提出ATLAS框架，整合市場、新聞與基本面三類資訊，並以Adaptive-OPRO做序列化提示優化，引導中央交易代理輸出可執行訂單。實驗顯示Adaptive-OPRO在多種市場條件下優於固定提示，反思機制未必帶來一致收益。
速報
ATLAS：以LLM串接威脅建模與形式驗證的SoC安全框架
背景：為提升SoC安全，本研究將標準化威脅模型與形式驗證結合。方法：ATLAS以LLM從CWE辨識資產、對應弱點並自動產生assertion與JasperGold腳本，將弱點推理轉為形式證明。結果：於三項HACK@DAC基準上偵測39/48個CWE並為33項漏洞生成正確性質。