It’s great to see this pattern of people realising that agents can specify the desired behavior then write code to conform to the specs. TDD, verification, whatever your tool; verification suites of all sorts accrue over time into a very detailed repository of documentation of how things are supposed to work that, being executable, puts zero tokens in the context when the code is correct. It’s more powerful than ream…
Leanstral: Open-source agent for trustworthy coding and formal proof engineering
151–160 of 234 posts
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#152Curious if anyone else had the same reaction as me This model is specifically trained on this task and significantly[1] underperforms opus. Opus costs about 6x more. Which seems... totally worth it based on the task at hand. [1]: based on the total spread of tested models
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#153Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#154Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#155Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#156Earlier quoted context omitted.
This would be unfortunately a rather nuclear option due to the continent’s insane reliance on technology that breaks its unenforced laws.
How about not making these unenforced laws in the first place so that European companies could actually have a chance at competing? We're going to suffer the externalities of AI either way, but at least there would be a chance that a European company could be relevant. The AI Act absolutely befuddled me. How could you release relatively strict regulation for a technology that isn't really being used yet and is in the…
Speaking as someone who's been doing stats and ML for a while now, the AI act is pretty good. The compliance burden falls mostly on the companies big enough to handle it.
The foundation model parts are stupid though.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#157Earlier quoted context omitted.
The scientific approach is not only or primarily empiricism. We didn't test our way to understanding. The scientific approach starts with a theory that does it's best to explain some phenomenon. Then the theory is criticized by experts. Finally, if it seems to be a promising theory tests are constructed. The tests can help verify the theory but it is the theory that provides the explanation which is the important par…
> The scientific approach starts with a theory that does it's best to explain some phenomenon At the risk of stretching the analogy, the LLM's internal representation is that theory: gradient-descent has tried to "explain" its input corpus (+ RL fine-tuning), which will likely contain relevant source code, documentation, papers, etc. to our problem. I'd also say that a piece of software is a theory too (quite literal…
Vibing gives you something like the geocentric model of the solar system. It kind of works but but it's much more complicated and hard to work with.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#158Earlier quoted context omitted.
The scientific approach is not only or primarily empiricism. We didn't test our way to understanding. The scientific approach starts with a theory that does it's best to explain some phenomenon. Then the theory is criticized by experts. Finally, if it seems to be a promising theory tests are constructed. The tests can help verify the theory but it is the theory that provides the explanation which is the important par…
The theory still emanated from actual observations, didn't it ?
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#159It’s great to see this pattern of people realising that agents can specify the desired behavior then write code to conform to the specs. TDD, verification, whatever your tool; verification suites of all sorts accrue over time into a very detailed repository of documentation of how things are supposed to work that, being executable, puts zero tokens in the context when the code is correct. It’s more powerful than ream…
Be careful here - make sure you encode the right details. I've seen many cases where the tests are encoding the details of how it was implemented and not what it is intended to do. This means that you can't refactor anything because your tests are enforcing a design. (refactor is changing code without deleting tests, the trick is how can you make design changes without deleting tests - which means you have to test as much as possible at a point where changing that part of the design isn't possible anyway)