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
I accidentally turned LLM memory into program analysis
41–50 of 94 posts
Re: I accidentally turned LLM memory into program analysis
#42So 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.
In general, what all the big LLM providers are doing is moving towards classical & neural (neuro-symbolic) AI - even though they dont publicly admit it because that would counter their claims for years of "scale is all you need" (which has vanished with diminishing returns, see $MS / altman's GPT-5 bet).
How do you know this?
Re: I accidentally turned LLM memory into program analysis
#43Has 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
Re: I accidentally turned LLM memory into program analysis
#44So 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.
With validity intervals mentioned it'll also be nice to have LTL's "next" and "until" too.
Re: I accidentally turned LLM memory into program analysis
#45This 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…
[dead]
Re: I accidentally turned LLM memory into program analysis
#46Has 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
At one point I was using TLA+ but it just made the problem "is the spec right?" or "does the code match the spec?". I could ensure that the properties defined in the spec were valid, but that didn't seem to translate into confidence that my code was correct. Maybe I was holding it wrong, it was just an experiment in an area I'm unfamiliar with.
Ultimately I have stuck to the informal verification of defining my expectations and ensuring that tests cover them.
Re: I accidentally turned LLM memory into program analysis
#47Is 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?)
Re: I accidentally turned LLM memory into program analysis
#48Is 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?)
Yeah, philosophy of science & analytic philosophy (especially with Quine) has been down this rabbit hole before.
Formalisms should be in service to higher-level intelligences, not the other way around. It's pretty clear that LLM's are intelligent inherently; the lean doesn't just "prove math itself". (Admittedly, I'm not full blown AGI pilled either - there are some structural constraints that do make me think there is room to be gained in intelligence. And formalism will play a part in that. But it's not the end-all be-all to it).
Re: I accidentally turned LLM memory into program analysis
#49So 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.
In general, what all the big LLM providers are doing is moving towards classical & neural (neuro-symbolic) AI - even though they dont publicly admit it because that would counter their claims for years of "scale is all you need" (which has vanished with diminishing returns, see $MS / altman's GPT-5 bet).
[deleted]
Re: I accidentally turned LLM memory into program analysis
#50Datalog 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.