Lemmalog: 使用 Datalog 將 LLM 記憶轉化為程式分析

在長期調查中維持一致的狀態是 LLM agent 的主要失效模式。在漏洞研究等複雜任務中，模型往往會忘記先前已被排除的假設，或者繼續根據已被證偽的觀察結果進行推理。Lemmalog 透過將 LLM 記憶視為程式分析問題而非檢索問題，並使用 Datalog 引擎來維持確定性的演繹狀態，來解決此問題。

問題：LLM 記憶中的狀態衰減

標準的 LLM 記憶系統通常依賴向量資料庫和語義檢索 (RAG)。雖然對於檢索相關的過去對話非常有效，但這些系統在處理「真理」和狀態更新方面表現不佳。如果一個 agent 確立了 object_a 指向 object_b，隨後發現這是錯誤的，向量資料庫只會簡單地儲存這兩個矛盾的陳述。LLM 隨後必須在提示詞中調和這些矛盾，這往往會導致幻覺或已失效假設的復甦。

Lemmalog 的架構：分離模糊邏輯與確定性邏輯

Lemmalog 將記憶問題拆分為兩個截然不同的組件：用於提取的機率性前端，以及用於推理的確定性後端。

1. 模糊前端 (LLM)

LLM 被用作解析器，將非結構化數據（例如原始碼、除錯器輸出和自然語言筆記）轉換為結構化事實。例如，像「LLDB shows that the freed object is later reused」這樣的陳述會被轉換為正式事實：freed(object_a) 和 reused_as(object_a, write_target)。

2. 確定性後端 (Datalog)

一旦事實被結構化，Lemmalog 就使用 Datalog（一種宣告式邏輯程式語言）根據預定義的規則來推導新事實。這確保了結論是邏輯上合理的，並且會自動更新。

關鍵能力包括：

  • 增量評估 (Incremental Evaluation)： 當輸入事實發生變化時，只有受影響的結論會被更新，而不是重新執行整個調查。
  • 自動撤回 (Automatic Retractions)： 如果用於推導結論的事實被移除，除非該結論有另一個獨立的推導路徑支持，否則該結論會自動失效。
  • 來源追蹤 (Provenance Tracking)： 系統為每個推導出的事實維護一個依賴圖，允許 agent 回答「為什麼」特定結論是正確的，透過追溯到其原始觀察結果。
  • 時間有效性 (Temporal Validity)： 事實與有效性區間相關聯（例如，viable(primitive_a) [10:14, 12:37)），允許系統追蹤知識如何隨時間演變，而不會維持矛盾的狀態。

效能基準測試

Lemmalog 針對 LongMemEval 和 LoCoMo 基準測試進行了測試，以評估其處理長期對話記憶的能力。

LongMemEval 結果

Lemmalog 達到了 0.463 +/- 0.010 的 F1 分數和 0.575 +/- 0.004 的準確度。雖然略微落後於某些專門的記憶系統（如 PropMem），但它顯著優於全上下文提示 (GPT-4.1)，後者的 F1 分數為 0.197。

至關重要的是，Lemmalog 大幅降低了上下文窗口的需求。對於 LongMemEval，回答模型收到的資訊量大約為 2,700 tokens per question，而全上下文方法則需要 104,000 tokens——上下文大小減少了 38 倍。

LoCoMo 結果

在規模更大的 LoCoMo 基準測試（1,986 個問題）中，Lemmalog 達到了 0.533 +/- 0.001 的 F1 分數，在專門的記憶系統中排名第三。與全上下文模型（0.509 F1）相比，它在 對抗性問題 (adversarial questions)（0.707 F1）中表現尤特別出色，因為結構化記憶可以明確地識別出缺乏支持事實的情況，而不是被語義相似性所誤導。

比較：演繹狀態 vs. 情節式記憶

Lemmalog 提出了一種用於 agent 記憶的混合架構，區分了演繹狀態與情節式記憶：

特徵 演繹狀態 (Lemmalog) 情節式記憶 (Vector DB)
性質 事實、規則、時間 模糊上下文
機制 來源追蹤與撤回 語義檢索
儲存 維持的狀態 原始文本
優勢 邏輯一致性、真理 相關性、細微差別

社群洞察與反對意見

技術同行之間的討論突顯了這種方法的潛力與歷史背景：

"LLMs should only really sit at the terminals of request fulfilment... Between those terminals, the work should be mechanical reasoning over some ontology or formal knowledge structure."

一些貢獻者指出，這種方法反映了「傳統 AI (GOFAI)」和符號 AI，並警告說該系統最終可能面臨符號邏輯的經典挑戰，例如對量詞的需求以及處理「模糊」或基於觀點的資訊的困難度。

結論

Lemmalog 演示了對於需要邏輯一致性和狀態追蹤的任務，維持一個正式的分析狀態比增加上下文窗口更有效。透過將 LLM 作為確定性 Datalog 引擎的機率性解析器，該系統降低了 token 成本並防止了已證偽假設的復甦，為長期自主研究 agent 提供了一條可擴展的途徑。

Sources

相關