9 ms·

Leanstral 1.5: Proof abundance for all

374 points by programLyrique 3mo ago

boulos 3mo ago
This is nice work, but I found the bug finding example to be weird: > One such bug was in the sign function for zigzag decoding of the datrs/varinteger library. On input Std.U64.MAX, the expression (value + 1) overflowed, causing crashes in debug mode and silent corruption in release mode—an edge case that testing and fuzzing would typically miss. In what way would this boundary condition case be considered something that "testing [...] would typically miss"? It's certainly something that bad tests would miss or not think about, but I find that (a) careful people and (b) ML coding systems are actually really good at "oh, I should test the extreme values". Especially for things that parse user input. I'm curious if they found other bugs that were more interesting, but found them too hard to explain quickly.
- pierrefermat1 3mo ago
  [flagged]
  - fjdjshsh 3mo ago
    I feel this is a lazy, straw-manning comment.
- fjdjshsh 3mo ago
  Maybe it's not something they would "typically miss", but, from proof by existence, it's something they sometimes miss. It does speak to the benefits of using lean in that you don't need to be clever about the different examples you test.
- Exoristos 3mo ago
  Yes, it's basic QA. If tests missed this kind of thing, they would be of much more limited use than we generally expect them to be. It raises questions about the authors' background.
- Groxx 3mo ago
  particularly "and fuzzing", yea. fuzzing generally does intentionally explore boundary values, from what I've seen. for an encoding library like this, I think it's fair to say that fuzzing is a baseline expectation for any decent code, and it almost certainly would've caught this in seconds. --- edit concretely, I made a very simple round-trip test with proptest, and got dozens of failures and this in less than a second: thread 'signed_round_trip' (50528) panicked at tests/test.rs:72:1: Test failed: attempt to multiply with overflow. minimal failing input: value = 4611686018427387904 successes: 2 local rejects: 0 global rejects: 0
- Quekid5 3mo ago
  Because this is garbage PR. That's it. Every property-based testing system (invented ca. 1980) will explore boundary values. The semantics (or lack thereof) of C and C++ can make this difficult to actually test for because the compiler is allowed to say "test passed" to any input leading to UB.
  - vlovich123 3mo ago
    Property based testing is good at generating boundary values for inputs. But for any more complicated piece of code getting boundary value coverage of interior values is an open problem that requires instrumentation feedback to understand branch coverage and value coverage of the code that got tested. It’s not an easy thing at all.
  - teiferer 3mo ago
    > The semantics (or lack thereof) of C and C++ can make this difficult to actually test for because the compiler is allowed to say "test passed" to any input leading to UB. I get what you are saying but does this actually apply to a test? If the code under test is in one compilation unit and the test harness in another and they are linked together then the UB optimization issue ends at the API boundary and can't possibly make the test pass ..?
    - Quekid5 2mo ago
      It's definitely less likely with that technique (in practice!), but still very possible, via e.g. ODR violation or even the classic SIOF. So, ideally you'd want each separate test case to be compiled separately, but even then you wouldn't be safe! ... because any UB in that test (or the code it's testing!) could lead to a random pass. UB is good in some ways, but other ways it's really really bad. EDIT: I will say: If you have a UBSAN turned on for testing, etc. you're reasonably safe... but not fully. There's a lot of stuff they don't catch because it's essentially impossible.
satvikpendem 3mo ago
I also submitted the HuggingFace link itself here: https://news.ycombinator.com/item?id=48779902 https://news.ycombinator.com/item?id=48779902
nullc 3mo ago
It would be nice if special purpose models provided a some diverse examples of exactly the input required to get its expected performance on a mix of problem types. Maybe also a document intended for LLMs to read that advises on prompt construction. I've found that you can get wildly different quality results from these sorts of models due to seemingly insignificant differences in prompt construction. It would be much easier to guess at what it wants if I could just see some RL transcripts -- and so the model author is in a much better position to provide initial advice.
moonset 3mo ago
I gave Codex with GPT-5.5 High this prompt: Identify bugs in [datrs/varinteger](https://github.com/datrs/varinteger) . Do NOT look at the GitHub issues, just inspect the source It also found the bug that Leanstral 1.5 found and the authors highlighted. I think this bug wasn't especially tricky; it's just a case of too few eyeballs on this repo. Congrats on the release regardless! Excited for the direction Lean + automated AI proofs are headed. Disclosure: I work at OpenAI.
- 8note 3mo ago
  the mechanism is whats interesting, rather than whether it could do it. this sounds like a great tool to add to the toolbelt, as part of the "how do we handle all the code output from LLMs" problem
- noperator 3mo ago
  Leanstral 1.5 has 6B active parameters. How many parameters does GPT-5.5 have?
  - lioeters 3mo ago
    We can run Leanstral locally on commodity/consumer hardware. Nuff said.
- ilc 3mo ago
  Given that they directly compare to GPT-5.5 in their documentation. This comes off as puppy kicking to me. They state it is not SOTA, even IN its domain! Honestly: Think twice before dragging your firm into what you say. Disclaimer: I speak for myself. Not any firm I am associated with.
  - deleted 3mo ago
    [deleted]
  - moonset 3mo ago
    Sorry, I recognize that these are different classes of model and didn't mean to punch down. I'm genuinely excited for the work Mistral is doing in this space!
henryrobbins00 3mo ago
Try out Leanstral 1.5 on the latest version of OpenATP! OpenATP is an open-source Python package and CLI for agentic automated theorem provers. It natively supports running provers locally in Docker or remotely in Modal sandboxes. GitHub: https://github.com/henryrobbins/open-atp https://github.com/henryrobbins/open-atp Docs: https://open-atp.henryrobbins.com https://open-atp.henryrobbins.com
- mathieudombrock 3mo ago
  [flagged]
  - henryrobbins00 3mo ago
    Earnest question: any recommendation to not come off this way in forums? I created this tool for my own research and have found it really helpful to benchmark different automated theorem provers (my experience so far has been that Claude Code + Codex still out-perform Leanstral). My genuine aim is to share that usefulness with others, not self promote!
    - zuzululu 3mo ago
      I don't know why but sometime ago, HN started resembling reddit, and there seems to be just widespread fear/jealousy/cynicism towards anybody advertising their work or services even, I don't think there was anything wrong with your post, it was informative. Probably the most annoying part about Reddit and HN and X (although it let you mute people) is the abundance of "expert" opinions from people who aren't experts at all. You just end up with a bunch of false signals that you shouldn't even be listening to. all in all I say invest in spreading the words via other channels, maybe even X is better and even the right time zone (besides US working hours, I find European time the worst statistically for sharing your work).
    - deleted 3mo ago
      [deleted]
    - lioeters 3mo ago
strongly-typed 3mo ago
Lean is such a wonderful language. So hyped by these releases.
Groxx 3mo ago
>One such bug was in the sign function for zigzag decoding of the datrs/varinteger library. On input Std.U64.MAX, the expression (value + 1) overflowed, causing crashes in debug mode and silent corruption in release mode—an edge case that testing and fuzzing would typically miss. that library is: https://github.com/datrs/varinteger https://github.com/datrs/varinteger it seems probably correct, as there's an identical issue filed on that repo a week before this was published: https://github.com/datrs/varinteger/issues/8 https://github.com/datrs/varinteger/issues/8 (is this a leanstral employee? they have almost no info and only very sparse activity. or did leanstral perhaps just pick up this issue?) it's a tiny, surprisingly-poorly tested, long-untouched (8y) library: https://github.com/datrs/varinteger/blob/master/tests/test.rs https://github.com/datrs/varinteger/blob/master/tests/test.r... that has about 1k downloads per day: https://crates.io/crates/varinteger https://crates.io/crates/varinteger [1] which seems rather low. I don't think I'd consider that such a smashing success that it's worth bringing up as the sole example tbh. though automated detection is certainly useful. or is this a noteworthy accomplishment for this sub-field? I haven't played with proof-writing LLMs, but given the paucity of training data I wouldn't be surprised if they're a bit rough compared to general coding. 1: https://crates.io/crates/varinteger https://crates.io/crates/varinteger lists it as https://github.com/mafintosh/varinteger-rs https://github.com/mafintosh/varinteger-rs which redirects to https://github.com/datrs/varinteger https://github.com/datrs/varinteger , so despite looking different at a glance it does appear to be the same library
- frostlynx 3mo ago
  The problem with proof is that it’s a bit hard sometimes to convey the value. The point is not to find bugs, but to prove that there are none (of a certain class; under certain assumptions; etc). But it’s a hard story to sell, so often the marketing is around “look at this bug we found”.
  - Eridrus 3mo ago
    I would be much more interested in "here is a provably memory safe version of openssl with all its memory safety bugs fixed"
  - 3mo ago
andai 3mo ago
Discussed the other day: https://news.ycombinator.com/item?id=48738938 https://news.ycombinator.com/item?id=48738938
andai 3mo ago
Halfway thru the article it shows a comparison with several frontier-ish LLMs. But they're all from half a year ago. "Our new model is better than all these Chinese models from 3 generations ago" is pretty funny to me.
- dannyw 3mo ago
  It’s a 6bn model. Totally different class. I’m more excited about “frontier small language models” tbh.
  - andai 3mo ago
    It's a 119B model, 6B active. That's still 3-10x smaller than the other models in that graph though (400B, 1T, 1.5T).
- rtaylorgarlock 3mo ago
  Agreed, though open weights + relatively small is still headline worthy. This thing really cooks.
RossBencina 3mo ago
Curious that they are pitching Lean 4 for formal verification. I thought that this was more the domain of Isabelle/HOL and TLA+. At least I would have expected a model trained at using all three. Maybe also Isabell/Isar, which seems preferable for forward derivations in linear algebra. Could anyone shed some light on this?
- nextos 3mo ago
  It is true that Lean has seen relatively little adoption in software verification compared to e.g. Isabelle and Rocq (previously Coq). Even Agda has had more traction in that domain. However, Lean is currently gaining significant momentum as an alternative, particularly due to its capabilities as a general-purpose functional programming language. Personally, I think something based on Hoare or separation logic would be more practical as it'd be easier to align requirements with specifications. I like Dafny and F*.
yashthakker 3mo ago
[flagged]
ChrisArchitect 3mo ago
[dupe] https://news.ycombinator.com/item?id=48738938 https://news.ycombinator.com/item?id=48738938
- rtaylorgarlock 3mo ago
  Have you ever been downvoted for calling 'dupe?' I once was downvoted after calling dupe on a link posted thrice. HN is an interesting place to hang out, that's for sure.
  - ChrisArchitect 3mo ago
    oh of course, unfortunately people's self-interest in pushing their own submissions and not being told they missed a story causes adverse reactions, but a bit of sacrifice worth keeping the site fresh and discussions focused.
    - rtaylorgarlock 2mo ago
      I also classify 'presence on HN' as a cause of adverse reactions. ;)
zuzululu 3mo ago
I applaud mistral's efforts but reading this release made me realize that Europe is far far behind and that once the gap is solidified I don't think its recoverable in the same way Canada's brain drain had on its economy The best and the brightest from Europe have no incentive to build in Europe when they can do it in America and be compensated and treated far better
- bjelkeman-again 3mo ago
  At this point I wouldn’t move to USA if you paid me double the salary. There are more things in life than money. That said, if (or when) the progress of the LLMs flatten out, then I think even Europe can catch up in a few years. If they don’t, and that seems unlikely to me, if the required compute needs to increase at the rate it does today, then I am not sure any of us can predict where society ends up.
  - InsideOutSanta 3mo ago
    I think there is a non-zero chance that Europe stumbled into an optimal scenario where they avoided all the losses incurred by US companies, but still benefit from the research. Having said that, doing so would require moving at the exact right time.
    - 9dev 3mo ago
      I wouldn't underestimate the capability of European companies to build rock-solid industries on established science. We may not be the pioneers wedging new product categories into the market, but there are millions of highly qualified people here, working hard every day. For example, Mercedes autonomous driving team is moving ahead at glacial speed, but the system they have so far is excellent and reliable. I'd prefer that over the sad joke Tesla is promoting any day.
  - zuzululu 3mo ago
    Sure some people like to make less money and pay more taxes for ideological reasons. I respect that.
raphinou 3mo ago
Can this be useful for someone with no prior knowledge of lean? I'd like to verify a software I'm working on, but I have no experience in formal verification. Can I get useful result with the spec, the code and some (limited) learning time on my side?
- rubendev 3mo ago
  I think at minimum you would need to understand which theorems you want to prove about your code, and how to express those in Lean. Otherwise you won’t be able to verify the output. It may have proven some statement that is machine checked to be correct, but it’s pointless if you don’t understand what that statement means and if it covers what you want to verify about your code.
- camkego 3mo ago
  Read this section of the article “ Bug Discovery: Finding Hidden Flaws”, they appear to have used the model on open source Rust to find issues starting with just the Rust code. You might be also able to have conversations that help you write the Lean to verify your application, but I’m not certain about this.
- rzmmm 3mo ago
  You need to understand the bits you are trying to prove, but not the full proof. It's more like reading haskell types than math, even though the vocabulary is heavily inspired by math.
- reinitctxoffset 3mo ago
  I've gone from zero knowledge of lean4 to the point where I'm doing most of my coding with it in ~6 months, and this was dramatically helped by how facile the AI assist is: it's remarkable how consistently fluent models are in lean4. I've found this to be true of the near frontier and smaller local models alike, LLMs just seem to get lean4. I still have a ways to go before calling myself a lean4 expert, but I don't need assist to get useful programs anymore. The ability to start with very little knowledge and still be able to trust parts you don't fully understand is a real unlock on learning progress: it's both practical and motivating to get useful programs you can rely on with incomplete knowledge, it sort of drags you in. You're bounded by the subset of the language that describes your axiom and proposition surface, not the subset that describes the intermediate steps. Over time as your ambition goes up, you need to understand more to do more things, but you can operate safely at level N+1 in a sense. It's also just a delightful programming language irrespective of its theorem proving role, and it's remarkably fast. I've got it bolted to io_uring and in many cases it blows the ass off of C++ with libuv or Rust with Tokio. Now and again you'll see some huge tail at the p99.99 latency or something and you go make a number fixed width or something, but you have to tune C++ and Rust too.
InsideOutSanta 3mo ago
There's a lot of criticism of Mistral being unable to compete with large model, and that's fair. But I think it dismisses what Mistral is actually doing, which is making specific capabilities available at high quality in tiny models. I do a lot of OCR, file analysis, stuff like that. I use Mistral for that. I put 100$ into my account, and it just runs for a year without any worries about the amount of requests I make, because the cost is minuscule. That's valuable, even if it doesn't compete with Opus 4.8.
- ekjhgkejhgk 3mo ago
  Stupid Europoors, optimizing for making a good product, instead of optimizing for making as much money as possible /s
  - nok22kon 3mo ago
    big AI labs make so much money because they have a good (amazing) product
    - lou1306 3mo ago
      Do they even _make_ actual money? https://isaiprofitable.com/ https://isaiprofitable.com/ seems to disagree.
      - guiriduro 3mo ago
        Do they dupe VC into enormous datacentre and capacity build-out investment? Why yes, actual money going to the AI hypester pick-axe vendors (and early equity dumpers) in that sense, absolutely yes it does. Is Big AI on track to pay that back with profit from any foreseeable and defensible business model? Different question. I sincerely doubt it.
        RazorBucksICO 3mo ago
        I think one of the more sober analysis that focused on danish firms exclusively predicted the overall growth impact on GDP to be a bit less than half a percent. Now, well that doesn’t sound very large, considering nominal GDP for the world is nearly $60 trillion, that is a big deal. I don’t know if that justifies trillion dollar evaluations for the providers, but even a small improvement over a large base is meaningful.
easygenes 3mo ago
Was fun to see their developers make nods to Le Chaton Fat in the announcements for this on Twitter. I suspect a true "big new general-purpose" model is around the corner from them, whether or not they were in on Le Chaton Fat for real. They've mentioned it after the media circus. Hopefully more creatively named than just "Large 4".
TokenLens 3mo ago
[flagged]
bjt12345 3mo ago
I find it a bit ridiculous to be critisizing Mistral, of all companies, as falling behind the Frontier models. Firstly, who hasn't fallen behind? Grok...Meta....? A lot of big companies are struggling. Secondly, Mistral are trying to solve a different problem. Finally, Mistral should be congratulated for staying in the race for so long now.
- canada_dry 3mo ago
  Considering the (apparent) heaps of money and brains thrown at GROK I'd argue MISTRAL is relatively futher ahead. Every time I go back to trying GROK it is an abysmal disappointment.

374 points by programLyrique 3mo ago

This is nice work, but I found the bug finding example to be weird: > One such bug was in the sign function for zigzag decoding of the datrs/varinteger library. On input Std.U64.MAX, the expression (value + 1) overflowed, causing crashes in debug mode and silent corruption in release mode—an edge case that testing and fuzzing would typically miss. In what way would this boundary condition case be considered something that "testing [...] would typically miss"? It's certainly something that bad tests would miss or not think about, but I find that (a) careful people and (b) ML coding systems are actually really good at "oh, I should test the extreme values". Especially for things that parse user input. I'm curious if they found other bugs that were more interesting, but found them too hard to explain quickly.

pierrefermat1 3mo ago
[flagged]
- fjdjshsh 3mo ago
  I feel this is a lazy, straw-manning comment.
fjdjshsh 3mo ago
Maybe it's not something they would "typically miss", but, from proof by existence, it's something they sometimes miss. It does speak to the benefits of using lean in that you don't need to be clever about the different examples you test.
Exoristos 3mo ago
Yes, it's basic QA. If tests missed this kind of thing, they would be of much more limited use than we generally expect them to be. It raises questions about the authors' background.
Groxx 3mo ago
particularly "and fuzzing", yea. fuzzing generally does intentionally explore boundary values, from what I've seen. for an encoding library like this, I think it's fair to say that fuzzing is a baseline expectation for any decent code, and it almost certainly would've caught this in seconds. --- edit concretely, I made a very simple round-trip test with proptest, and got dozens of failures and this in less than a second: thread 'signed_round_trip' (50528) panicked at tests/test.rs:72:1: Test failed: attempt to multiply with overflow. minimal failing input: value = 4611686018427387904 successes: 2 local rejects: 0 global rejects: 0
Quekid5 3mo ago
Because this is garbage PR. That's it. Every property-based testing system (invented ca. 1980) will explore boundary values. The semantics (or lack thereof) of C and C++ can make this difficult to actually test for because the compiler is allowed to say "test passed" to any input leading to UB.
- vlovich123 3mo ago
  Property based testing is good at generating boundary values for inputs. But for any more complicated piece of code getting boundary value coverage of interior values is an open problem that requires instrumentation feedback to understand branch coverage and value coverage of the code that got tested. It’s not an easy thing at all.
- teiferer 3mo ago
  > The semantics (or lack thereof) of C and C++ can make this difficult to actually test for because the compiler is allowed to say "test passed" to any input leading to UB. I get what you are saying but does this actually apply to a test? If the code under test is in one compilation unit and the test harness in another and they are linked together then the UB optimization issue ends at the API boundary and can't possibly make the test pass ..?
  - Quekid5 2mo ago
    It's definitely less likely with that technique (in practice!), but still very possible, via e.g. ODR violation or even the classic SIOF. So, ideally you'd want each separate test case to be compiled separately, but even then you wouldn't be safe! ... because any UB in that test (or the code it's testing!) could lead to a random pass. UB is good in some ways, but other ways it's really really bad. EDIT: I will say: If you have a UBSAN turned on for testing, etc. you're reasonably safe... but not fully. There's a lot of stuff they don't catch because it's essentially impossible.

satvikpendem 3mo ago

I also submitted the HuggingFace link itself here: https://news.ycombinator.com/item?id=48779902 https://news.ycombinator.com/item?id=48779902

nullc 3mo ago

It would be nice if special purpose models provided a some diverse examples of exactly the input required to get its expected performance on a mix of problem types. Maybe also a document intended for LLMs to read that advises on prompt construction. I've found that you can get wildly different quality results from these sorts of models due to seemingly insignificant differences in prompt construction. It would be much easier to guess at what it wants if I could just see some RL transcripts -- and so the model author is in a much better position to provide initial advice.

moonset 3mo ago

I gave Codex with GPT-5.5 High this prompt: Identify bugs in [datrs/varinteger](https://github.com/datrs/varinteger) . Do NOT look at the GitHub issues, just inspect the source It also found the bug that Leanstral 1.5 found and the authors highlighted. I think this bug wasn't especially tricky; it's just a case of too few eyeballs on this repo. Congrats on the release regardless! Excited for the direction Lean + automated AI proofs are headed. Disclosure: I work at OpenAI.

8note 3mo ago
the mechanism is whats interesting, rather than whether it could do it. this sounds like a great tool to add to the toolbelt, as part of the "how do we handle all the code output from LLMs" problem
noperator 3mo ago
Leanstral 1.5 has 6B active parameters. How many parameters does GPT-5.5 have?
- lioeters 3mo ago
  We can run Leanstral locally on commodity/consumer hardware. Nuff said.
ilc 3mo ago
Given that they directly compare to GPT-5.5 in their documentation. This comes off as puppy kicking to me. They state it is not SOTA, even IN its domain! Honestly: Think twice before dragging your firm into what you say. Disclaimer: I speak for myself. Not any firm I am associated with.
- deleted 3mo ago
  [deleted]
- moonset 3mo ago
  Sorry, I recognize that these are different classes of model and didn't mean to punch down. I'm genuinely excited for the work Mistral is doing in this space!

henryrobbins00 3mo ago

Try out Leanstral 1.5 on the latest version of OpenATP! OpenATP is an open-source Python package and CLI for agentic automated theorem provers. It natively supports running provers locally in Docker or remotely in Modal sandboxes. GitHub: https://github.com/henryrobbins/open-atp https://github.com/henryrobbins/open-atp Docs: https://open-atp.henryrobbins.com https://open-atp.henryrobbins.com

mathieudombrock 3mo ago
[flagged]
- henryrobbins00 3mo ago
  Earnest question: any recommendation to not come off this way in forums? I created this tool for my own research and have found it really helpful to benchmark different automated theorem provers (my experience so far has been that Claude Code + Codex still out-perform Leanstral). My genuine aim is to share that usefulness with others, not self promote!
  - zuzululu 3mo ago
    I don't know why but sometime ago, HN started resembling reddit, and there seems to be just widespread fear/jealousy/cynicism towards anybody advertising their work or services even, I don't think there was anything wrong with your post, it was informative. Probably the most annoying part about Reddit and HN and X (although it let you mute people) is the abundance of "expert" opinions from people who aren't experts at all. You just end up with a bunch of false signals that you shouldn't even be listening to. all in all I say invest in spreading the words via other channels, maybe even X is better and even the right time zone (besides US working hours, I find European time the worst statistically for sharing your work).
  - deleted 3mo ago
    [deleted]
  - lioeters 3mo ago

strongly-typed 3mo ago

Lean is such a wonderful language. So hyped by these releases.

Groxx 3mo ago

>One such bug was in the sign function for zigzag decoding of the datrs/varinteger library. On input Std.U64.MAX, the expression (value + 1) overflowed, causing crashes in debug mode and silent corruption in release mode—an edge case that testing and fuzzing would typically miss. that library is: https://github.com/datrs/varinteger https://github.com/datrs/varinteger it seems probably correct, as there's an identical issue filed on that repo a week before this was published: https://github.com/datrs/varinteger/issues/8 https://github.com/datrs/varinteger/issues/8 (is this a leanstral employee? they have almost no info and only very sparse activity. or did leanstral perhaps just pick up this issue?) it's a tiny, surprisingly-poorly tested, long-untouched (8y) library: https://github.com/datrs/varinteger/blob/master/tests/test.rs https://github.com/datrs/varinteger/blob/master/tests/test.r... that has about 1k downloads per day: https://crates.io/crates/varinteger https://crates.io/crates/varinteger [1] which seems rather low. I don't think I'd consider that such a smashing success that it's worth bringing up as the sole example tbh. though automated detection is certainly useful. or is this a noteworthy accomplishment for this sub-field? I haven't played with proof-writing LLMs, but given the paucity of training data I wouldn't be surprised if they're a bit rough compared to general coding. 1: https://crates.io/crates/varinteger https://crates.io/crates/varinteger lists it as https://github.com/mafintosh/varinteger-rs https://github.com/mafintosh/varinteger-rs which redirects to https://github.com/datrs/varinteger https://github.com/datrs/varinteger , so despite looking different at a glance it does appear to be the same library

frostlynx 3mo ago
The problem with proof is that it’s a bit hard sometimes to convey the value. The point is not to find bugs, but to prove that there are none (of a certain class; under certain assumptions; etc). But it’s a hard story to sell, so often the marketing is around “look at this bug we found”.
- Eridrus 3mo ago
  I would be much more interested in "here is a provably memory safe version of openssl with all its memory safety bugs fixed"
- 3mo ago

andai 3mo ago

Discussed the other day: https://news.ycombinator.com/item?id=48738938 https://news.ycombinator.com/item?id=48738938

andai 3mo ago

Halfway thru the article it shows a comparison with several frontier-ish LLMs. But they're all from half a year ago. "Our new model is better than all these Chinese models from 3 generations ago" is pretty funny to me.

dannyw 3mo ago
It’s a 6bn model. Totally different class. I’m more excited about “frontier small language models” tbh.
- andai 3mo ago
  It's a 119B model, 6B active. That's still 3-10x smaller than the other models in that graph though (400B, 1T, 1.5T).
rtaylorgarlock 3mo ago
Agreed, though open weights + relatively small is still headline worthy. This thing really cooks.

RossBencina 3mo ago

Curious that they are pitching Lean 4 for formal verification. I thought that this was more the domain of Isabelle/HOL and TLA+. At least I would have expected a model trained at using all three. Maybe also Isabell/Isar, which seems preferable for forward derivations in linear algebra. Could anyone shed some light on this?

nextos 3mo ago
It is true that Lean has seen relatively little adoption in software verification compared to e.g. Isabelle and Rocq (previously Coq). Even Agda has had more traction in that domain. However, Lean is currently gaining significant momentum as an alternative, particularly due to its capabilities as a general-purpose functional programming language. Personally, I think something based on Hoare or separation logic would be more practical as it'd be easier to align requirements with specifications. I like Dafny and F*.

yashthakker 3mo ago

[flagged]

ChrisArchitect 3mo ago

[dupe] https://news.ycombinator.com/item?id=48738938 https://news.ycombinator.com/item?id=48738938

rtaylorgarlock 3mo ago
Have you ever been downvoted for calling 'dupe?' I once was downvoted after calling dupe on a link posted thrice. HN is an interesting place to hang out, that's for sure.
- ChrisArchitect 3mo ago
  oh of course, unfortunately people's self-interest in pushing their own submissions and not being told they missed a story causes adverse reactions, but a bit of sacrifice worth keeping the site fresh and discussions focused.
  - rtaylorgarlock 2mo ago
    I also classify 'presence on HN' as a cause of adverse reactions. ;)

zuzululu 3mo ago

I applaud mistral's efforts but reading this release made me realize that Europe is far far behind and that once the gap is solidified I don't think its recoverable in the same way Canada's brain drain had on its economy The best and the brightest from Europe have no incentive to build in Europe when they can do it in America and be compensated and treated far better

bjelkeman-again 3mo ago
At this point I wouldn’t move to USA if you paid me double the salary. There are more things in life than money. That said, if (or when) the progress of the LLMs flatten out, then I think even Europe can catch up in a few years. If they don’t, and that seems unlikely to me, if the required compute needs to increase at the rate it does today, then I am not sure any of us can predict where society ends up.
- InsideOutSanta 3mo ago
  I think there is a non-zero chance that Europe stumbled into an optimal scenario where they avoided all the losses incurred by US companies, but still benefit from the research. Having said that, doing so would require moving at the exact right time.
  - 9dev 3mo ago
    I wouldn't underestimate the capability of European companies to build rock-solid industries on established science. We may not be the pioneers wedging new product categories into the market, but there are millions of highly qualified people here, working hard every day. For example, Mercedes autonomous driving team is moving ahead at glacial speed, but the system they have so far is excellent and reliable. I'd prefer that over the sad joke Tesla is promoting any day.
- zuzululu 3mo ago
  Sure some people like to make less money and pay more taxes for ideological reasons. I respect that.

raphinou 3mo ago

Can this be useful for someone with no prior knowledge of lean? I'd like to verify a software I'm working on, but I have no experience in formal verification. Can I get useful result with the spec, the code and some (limited) learning time on my side?

rubendev 3mo ago
I think at minimum you would need to understand which theorems you want to prove about your code, and how to express those in Lean. Otherwise you won’t be able to verify the output. It may have proven some statement that is machine checked to be correct, but it’s pointless if you don’t understand what that statement means and if it covers what you want to verify about your code.
camkego 3mo ago
Read this section of the article “ Bug Discovery: Finding Hidden Flaws”, they appear to have used the model on open source Rust to find issues starting with just the Rust code. You might be also able to have conversations that help you write the Lean to verify your application, but I’m not certain about this.
rzmmm 3mo ago
You need to understand the bits you are trying to prove, but not the full proof. It's more like reading haskell types than math, even though the vocabulary is heavily inspired by math.
reinitctxoffset 3mo ago
I've gone from zero knowledge of lean4 to the point where I'm doing most of my coding with it in ~6 months, and this was dramatically helped by how facile the AI assist is: it's remarkable how consistently fluent models are in lean4. I've found this to be true of the near frontier and smaller local models alike, LLMs just seem to get lean4. I still have a ways to go before calling myself a lean4 expert, but I don't need assist to get useful programs anymore. The ability to start with very little knowledge and still be able to trust parts you don't fully understand is a real unlock on learning progress: it's both practical and motivating to get useful programs you can rely on with incomplete knowledge, it sort of drags you in. You're bounded by the subset of the language that describes your axiom and proposition surface, not the subset that describes the intermediate steps. Over time as your ambition goes up, you need to understand more to do more things, but you can operate safely at level N+1 in a sense. It's also just a delightful programming language irrespective of its theorem proving role, and it's remarkably fast. I've got it bolted to io_uring and in many cases it blows the ass off of C++ with libuv or Rust with Tokio. Now and again you'll see some huge tail at the p99.99 latency or something and you go make a number fixed width or something, but you have to tune C++ and Rust too.

InsideOutSanta 3mo ago

There's a lot of criticism of Mistral being unable to compete with large model, and that's fair. But I think it dismisses what Mistral is actually doing, which is making specific capabilities available at high quality in tiny models. I do a lot of OCR, file analysis, stuff like that. I use Mistral for that. I put 100$ into my account, and it just runs for a year without any worries about the amount of requests I make, because the cost is minuscule. That's valuable, even if it doesn't compete with Opus 4.8.

ekjhgkejhgk 3mo ago
Stupid Europoors, optimizing for making a good product, instead of optimizing for making as much money as possible /s
- nok22kon 3mo ago
  big AI labs make so much money because they have a good (amazing) product
  - lou1306 3mo ago
    Do they even _make_ actual money? https://isaiprofitable.com/ https://isaiprofitable.com/ seems to disagree.
    - guiriduro 3mo ago
      Do they dupe VC into enormous datacentre and capacity build-out investment? Why yes, actual money going to the AI hypester pick-axe vendors (and early equity dumpers) in that sense, absolutely yes it does. Is Big AI on track to pay that back with profit from any foreseeable and defensible business model? Different question. I sincerely doubt it.
      - RazorBucksICO 3mo ago
        I think one of the more sober analysis that focused on danish firms exclusively predicted the overall growth impact on GDP to be a bit less than half a percent. Now, well that doesn’t sound very large, considering nominal GDP for the world is nearly $60 trillion, that is a big deal. I don’t know if that justifies trillion dollar evaluations for the providers, but even a small improvement over a large base is meaningful.

easygenes 3mo ago

Was fun to see their developers make nods to Le Chaton Fat in the announcements for this on Twitter. I suspect a true "big new general-purpose" model is around the corner from them, whether or not they were in on Le Chaton Fat for real. They've mentioned it after the media circus. Hopefully more creatively named than just "Large 4".

TokenLens 3mo ago

[flagged]

bjt12345 3mo ago

I find it a bit ridiculous to be critisizing Mistral, of all companies, as falling behind the Frontier models. Firstly, who hasn't fallen behind? Grok...Meta....? A lot of big companies are struggling. Secondly, Mistral are trying to solve a different problem. Finally, Mistral should be congratulated for staying in the race for so long now.

canada_dry 3mo ago
Considering the (apparent) heaps of money and brains thrown at GROK I'd argue MISTRAL is relatively futher ahead. Every time I go back to trying GROK it is an abysmal disappointment.