News for hackers. Stuff that matters.

A comment on Leanstral: Open-Source foundation for trustworthy vibe-coding. Parent comment

Re:Leanstral: Open-Source foundation for trustworthy vibe-co... by flowerbreeze on Monday March 16, 2026 @05:54PM (#47405472)
They haven't made the chart very clear, but it seems it has configurable passes and at 2 passes it's better than Haiku and Sonnet and at 16 passes starts closing in on Opus although it's not quite there, while consistently being less expensive than Sonnet.
[ Parent | on HN ]
Re:Leanstral: Open-Source foundation for trustworthy vibe-co... by andai on Monday March 16, 2026 @06:01PM (#47405545)
Oh my bad. I'm not sure how that works in practice. Do you just keep running it until the tests pass? I guess with formal verification you can run it as many times as you need, right?
[ Parent | on HN ]
Re:Leanstral: Open-Source foundation for trustworthy vibe-co... by ainch on Monday March 16, 2026 @09:05PM (#47407314)
pass@k means that you run the model k times and give it a pass if any of the answers is correct. I guess Lean is one of the few use cases where pass@k actually makes sense, since you can automatically validate correctness.
[ Parent | on HN ]