Lemmalog：使用 Datalog 为 LLM 代理提供增量式、基于事实的记忆，用于漏洞研究

TL;DR

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 代理的朴素对话重播。该系统：

通过自动撤回被证伪的事实，保持当前状态的准确性。
提供廉价、可解释的查询，token 数量减少数个数量级。
在标准化记忆基准测试中提升知识更新性能。

结果尚未达到最先进水平（PropMem 仍整体领先），但收益来自工程化的具体 CS 解决方案，而非更大模型。下一步是将 Lemmalog 应用于真实、多小时的漏洞调查，测量其是否真正防止了已死假设的复活，并减少幻觉关系的产生。

源代码可在 https://github.com/JordyZomer/lemmalog 获取。