| ▲ | Leanstral 1.5: Proof Abundance for All(mistral.ai) | |||||||
| 36 points by programLyrique 2 hours ago | 4 comments | ||||||||
| ▲ | boulos an hour ago | parent | next [-] | |||||||
This 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. | ||||||||
| ||||||||
| ▲ | satvikpendem 39 minutes ago | parent | prev | next [-] | |||||||
I also submitted the HuggingFace link itself here: https://news.ycombinator.com/item?id=48779902 | ||||||||
| ▲ | nullc 29 minutes ago | parent | prev [-] | |||||||
It 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. | ||||||||