Lemmalog: LLMエージェントに脆弱性調査用の段階的で事実ベースの記憶を提供するためのDatalogの活用

まとめ

Lemmalogは、LLMの文脈を単純に再再生するのではなく、構造化された事実を保存・削除・推論するDatalogエンジンを用いることで、トークン使用量を大幅に削減し、LongMemEvalやLoCoMoなどのベンチマークにおける知識更新性能を向上させます。


問題点:LLMは現在正しい事実を忘れてしまう

脆弱性調査を支援するLLMエージェントは、大規模なコードベースを正しくナビゲートし、攻撃ベクトルを提案できます。しかし数時間後、モデルはすでに否定された仮定が何だったかを忘れ始めます。その結果、以下のようなことが起こります:

  • すでに除外されたアプローチを再提案する。
  • 偽の観察から継続的に推論を続ける。
  • 修正された事実を、トランスクリプト内で先に出現したためまだ正しいと扱う。

従来のメモリソリューションは、会話全体を保存するか、過去のメッセージを埋め込み、最も関連性の高いスニペットを検索します。これは過去の情報を検索するには有効ですが、取得された事実が現在の知識状態を反映しているとは保証されません


メモリをプログラム解析として再定義する

プログラム解析は、事実(例:calls(foo, bar))と規則(例:トランジティブな呼び出し到達可能性)のセットを維持します。固定点計算によりすべての可能な結論を導出し、入力が変更された際には影響を受ける事実のみをインクリメンタルに更新します。

LLMエージェントにこのアプローチを適用することで、明確な目標が得られます:

  • 現在の事実のセットを維持する。
  • 結論を自動的に導出する。
  • 新たな証拠によって反証された場合、事実を削除し、依存する結論に変更を伝播させる。

Lemmalogの紹介

Lemmalog (https://github.com/JordyZomer/lemmalog) は上記のアイデアを実装しています:

  1. 曖昧なフロントエンド – LLMが自然言語入力(デバッガー出力、ソースコード、メモ)を原子的な事実に解析します。
  2. 決定論的なバックエンド – Datalogエンジンがこれらの事実を格納し、ユーザー定義の規則を適用し、導出された事実を計算します。
  3. インクリメンタルな更新 – 事実の追加は前方推論をトリガーし、削除は後方再帰をトリガーし、まだ有効な導出を保持します。
  4. 証拠追跡 – 各導出された事実は、サポートする事実と規則の正確な連鎖を記録しており、「なぜ?」というクエリに対応できます。
  5. 時間的区間 – 事実に有効期間を付与でき、例えば「primitive_a は現在有効ですか?」や「なぜ以前は有効だと考えたのですか?」といったクエリが可能になります。

削除と複数の導出の扱い

Datalogエンジンは、事実が真である理由を知る必要があります。次の例を考えてみましょう:

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

a が削除されても、b がまだ c を導出しているため、c は真のままです。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は2番目の問題を解決しますが、ベクトルストアは1番目の問題(生のスニペットの意味的検索)に使用できます。この2つのレイヤーは互いに補完し合い、実際にはよく組み合わせられます。


ベンチマーク評価

LongMemEval(102の質問)

指標 Lemmalog PropMem SimpleMem Full‑Context GPT‑4.1
F1 0.463 ± 0.010 0.550 0.480 0.197
Accuracy 0.575 ± 0.004
クエリあたりのトークン数 ~2.7 k ~104 k

Knowledge‑Update(脆弱性調査に最も類似したカテゴリ)では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は専用メモリシステムの中で3位ですが、クエリあたりのトークン数が約6倍少ない(3.4 k vs. 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

これらのコメントは、コミュニティが曖昧な抽出と決定論的推論の分離を有望な方向性と見ていることを裏付けています。


時間経過によるトークン節約

ループ数 フルコンテキストのトークン/クエリ Lemmalogのトークン/クエリ
50 ~100 k ~2.5 k
100 ~200 k ~2.5 k
500 ~1 M ~2.5 k

Lemmalogのクエリサイズは一定のため、コンテキストウィンドウの制限に達することなく、任意に長い調査にスケーリングできます。


結論

Lemmalogは、プログラム解析技術——事実、規則、インクリメンタルな固定点計算、証拠追跡——が、LLMエージェントにおける単純なトランスクリプト再生を置き換えることができることを示しています。このシステムは:

  • 自動的に無効化された事実を削除することで、現在の状態を正確に保ちます。
  • トークン数が桁違いに少ない、安価で説明可能なクエリを提供します。
  • 標準化されたメモリベンチマークにおける知識更新性能を向上させます。

結果はまだ最先端ではありません(PropMemが全体でリードしていますが)、しかし利点はより大きなモデルではなく、具体的なCSソリューションのエンジニアリングから得られています。次のステップは、Lemmalogを実際の数時間にわたる脆弱性調査で実行し、本当に死んだ仮説が再浮上することを防ぎ、幻覚的な関係を減らすかどうかを測定することです。

ソースコードは https://github.com/JordyZomer/lemmalog で公開されています。

Sources

関連

  • プロジェクト
  • プロジェクト
  • Dispatch
  • Dispatch
  • Dispatch