Leanstral 1.5: Proof abundance for all(mistral.ai) |
Leanstral 1.5: Proof abundance for all(mistral.ai) |
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.
Basically, to find the answer you really need your own benchmark you run with real examples from what you want to do. Basically the same goes for anything ML nowadays as the public benchmarks cannot really be trusted to give you any sort of indication on how we'll it'd work for you.
They don't seem to release as much open-weights at Mistral as they used to though :)
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.
And yes, its good that "its good for buyer" after all we do business so that living would be nicer, not the other way around (live to do business)
> 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.
That's still 3-10x smaller than the other models in that graph though (400B, 1T, 1.5T).
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
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.
Every time I go back to trying GROK it is an abysmal disappointment.
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*.
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".
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.
Identify bugs in [datrs/varinteger](https://github.com/datrs/varinteger) . Do NOT look at the GitHub issues, just inspect the source
Congrats on the release regardless! Excited for the direction Lean + automated AI proofs are headed.
Disclosure: I work at OpenAI.
This is a little bit like someone pointing the moon and you look at the finger.
The formal proof domain goes way beyond just finding bugs.
It has tons of usages in term of functional safety, protocol validation, cryptography, etc...
The fact Mistral tackle this kind of problem is both smart and not so surprising.
Smart because it is niche enough that they do not front face the big competitors (yet).
No so surprising because the French labs have a well known and long time expertise with formal proof tools (Coq and all its Ocaml associated tools). It has been historically mainly pushed by the aerospace and train industries (Airbus, Dassault, Alsthom).
Honestly: Think twice before dragging your firm into what you say.
Disclaimer: I speak for myself. Not any firm I am associated with.
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
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
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.
Life's not all about the number on your bank account. Once you're past a certain level (which a competent engineer can easily reach in Europe as well), the marginal utility of money diminished quite quickly.
--- 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: 0It does speak to the benefits of using lean in that you don't need to be clever about the different examples you test.
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.
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 ..?
Now, go write the code for an artificial heart , and sleep at night thanks to strong testing !
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.
In terms of process I don't know that I really have any unique edge or anything, I'm still very intermediate as a lean4 programmer. I was a strong Haskeller before so I had a little bit of a map. The key thing about lean4 coming from e.g Haskell is that it has a much cleaner type tower, there's no type/kind/PolyKind jank, it's just Type 0, Type 1, as high as you care to go (which usually isn't very high), so a fair bit is unlearning some of that.
A mistake I made was to try to learn lean4 in emacs, which I'm working on making more reasonable, but today lean4 is a vscode only experience IMHO, this is partially because the default Mathlib4 style is really unapproachable without the tooling (not being a professional mathematician I'll stop short of calling the style bad, maybe it's intuitive to mathematicians, but it's very ill suited for programming in the large as a hacker would approach it). Proofs of theorems are this tactic match space with a lot of implicit projection up into a big possibility space at every step, and then the next explicit tactic is grabbing things from that space often very implicitly. It's my least favorite part of the semantics (or maybe one I feel is over-used, there are ways to make it more explicit, the canonical example is probably `simp_only` which grounds in specific lemmas).
The effectful part of the language should be a pretty short hop from anything else with do-notation, it reads very naturally and the conditional/looping/match stuff sorta looks like Rust if you squint a little. One place the AI assist really shines is to go rename all the variables something reasonable, a lot of otherwise great code looks like it hybridized with a bizarre Hungarian-notation splinter faction, the keywords are fine.
There's some stuff that probably makes a lot of sense in a meta mathematical view of things that makes zero sense from a TCB standpoint. To mathematicians there is a distinction between the map coloring proof and Wiles' FLT proof. This is real and it makes sense in mathematics. But in high-assurance software having an issue with `native_decide` as opposed to `bv_decide` is a weird religion: TCB certifying them is identically compromised by a compromised compiler.
So I think it's mostly just a very small community trying to write code as the primary activity and layering on formal methods as a correctness strategy as opposed to a much bigger community doing real maths where the programming language is more of an amenity than the main show.
I suppose my approach is to be willing to go a different way in a different use case.
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.
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.
Which can run comfortably on 12gb of vram. I gave it a whirl and it does seem pretty competitive. I wonder how that compares for your usecase
Another big use case is GPU kernel compilation. I've encoded the polyhedral algebra used by CuTe and all of the stated theorems from nvfuser in lean4. From this you can recover scheduling and tiling properties that must be met to get equal or better performance to CASK (likely optimal) for many operations, and then lower that to PTX. Surprisingly often the candidate set for the fastest possible kernel turns out to be finite and enumerable, so fast inference.
Somewhat recently I started benchmarking stuff just directly in lean4 with a very small TCB shim to e.g. io_uring. I've done like the basic systems programming ABCs (I've got a reverse proxy that's lean4 and ~100 lines of C and shatters nginx, faster at every point on the histogram, memory use flat as a strap). Lithe runs on it so I can do web serving as fast as anything in the hyper ecosystem.
Now that I've got my feet with it I'm digging in on a serious project which is a hypervisor that addresses the deficiencies in firecracker. This is a place where some proven properties can really get you a lot of performance (something like firecracker has to be very defensive regarding e.g. virtqueue semantics in the presence of a malicious guest). Firecracker is an exceptional piece of code and it's carried me far but at agent scale it's time to go another turn of the crank on virtualization performance.
I have lived in the UK, in the US and spent significant time running a startup in the Netherlands, and half the family lives there. I have relatives in Spain and in Switzerland. I have helped setup startup subsidiaries on all continents.
Food is important for national security so we should subsidize it, but it's a cost center. It'll never drive growth.
If that's what Mistral is aiming for, it would probably be better to give up now.
If Mistral is aiming not to grow to infinity but instead to offer niche models at reasonable prices, should they give up now? I think I'm not sure what exactly you're saying.
There are a whole lot of commodity businesses that flourishes and that are profitable. It's true, that, yes, they will not have huge margins.
Grocery stores are like that - some of their suppliers might be subsidised but they are not, and many places they operate with typical margins in the 2% range. Discount supermarkets in the UK are operating on around 0.7% margins.
They are still huge, profitable businesses.
And they are examples of what happens when markets work.
Is Big AI on track to pay that back with profit from any foreseeable and defensible business model? Different question. I sincerely doubt it.
The good thing about open capital markets is the possibility to invest in the upside. The downside is who gets holding the bag when the money runs out
And API is 80% of their business (subscriptions the other 20%)
One, this conversation is about economy side of things.
And two, calling comparison between humans and LLMs disgusting when LLMs are borderline GAIs sounds very xenophobic. Did you see the thread about LLM-written fiction contest the other day? https://news.ycombinator.com/item?id=48782890
I take it you know your primary purpose.