Unreadable
266 karma · joined June 6, 2018
Just had a thought: two local models, one with static weights trained mostly in the space of manipulating neural network weights, manipulating the weights of a dynamic LLM to enable learning.
I was going through an experiment trying to spec out a simple caching system in Lean. I was getting Gemini to help me run through doing this, step by step. At one point it writes out this statement with a proof to show something, the specifics of which I forget, but it was some simple property of the cache. I stare at it for a while thinking to myself this can't be right, it was some sort of plain tautological statement that didn't really say anything, like saying 1 = 1.
I give it to Opus 5.5 and it basically confirmed my gut feeling that it was useless.
I'd like to rely more on formal verification. I like the idea of starting out with specs in a formal setting and designing software that way. The problem is it's hard to do right, and my point is even with AI, it's hard to do right.
How do you actually know what the LLM proved is what you want?
Scaling up to this kind of complexity even with AI is still a challenge, at least for me.
Can we use it to specify module meanings and laws, to make the design precise and checkable, and would allow us to implement property based tests for those laws in our implementation. Lean becomes a tool for more precise thinking about the design.
Consider the number 37. On its own, it is merely data. Say that it represents millions of dollars of investment exposure: that adds context."
Who can even read this? People, please, put some effort into what you publish.
Personally I have a some tools that build dependency graphs (C# and Python) and store the results in a local database. Agents seem quite good at poking at this and coming up with refactor ideas. Graph analysis tools are useful here, simple application will detect cyclical dependencies, but I encourage the agents to use more complex tools like clustering to poke at the data.