Leanstral 1.5: Proof abundance for all
mistral.ai
Leanstral 1.5: Proof abundance for all
1–10 of 116 posts
Re: Leanstral 1.5: Proof abundance for all
#2This 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.
Re: Leanstral 1.5: Proof abundance for all
#3I also submitted the HuggingFace link itself here: https://news.ycombinator.com/item?id=48779902
Re: Leanstral 1.5: Proof abundance for all
#4This 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…
[flagged]
Re: Leanstral 1.5: Proof abundance for all
#5It 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.
Re: Leanstral 1.5: Proof abundance for all
#6This 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…
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.
Re: Leanstral 1.5: Proof abundance for all
#7This 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…
[flagged]
I feel this is a lazy, straw-manning comment.
Re: Leanstral 1.5: Proof abundance for all
#8I gave Codex with GPT-5.5 High this prompt:
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.
Re: Leanstral 1.5: Proof abundance for all
#9Try 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.
Re: Leanstral 1.5: Proof abundance for all
#10This 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…
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.