Lemmalog：使用 Datalog 為 LLM 代理提供增量式、基於事實的記憶，用於漏洞研究

簡要說明

Lemmalog 是一種基於 Datalog 的記憶層，用於 LLM 代理，將觀察結果儲存為結構化事實，透過邏輯規則推導結論，並自動撤銷無效的事實，從而大幅縮小查詢上下文（2–3 k tokens 對比 >100 k），在 LongMemEval 和 LoCoMo 基準測試中表現競爭力。

問題：LLM 會遺忘當前為真的資訊

當 LLM 代理協助漏洞研究時，它能正確導航大型程式碼庫並提出攻擊向量。然而，數小時後，模型開始遺忘哪些假設已被證偽。它可能會：

重新建議已被排除的方法。
繼續從錯誤的觀察進行推理。
因為某個修正的事實出現在對話早期，而仍視為正確。

傳統的記憶解決方案會儲存整個對話，或將過去訊息嵌入並擷取最相關的片段。這對尋找過去資訊有效，但 無法保證 擷取的事實反映當前的知識狀態。

將記憶重新定義為程式分析

程式分析維持一組事實（例如 calls(foo, bar)）和規則（例如傳遞呼叫可達性）。固定點計算推導出所有可能的結論，而增量演算法僅在輸入變更時更新受影響的事實。

將此應用於 LLM 代理，可明確目標：

維持一組當前的事實。
自動推導 結論。
撤銷當新證據推翻時的事實，並將變更傳播至依賴的結論。

引入 Lemmalog

Lemmalog（https://github.com/JordyZomer/lemmalog）實現上述概念：

模糊前端 – LLM 解析自然語言輸入（除錯器輸出、原始碼、筆記）為原子性事實。
確定性後端 – Datalog 引擎儲存這些事實，套用使用者定義的規則，並計算衍生事實。
增量更新 – 新增事實會觸發前向推理；移除事實會觸發後向撤銷，保留任何仍有效的推導。
來源追蹤 – 每個衍生事實記錄完整的支援事實與規則鏈，支援「為什麼？」查詢。
時間區間 – 事實可標註有效性時間窗，支援如「primitive_a 目前是否可行？」或「我們為什麼早先認為它可行？」等查詢。

處理撤銷與多重推導

Datalog 引擎必須知道某事為真的原因。考慮：

a.
b.
c :- a.
c :- b.

若 a 被移除，c 仍為真，因為 b 仍可推導它。Lemmalog 記錄所有推導路徑，因此移除僅會消除其最後支援事實消失的結論。

這類似於漏洞研究中，候選攻擊可能有多個獨立的原始能力；只要所有支援原始能力未被證偽，候選攻擊仍具可行性。

來源：提出「為什麼？」

由於 Lemmalog 記錄依賴圖，使用者可要求任何衍生事實的論證。範例輸出：

candidate_3_is_exploitable
|
+-- attacker_controls_pointer
|   |
|   +-- observation_41
+-- pointer_reaches_target
+-- observation_57
+-- rule_12

若 observation_41 後來被證偽，系統會自動撤銷頂層結論。

時間性事實與有效性區間

事實可隨時間改變，而不必完全刪除。Lemmalog 將其表示為：

viable(primitive_a) [10:14, 12:37)
not_viable(primitive_a) [12:37, ...)

查詢可針對當前狀態，或探討導致過去決策的 歷史推理，且無需在同一邏輯世界中儲存矛盾的事實。

為何不直接使用向量資料庫？

向量儲存擅長擷取相關的過去片段，但無法：

檢測擷取的事實是否已被撤銷。
將撤銷的影響傳播至依賴的結論。
在無額外邏輯的情況下回答「目前什麼為真？」。

Lemmalog 解決第二個問題，而向量資料庫仍可用於第一個（原始片段的語意擷取）。兩層互補，實務上常結合使用。

基準測試評估

LongMemEval（102 個問題）

指標	Lemmalog	PropMem	SimpleMem	Full‑Context GPT‑4.1
F1	0.463 ± 0.010	0.550	0.480	0.197
准確率	0.575 ± 0.004	–	–	–
每查詢 token 數	~2.7 k	–	–	~104 k

知識更新（最類似漏洞研究的類別）得分 0.579，超越 PropMem（0.528），遠高於完整上下文（0.202）。

LoCoMo（1,986 個問題）

系統	F1
PropMem	0.605
OpenClaw	0.557
Full‑Context	0.542
Lemmalog	0.533 ± 0.001
Hindsight	0.489
Graphiti	0.416
Memory‑R1	0.389
SimpleMem	0.358

Lemmalog 在專用記憶系統中排名第三，同時每查詢使用 約 6 倍少的 token（3.4 k 對比 18.9 k）。

從基準測試中學到的教訓

實體解析 – 將提及標準化（例如「Honda Civic」與「the Civic」）可防止產生虛假的獨立事實。
日期處理 – 將擷取的日期轉換為可比較的整數，修復了重大時間推理錯誤。
聚合可見性 – 行數統計被過度嚴格的詞幹提取器過濾掉；公開它們後恢復了正確答案。
閱讀器指令 – 「若無單一事實包含答案則拒絕」的過度嚴格設定導致許多假陰性；將「無支援前提」與「需聚合」分離後解決了此問題。

所有改進均為工程層級修正，非模型擴展。

前端比你以為的更重要

最大的性能提升來自更好的 資訊擷取 和 實體整合，而非更聰明的 Datalog 評估器。將自然語言準確解析為正確謂詞是瓶頸；一旦事實乾淨，邏輯引擎便能免費承擔繁重工作。

此方法仍不足之處

條件或機率知識 – 純 Datalog 是單調的；像「除非與朋友同行，否則偏好安靜餐廳」等細膩陳述在扁平化後會失去細節。
推論／軟性推理 – Lemmalog 在 LoCoMo 的推論類別中 F1 為 0.164，落後於 PropMem（0.289）。加入條件規則或混合模糊邏輯層可彌補此差距。
多會話擷取 – 失敗常因遺漏事實而非推理錯誤；提升擷取器的覆蓋率對真實世界長時間代理至關重要。

架構概覽

LLM（模糊前端） ──► 提取事實 ──► Lemmalog（Datalog 引擎）
      ▲                                 │
      │                                 ▼
   自然語言 ◄─── 顯示事實與來源 ──► 答案生成

代理記憶 = 結構化事實 + 來源。
情節記憶 = 原始片段、嵌入向量、BM25/圖提升。
查詢路徑 = 擷取相關事實 → 執行小型 Datalog 片段 → 讓 LLM 將結果轉回自然語言。

社群反應（選摘 HN 評論）

"LLM 應坐在請求履行的終端上；中間層應是像 Datalog 一樣嚴謹的表示法。" – @sim04ful

"我試過將 Claude 的筆記索引到 SQLite，僅查詢模型需要的部分；Datalog 看起來是下一步的絕佳選擇。" – @akkad33

"這類似於早期 AI 嘗試（Cyc、知識圖譜），但搭配現代 LLM 前端進行模糊擷取。" – @keeda

"最大的痛點是移除資訊；Lemmalog 的明確撤銷解決了我每天面對 Claude 遺忘已被證偽事實的問題。" – @iamflimflam1

這些評論強化了社群認為 模糊擷取與確定性推理的分離 是一個有前景的方向。

隨時間推移的 token 節省

回合數	完整上下文 token/查詢	Lemmalog token/查詢
50	~100 k	~2.5 k
100	~200 k	~2.5 k
500	~1 M	~2.5 k

由於 Lemmalog 的查詢大小保持不變，它能無限擴展至長時間調查，而不會觸及上下文視窗限制。

結論

Lemmalog 表明，程式分析技術——事實、規則、增量固定點計算與來源——可取代 LLM 代理的 naïve 對話重播。此系統：

透過自動撤銷無效事實，保持當前狀態的準確性。
提供低成本、可解釋的查詢，token 數量減少數個數量級。
在標準化記憶基準測試中提升知識更新表現。

結果尚未達到最尖端（PropMem 仍整體領先），但收益來自具體的工程性電腦科學解決方案，而非更大的模型。下一步是將 Lemmalog 運行於真實的多小時漏洞調查中，並衡量其是否真能防止已死假設的復活，並減少幻覺關係的產生。

原始碼可於 https://github.com/JordyZomer/lemmalog 取得。