Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Leanstral: Open-source agent for trustworthy coding and formal proof engineering

mistral.ai

Post reply on HN
Print view View original

181–190 of 234 posts

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#181

Post by jasonjmcghee »

naasking wrote: post #172
hobofan wrote: post #103

Earlier quoted context omitted.

Sorry, but what are you talking about? This is a 120B-A6B model, which isn't runnable on any laptop except the most beefed up Macbooks, and then will certainly drain its battery and cook your legs.

You can easily run a quant of this on a DGX Spark though. Seems like a small investment if it meaningful improves Lean productivity.

Is it though?

Most people I know that use agents for building software and tried to switch to local development, every single time they switch back to Claude/codex.

It's just not worth it. The models are that much better and continue to get released / improve.

And it's much cheaper unless you're doing like 24/7 stuff.

Even on the $200/m plan, that's cheaper than buying a $3k dgx or $5k m4 max with enough ram.

Not to mention you can no longer use your laptop as a laptop as the power draw drains it - you'd need to host separately and connect

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#182

Post by TimTheTinker »

naasking wrote: post #173
TimTheTinker wrote: post #68

Earlier quoted context omitted.

Presumably the idea is that an agent generates a Lean4 specification against which the software is measured. But then the Lean4 specification effectively becomes the software artifact. And we're sort of back to square 1. How do you verify a Lean4 spec is correct (and that it describes what needs to be built in the first place) without human review?

> And we're sort of back to square 1. Specifications are smaller than the full code, just as high level code is smaller than the functionally equivalent assembly. As we ascend the abstraction ladder the amount of reading a human needs to do decreases. I don't think this should really count as "back to square 1".

That has always been the perceived promise of higher-abstraction software specs: automated code generation from something higher-level, thus making programmers increasingly obsolete.

  binary => hexadecimal instructions
  hexadecimal => assembly language
  assembly => portable, "high-level" languages (C, FORTRAN, COBOL, etc.)
  HLLs => 3GLs (BASIC, C++, Pascal, Java, C#, JavaScript, etc.)
  3GLs => 4GLs/DSLs/RADs and "low-code/no-code"[0]
Among the RADs is Microsoft Visual Basic, which along with WinForms and SQL was supposed to make business programmers nearly obsolete, but instead became a new onramp into programming.

In particular, I'd like to highlight UML, which was supposed to mostly obsolete programming through auto-generated code from object-oriented class diagrams.[1] The promise was that "business domain experts" could model their domain via visual UML tooling, and the codegen would handle it from there. In practice, UML-built applications became maintenance nightmares.

In every one of these examples, the artifact that people made "instead of programming" became the de-facto programming language, needing to be maintained over time, abstracted, updated, consumed behind APIs, etc. -- and programmers had to be called in to manage the mess.

It's interesting that Spec4 can be auto-generated, then used to generate code. My question is - what do you do when you have (a) consumers depending on a stable API, and (b) requests for new features? Maybe hand the job to Claude Code or a human developer with a suite of unit tests to guarantee API compatibility, but at that point we're back to an agent (LLM or human) doing the work of programming, with the Spec4 code as the programming language being updated and maintained.

[0] https://en.wikipedia.org/wiki/Fourth-generation_programming_...

[1] https://news.ycombinator.com/item?id=26934795

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#183

Post by auggierose »

AlotOfReading wrote: post #166
auggierose wrote: post #122

Earlier quoted context omitted.

You are confusing the proof with the spec/theorem. A correct proof and a valid proof are the same thing. It doesn't really matter how long the proof is, and you don't even need to understand it for it to be correct, the machine can check that. But indeed, if the spec includes 8.7k of C code, that is problematic. If you cannot look at the theorem and see that it is what you mean, that is a problem. That is why abstrac…

I'm not confusing them. That's why I gave each of the numbers for SeL4 separately. Knowing whether those theorems are the right theorems for the problem can be as difficult as understanding the implementation itself. Hence the example of SeL4 where the number of theorems exceeds lines of code in the original implementation and the formal model is large. It's my experience that most people doing formal methods have se…

I think you have been confusing them. Two theorems are the same if they have the same statement (spec). A proof is not a theorem, nobody cares about when two proofs are the same or not.

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#184

Post by andai »

patall wrote: post #18
andai wrote: post #13

Earlier quoted context omitted.

This is called a "LLM alloy", you can even do it in agentic, where you simply swap the model on each llm invocation. It does actually significantly boost performance. There was an article on here about it recently, I'll see if I can find it. Edit: https://news.ycombinator.com/item?id=44630724 They found the more different the models were (the less overlap in correctly solved problems), the more it boosted the score.

That sounds quite interesting. Makes me wonder if sooner or later they will have to train multiple independent models that cover those different niches. But maybe we will see that sooner or later. Thanks for the link.

Mixture of Mixtures of Experts ;)

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#185

Post by warpspin »

tin7in wrote: post #163
warpspin wrote: post #143

Earlier quoted context omitted.

The problem with the European independence story is, that it seems Mistral runs its own stuff also on US cloud act affected infrastructure. This makes them a very weird value proposition: If I accept a level of "independence" whereby I run on AWS or Azure, I could as well pay for Anthropic or GPT to have SOTA performance. If I do not accept that level of independence but want more, I need to buy what's on OVH, Scalew…

They are building their own infra - south of Paris and another one was announced in Sweden recently.

Then why does their list of subprocessors list Google and Microsoft "for cloud infrastructure", specifically for "Le Chat, La Plateforme, Mistral Code"? Sounds to me as if they're mainly running on Azure.

Also, they're listing CoreWeave as inference provider in "EEA" area, but CoreWeave is of course also an US company. Even if they have their data center physically in the EU, it must be considered open access for the USA due to the CLOUD act.

https://trust.mistral.ai/subprocessors

If what you say is true, they have a communications problem and they need to fix that urgently. Right now, this is why they don't get my business. Others will have made the same decision based on their own subprocessor list.

Or did you mean, they're like, right now building it and plan to move there, but it's not up yet?

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#186

Post by andai »

Aerroon wrote: post #91
cyanydeez wrote: post #22

Earlier quoted context omitted.

One would think that LoRAs being so successful in StableDiffusion, that more people would be focused on constructing framework based LoRas; but the economics of all this probably preclude trying to go niche in any direction and just keep building the do-all models.

The SD ecosystem in large part was grassroots and focused on nsfw. I think current LLM companies would have a hard time getting that to happen due to their safety stuff.

Fine-tuning does exist on the major model providers, and presumably already uses LoRA. (Not sure though.)

We saw last year that it's remarkably easy to bypass safety filters by fine-tuning GPT, even when the fine-tuning seems innocuous. e.g. the paper about security research finetuning (getting the model to add vulnerabilities) producing misaligned outputs in other areas. It seems like it flipped some kind of global evil neuron. (Maybe they can freeze that one during finetuning? haha)

Found it: Emergent Misalignment

https://news.ycombinator.com/item?id=43176553

https://news.ycombinator.com/item?id=44554865

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#187

Post by boyoboy »

discreteevent wrote: post #158
ptidhomme wrote: post #141

Earlier quoted context omitted.

The theory still emanated from actual observations, didn't it ?

It did but they were meaningless without a human intellect trying to make sense of them.

[dead]

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#188

Post by andai »

teekert wrote: post #110
andai wrote: post #3

Trustworthy vibe coding. Much better than the other kind! Not sure I really understand the comparisons though. They emphasize the cost savings relative to Haiku, but Haiku kinda sucks at this task, and Leanstral is worse? If you're optimizing for correctness, why would "yeah it sucks but it's 10 times cheaper" be relevant? Or am I misunderstanding something? On the promising side, Opus doesn't look great at this benc…

I also don't understand the focus on vibe coding in the marketing. Vibe coding kind of has the image of being for non-devs, right? I do like agents (like Claude Code), but I don't consider myself to be vibe coding when I use them. Either I'm using a language/framework I know and check every step. OR I'm learning, checking every step and asking for explanations. I tried vibe coding, and really dislike the feeling I ha…

Yeah, the original meaning of Vibe Coding was "not looking at the code, just going on vibes", but a lot of people now use it to mean "AI was involved in some way".

I see a whole spectrum between those two. I typically alternate between "writing code manually and asking AI for code examples" (ChatGPT coding), and "giving AI specific instructions like, write a function blarg that does foo".

The latter I call Power Coding, in the sense of power armor, because you're still in control and mostly moving manually, but you're much stronger and faster.

I like this better than "tell agent to make a bunch of changes and come back later" because first of all it doesn't break flow (you can use a smaller model for such fine-grained changes so it goes very fast -- it's "realtime"), and second, you don't ever desync from the codebase and need to spend extra time figuring out what the AI did. Each change is sanity-checked as it comes in.

So you stay active, and the code stays slop-free.

I don't hear a lot of people doing this though? Maybe we just don't have good language for it.

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#189

Post by naasking »

jasonjmcghee wrote: post #181
naasking wrote: post #172

Earlier quoted context omitted.

You can easily run a quant of this on a DGX Spark though. Seems like a small investment if it meaningful improves Lean productivity.

Is it though? Most people I know that use agents for building software and tried to switch to local development, every single time they switch back to Claude/codex. It's just not worth it. The models are that much better and continue to get released / improve. And it's much cheaper unless you're doing like 24/7 stuff. Even on the $200/m plan, that's cheaper than buying a $3k dgx or $5k m4 max with enough ram. Not to…

A single DGX Spark can service a whole department of mathematicians (or programmers), and you can cluster up to 4 of them them to fit very large models like GLM-5 and quants of Kimi K2.5. This is nearing frontier-level model size.

I understand the value proposition of the frontier cloud models, but we're not as far off from self-hosting as you think, and it's becoming more viable for domain-specific models.

Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering

#190

Post by chriswarbo »

cowboy_henk wrote: post #149
chriswarbo wrote: post #127

Earlier quoted context omitted.

Tests (and type-checkers, linters, formal specs, etc.) ground the model in reality: they show it that it got something wrong (without needing a human in the loop). It's empiricism, "nullius in verba"; the scientific approach, which lead to remarkable advances in a few hundred years; that over a thousand years of ungrounded philosophy couldn't achieve.

This only holds if you understand what's in the tests, and the tests are realistic. The moment you let the LLM write the tests without understanding them, you may as well just let it write the code directly.

> The moment you let the LLM write the tests without understanding them, you may as well just let it write the code directly.

I disagree. Having tests (even if the LLM wrote them itself!) gives the model some grounding, and exposes some of its inconsistencies. LLMs are not logically-omniscient; they can "change their minds" (next-token probabilities) when confronted with evidence (e.g. test failure messages). Chain-of-thought allows more computation to happen; but it doesn't give the model any extra evidence (i.e. Shannon information; outcomes that are surprising, given its prior probabilities).

Post reply on HN