Does Mistral come close to Opus 4.6 with any of their models?
Not at the moment, but a release of Mistral 4 seems close which likely bridges the gap.
Leanstral: Open-source agent for trustworthy coding and formal proof engineering
11–20 of 234 posts
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#12Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#13Maybe a naive question: given that they see better performance with more passes but the effect hits a limit after a few passes, would performance increase if they used different models per pass, i.e leanstral, kimi, qwen and leanstral again instead of 4x leanstral?
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.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#14This is great, congratulations to the Mistral team! I'm looking forward to the code arena benchmark results. Thanks for sharing.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#15What are these "passes" they reference here? Haven't seen that before in LLM evals
Could definitely be interesting for having another model run over the codebase when looking for improvements
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#16Curious if anyone else had the same reaction as me This model is specifically trained on this task and significantly[1] underperforms opus. Opus costs about 6x more. Which seems... totally worth it based on the task at hand. [1]: based on the total spread of tested models
I'm never sure how much faith one can put into such benchmarks but in any case the optics seem to shift once you have pass@2 and pass@3.
Still, the more interesting comparison would be against something such as Codex.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#17[flagged]
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#18Maybe a naive question: given that they see better performance with more passes but the effect hits a limit after a few passes, would performance increase if they used different models per pass, i.e leanstral, kimi, qwen and leanstral again instead of 4x leanstral?
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.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#19Does Mistral come close to Opus 4.6 with any of their models?
I use mistral-medium-3.1 for a lot of random daily tasks, along with the vibe cli. I'd state from my personal opinion that mistral is my preferred 'model vendor' by far at this point. They're extremely consistent between releases while each of them just feels better. I also have a strong personal preference to the output.
I actively use gemini-3.1-pro-preview, claude-4.6-opus-high, and gpt-5.3-codex as well. I prefer them all for different reasons, however I usually _start_ with mistral if it's an option.
Re: Leanstral: Open-source agent for trustworthy coding and formal proof engineering
#20What are these "passes" they reference here? Haven't seen that before in LLM evals Could definitely be interesting for having another model run over the codebase when looking for improvements
It's the number of attempts at answering the question.