I reached a similar conclusion: LLMs should only really sit at the terminals of request fulfilment.

1. User request understanding: natural language -> a more rigorous representation, in my case Datalog.

2. Result interpretation: facts and derived facts -> natural language.

Between those terminals, the work should be mechanical reasoning over some ontology or formal knowledge structure.

That connects to another principle I've been thinking about, which I call Weathering: useful reasoning should change the shape of the system. If an LLM has already had to infer a relation, mapping, rule, or abstraction, repeated use should wear that inference into the system so that the next similar request doesn't require discovering it again from scratch.

With continued use, a weathering-capable system should therefore require less and less probabilistic intelligence for recurring work. Put another way, there should be a declining marginal cost of cognition since the products of intelligence harden into structure that can subsequently be reused and evaluated mechanically.

So he's using an LLM to generate data stored in an "is_a" representation. That's so classic AI.

Soon, he'll discover that he needs quantifiers. Then that "for all" is too strong sometimes, and he needs "for most". That way lies Cyc.

It's not a bad idea. But it does have a history.

Datalog seems like a way to "spell" knowledge graph (KG).

The article touches on Datalog statements changing over time. One ingredient I think would be good to add to the system is to make every statement carry "providence" metadata. The providence should be sufficient to enable later confirmation that a statement is still valid or if the statement needs to be reformed without the need to remake the entire graph from scratch.

I would make at least some forms of providence follow a strict schema that is defined for the subject matter that is being captured. For example, statements about a code base should refer to the source files and their version (file modification date, content hash) from which the statements were concluded. When a source file is modified we may then find all statements made from them and reevaluate just those statements.

The next level would be to keep statements even if reevaluation breaks them and add a method to derive a subgraph for a given state of the subject. For example, over many releases of a code base, a lot of statements would not change, some would. Having a graph that spans all conclusions about all releases of a code base and a way to form the subgraph for a specific release would allow the system to efficiently target queries for a particular release.

I recently stumbled upon the technique of asking the LLM to create a Dot Viz (or mermaid) flowchart of the program flow.

The LLMs are great at:

- understanding the flow

- making diagrams

- running the code with logging they add to to even better understand the flow

The flow being in Dot (or other machine readable format) makes it even easier for the LLM to use that as a reference going forward.

Is this the kind of thing that works when you have a tight domain-specific language, but devolves into natural language (English) eventually?

E.g. A -> B, B -> C so A -> C (works, great). A -> B when A is sort of red and blue, also A is intermittent (what to do now?)

Very cool. I recall an HN submission (which I can't find offhand unfortunately) that did something similar -- it used an LLM to decompose articles into a set of statements which were used to construct an entity-relationship graph of facts and events. It then queried that using conventional graph query methods, much like DataLog / Lemmalog is doing here. I remember it was particularly effective at answering timeline-based queries that LLMs (back then) sucked at.

(See also Cyc: https://en.wikipedia.org/wiki/Cyc)

I think approaches like this are going to be (or maybe already are?) the basis of effective grounding of LLM responses in authoritative data sources. It should be possible to pinpoint any error to an incorrect traversal or an incorrect "fact." This would work best for concrete, unambiguous facts, however; fuzzy, ambiguous or opinion-based information will probably remain the purview of LLMs.

This really matches up to my experience on long research projects with Claude.

It’s very hard to remove information - Claude has a habit of recording things all over the place and will happily treat things as facts even after they’ve been disproved.

What is currently true can get easily contaminated with old “facts”.

This is the fact I’ve been struggling with for quite some time. It’s not because it forgets the facts, it’s because the invalidation doesn’t propagate.

My way of handling that is a decision log. For every project since I started doing that it’s working great. My CLAUDE.md instruct the agent to store my every decision to the file with a metadata when I made this decision and what was the context. The agent is using this file as an index of decisions and rarely lose a track. It also helps team members to find out more about the development phases.

Does your system invalidate the parts of the memory if these are not valid or relevant anymore or just store/retrieve?

Something of this capacity would be useful in investigating obscure hardware failures in the logs that I couldn't confirm because the problem was not being observed while the device was in my shop. the problem was surfacing in another location probably due to some set of circumstances in the software that I could recreate, or some particular peripherals that were attached.

I ran into the very same problem of the LLM forgetting that we ruled out a conclusion that was verified not to be the cause as it came up further in the conversation history while I was exploring possibilities.

I had to keep reminding we ruled out that conclusion prior.. I just carried on with having the LLM capture some of the supporting sources of other people experiencing the same problem and kept having to refine those sources because it was focused only on summaries, but eventually i got the sources to a point where they were good enough hypothesis that we could formulate a better conclusion on what the potential cause was.

> The LLM handles the fuzzy part: > And Lemmalog handles the deterministic part:

There seems to be this view in some circles that the LLM should do EVERYTHING. The most extreme version of this was "just commit the prompt, bro".

The more I've used LLMs, the more I think that the LLM should do either:

1. the fuzzy parts as mentioned in the post

2. helping to write deterministic tools to expand the "non-fuzzy" part

For #2, we invented code to run the same instructions the same way over and over again for very, very low cost. The code is also easy to read and modify as needed.

Why we would replace the above with a smart but stochastic system still seems strange to me.

I had tried to get long term memory out of Claude by indexing my notes with keywords and putting that in a sqllite database and Claude queries using full text search. Don't know how good it is, it seems to find things alright. My goal was to keep context small and only get Claude to ask for what it needs. Datalog seems like a great idea, will definitely try it out

This summer I’ve been investigating agentic coding with local LLMs, and while I’m far from an expert, one thought that has been on my mind is leveraging techniques from “old-school” AI such as heuristic search to guide agents when it comes to planning. The use of Datalog in this article resonates with me, since logic programming was a major part of old-fashioned symbolic AI. I’m very curious about this combination of “old-school” AI and LLMs.

Has anyone tried formal verification with AI generated code? I can't convince my company to use it but I realise it's very easy to ask Claude to add a verification step locally on my own PRs

You should checkout cave lang [0] - terse language that explores this area of knowledge/graph/ontology/provenance/querying/confidence/solver etc.

[0] https://mirekrusin.com/cave

Eventually lambda prolog will rise again

Great work! If anyone is looking for a way to integrate something like this into their own harness or the pi coding agent, then you might be interested in DeepClause [0]. It comes with a Prolog-like language implemented on top of SWI-Prolog (WASM Version). The purpose of the project is to allow for broad experimentation around the intersection of LLMs/Agents and GOFAI. So you could use it to build memory systems like OP did, create executable specs, define graphs and loops for agents and subagents... It also comes with a pi extension that greatly simplifies getting started with it.

Opposed to OP, DeepClause uses Prolog semantics, so running some more complex queries on knowledgebases might cause some issues (which is the use case where a Datalog might be more useful). For smaller scales it should be fine though.

[0] https://github.com/deepclause/deepclause-sdk [1] https://github.com/deepclause/deepclause-pi

Interesting and potentially has applicability in deriving logical rules from regulation, contracts etc. Are there already formal languages that can be used to codify, that sort of information.

yooo.. this is exactly what I wanted to do... I'm so happy because (a) I hadn't figured out how to do it (b) it seemed kind of difficult in general and (c) now I don't have to, lol.

I was trying to connect to wifi on a fresh macOS install without only a keyboard connected last week.

After googling for an hour, I gave up.

Very cool article. I had a similar idea where "fact checking" should be real programs for logic correctness.

But IRL it's too vague. The exploit hunting is a better use case.

It seems like you might be inventing a form of non-monotonic logic. Check out answer set programming, it actually does exactly what you want of "unlearning" facts that you've learned. Not sure if it helps in your particular instance, but it's very cool stuff and IIRC there is an implementation that extends datalog. https://en.wikipedia.org/wiki/Answer_set_programming

Limitation of LLM for and toward reverse engineering; it's the LLM innate error of forgetting states thru agentic recursion by overflow of context or prior premises being optimized away due to not using ternary-state (uninit/written/read) memory state.

Once again, on LLM being: a digital librarian, at its finest; logic a logic analyst, not so much.

Ctrl-F “prolog”: 0 result. :-/

This was a pretty awesome read, I liked it a lot!

What I found out during malware analysis is that LLM agents have a couple of quirks that you can solve by:

- optimize for short lived agent workflows

- use symbols as function contracts

- maintain decision and discovery state

- give LLMs CLI linters

- give LLMs access to knowledge bases

The linter part is mindblowing. I built linters that validate HTML or markdown or docx or Go or C files, for example, and they output what kind of structure is expected instead of useless token based errors (e.g. h4 inside h1? Must be h1 > h2 ...).

With linters the output quality of agents is just soo much better.

For program analysis, I'm currently exploring the idea of using an external ebpf daemon that programs can be observed with via a public API (which is the tool for the agent to use). Not sure if it'll do the trick yet, but I think it has lots of potential.

My stuff in case you're interested:

[1] https://github.com/cookiengineer/exocomp

[2] https://github.com/cookiengineer/gobayashi

[3] https://github.com/cookiengineer/gonano

Is this sort of re-inventing Graph RAG from another angle, or does it feel novel?