Birbla

Discussion summary

The discussion highlights Europe's lag in AI development compared to North America, with some noting the US's less desirable environment. Participants discuss the capabilities of Leanstral 1.5 with 6B parameters and compare it to larger models like GPT-5.5, emphasizing the importance of mechanisms over size.

What the discussion says

  • Europe is behind in AI progress and may not recover easily.
  • US offers higher pay but worse living conditions, making it less attractive.
  • Leanstral 1.5 with 6B parameters is notable, but GPT-5.5 has more parameters.
  • Some see value in mechanisms and tools over sheer model size.
“Europe is far behind, and the gap might be irrecoverable.”
— zuzululu
“Treating AI models better doesn't necessarily mean earning more.”
— pbkompasz

Join the discussion

Write your take first — we'll ask for email only when you're ready to publish.

Sign in
  • Hacker News
  • 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

    Docs: https://open-atp.henryrobbins.com

    by henryrobbins00
  • 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.

    by nullc
  • 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".

    by easygenes
  • I also submitted the HuggingFace link itself here: https://news.ycombinator.com/item?id=48779902
    by satvikpendem
  • Discussed the other day:

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

    by andai
  • 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?
    by raphinou
  • 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.
    by rubendev
  • 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.
    by camkego
  • 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.
    by rzmmm
  • 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.

    by reinitctxoffset
  • 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?
    by RossBencina
  • 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*.

    by nextos
  • 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.

    by bjt12345
  • 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.

    by canada_dry
  • >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

    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 (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.r... that has about 1k downloads per day: 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 lists it as https://github.com/mafintosh/varinteger-rs which redirects to https://github.com/datrs/varinteger , so despite looking different at a glance it does appear to be the same library

    by Groxx
  • 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”.
    by frostlynx
  • 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.
    by andai
  • Agreed, though open weights + relatively small is still headline worthy. This thing really cooks.
    by rtaylorgarlock
  • It’s a 6bn model. Totally different class. I’m more excited about “frontier small language models” tbh.
    by dannyw
  • 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.

    by boulos
  • 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.
    by Exoristos
  • 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.

    by Quekid5
  • 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.

    by fjdjshsh
  • 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
    by Groxx
  • 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.

    by InsideOutSanta
  • I'm not sure the "a year of document processing for under 100 USD/y" is such as great thing as you think it is (at least not for European competitiveness)... It means Mistral is essentially setting a revenue ceiling very low. OCR is a commodity at this point, and open source models, AWS, etc already do it out of the box.

    Plus, you can't really build loyalty on a 100 USD/Y price tag. Since there are no switching costs holding them back, those buyers will leave the moment somebody offers a lower rate. An easily cloned, low cost tool with zero customer lock in is not a business. It is a feature.

    That might sound great for the buyer (you), but it is a terrible strategy if we want a European company to compete long term against global competitors on actual product merit instead of just regulatory arbitrage.

    by baridbelmedar
  • Stupid Europoors, optimizing for making a good product, instead of optimizing for making as much money as possible /s
    by ekjhgkejhgk
  • Yeah, I think also efforts like Docling and similar are showing that smaller, specialized models with the right tooling might be more effective (and efficient) at this than throwing everything at Opus.

    They don't seem to release as much open-weights at Mistral as they used to though :)

    by nejch
  • i would argue it is more valuable
    by nicman23
  • But how does it compete on OCR? I find that having good quality at a cheap price is more niche than having the best quality at 10x the cheap price, because for most use cases you want to pay a bit more if it saves you mistakes later.
    by stavros