Here we go.
Leanstral: Open-source agent for trustworthy coding and formal proof engineering
41–50 of 234 posts
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#42I don’t know a single person using Mistral models.
I used Ministral for data cleaning.
I was surprised: even tho it was the cheapest option (against other small models from Anthropic) it performed the best in my benchmarks.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#43[dead]
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#44is the haiku comparison because they've distilled from the model?
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#45Earlier quoted context omitted.
Not at the moment, but a release of Mistral 4 seems close which likely bridges the gap.
Mistral Small 4 is already announced.
MOE but 120B range. Man I wish it was an 80B. I have 2 GPUs with 62Gib of usable VRAM. A 4bit 80B gives me some context window, but 120B puts me into system RAM
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#46There have been a lot of conversations recently about how model alignment is relative and diversity of alignment is important - see the recent podcast episode between Jack Clark (co-founder of Anthropic) and Ezra Klein.
Many comments here point out that Mistral's models are not keeping up with other frontier models - this has been my personal experience as well. However, we need more diversity of model alignment techniques and companies training them - so any company taking this seriously is valuable.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#47I don’t know a single person using Mistral models.
I used Ministral for data cleaning. I was surprised: even tho it was the cheapest option (against other small models from Anthropic) it performed the best in my benchmarks.
Mistral is super smart in smaller context and asking questions about it
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#48Earlier quoted context omitted.
Agreed. The idea is nice and honorable. At the same time, if AI has been proving one thing, it's that quality usually reigns over control and trust (except for some sensitive sectors and applications). Of course it's less capital-intense, so makes sense for a comparably little EU startup to focus on that niche. Likely won't spin the top line needle much, though, for the reasons stated.
EU could help them very much if they would start enforcing the Laws, so that no US Company can process European data, due to the Americans not willing to budge on Cloud Act. That would also help to reduce our dependency on American Hyperscalers, which is much needed given how untrustworthy the US is right now. (And also hostile towards Europe as their new security strategy lays out)
This would be unfortunately a rather nuclear option due to the continent’s insane reliance on technology that breaks its unenforced laws.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#49Earlier quoted context omitted.
It’s really not hard — just explicitly ask for trustworthy outputs only in your prompt, and Bob’s your uncle.
Assuming that what you're dealing with is assertable. I guess what I mean to say is that in some situations is difficult to articulate what is correct and what isn't depending in some situations is difficult to articulate what is correct and what isn't depending upon the situation in which the software executes.
And Bob’s your uncle.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#50Pleasant surprise: someone saying "open source" and actually meaning Open Source . It looks like the weights are Apache-2.0 licensed.
Based on community definitions I've seen, this is considered "open weights". If you can't reproduce the model, it's not "open source"