EG-VAR: 用 Lean 4 形式驗證消滅 LLM Agent 幻覺

一句話核心結論

LLM 拿到工具不代表推論就可信——現有 agent 的「實證推理」既不保證輸出真的來自工具證據，也不保證演繹鏈經得起形式檢查。EG-VAR 把 Lean 4 proof assistant 做成 agent 的形式 sidecar：Lean kernel 是唯一能鑄造「Verified」標籤的實體，所有驗證過的輸出結構性地追溯至一個工具調用（定理 3.1），且推理鏈的每一步都經 kernel type-check（定理 3.2）。120/120 TableBench，反事實壓力測試保持 100% source-faithful。

核心架構：四層信任堆疊 + 信任帳本

EG-VAR 不是要取代 LLM——而是給 LLM agent 加一個 形式治理層。四層架構：

1. L0 來源層：原始資料——CSV、API 回應、資料庫查詢結果。不可信的原始位元。
2. L1 儲存層：將表格資料結構化存入 Lean 型別系統，每一格都有型別標記。
3. L2 工具證明層：工具執行後回傳的是帶證據封條的 Lean term，例如 CellValue "Tokyo" 37400000。
4. L3 宣告層：每條宣告要嘛附上 Lean proof term（kernel 檢查通過 → Verified），要嘛誠實說 Abstain（附可重播審計軌跡）。

信任帳本（Trust Ledger）：每個推論步驟的三元組（來源範圍、證據邊界、證明義務）被記錄在案。第三方可獨立重播整個推理鏈。

兩條安全定理

定理 3.1（無憑空輸出）：任何被標記為 Verified 的宣告，其 proof term 的所有觀察節點必須對應到存在的工具調用記錄。不能宣稱「數據顯示 X」但從未查過數據。

定理 3.2（無演繹錯誤）：所有推理步驟都是 Lean 4 kernel type-check 通過的有效推導。不會有邏輯跳躍或隱含假設。

兩定理的關鍵：mkVerified 規則是唯一能鑄造「Verified」標籤的入口，要求 (a) proof term (b) kernel type-check (c) 所有 observation-leaf 有對應工具調用，三樣同時成立。

實驗設計：三層漸進式評估

Tier 1（Gold-goal）：TableBench 120 題，人工 Lean proof term。EG-VAR 120/120；same-tool 114/120（錯的 6 題全是幻覺）。

Tier 1.5（反事實壓力）：故意給錯誤來源資料。EG-VAR 100% source-faithful；same-tool 80-90%（模型用參數記憶「修正」來源）。

Tier 2（LLM 形式化器）：讓 Sonnet/Opus 自己轉 Lean proof term。Sonnet 誤差 3.3%，Opus 1.7%。97-98% 可自動形式化並通過 kernel 驗證。

對 DKY Agent 的啟發

• 網頁爬取驗證：任何「根據 XX 網站…」的宣稱，必須附 URL + HTTP 狀態 + 內容 hash。
• 工具調用審計：每次 tool call 結果注入 context 前，確認來源、時間、參數。
• Abstain 優於瞎猜：誠實說「我不知道」+ 審計軌跡，比吐出看似合理的數字有價值得多。

限制

• 目前只處理結構化表格數據，未擴展到自由文本或非結構化 API 回應
• 形式化需要人工撰寫 per-source lift，無法全自動
• LLM 形式化器的 1.7-3.3% 語義誤差在高風險場景仍不可接受
• 單作者論文，樣本量有限（120 題 TableBench 子集）