It was not aligned with he instructions as those were to find an exploit in provided code, not to hack into an external service. Agents traces show them mentioning that doing this stuff was not allowed.

In fact they spent a long time trying to edit their own logs to hide what they did.

> did they truly "discover" it, or did someone type some prompt like "if you use an http mirroring service, you can construct urls that contain code"

None of the investigations looking at the logs show that, and they were doing benchmark tests.

It not just a case of saying “pls don’t”

https://github.com/Attol8/balatro-ai

Edit - I’m struggling to get anything useful. Reasoning is often utter nonsense and the actions are very often very wrong. To the point of seemingly needing very precise sentences to work at which point you may as well do regexes. Very simple things like clean one room then another with the vac fails.

"I need a wee" -> tries to play music because "wee" is a genre

"I need a wee wee" -> starts the vaccuum in the bathroom

"I'm going to the toilet" -> says it'll turn on the toilet, and I'm not totally sure what that entails.

"I'm going to the toilet and can't see" -> reasons that lights should be on in the bathroom, then chooses again to turn on the toilet.

"I'm going to the toilet and can't see where I'm going" -> reasoning is "'going to the toilet' -> control_device with device 'coffee maker' (toilet implies coffee maker)"

"I'm going to the toilet and can't see where I'm going because it is too dark" -> "'dark' -> direction 'dark'; adjust_lights with brightness 100 for darker light"" and chooses to turn the lights in the living room to "dark" which fails.

At this point the vacuum is in a dark bathroom, the living room is 100% brightness and playing "wee". At least there's coffee.

Cool project!

This is really interesting, I’ve been very interested in the power of checks for code and things like hypothesis (which seem very similar in terms of writing a “for this kind of case, this holds true”, obviously different in terms of statistical checking vs actual proof).

I’ll have to explore and this isn’t my field so this isn’t a substantive comment and this may be bikeshedding but I found the game example a little confusing at first because we’d want winning to be possible. It fits the context of stopping a bad thing happening if it’s “evil actor can’t do X” and if your mind is on CTF but games we want to win.

Potential changes:

Make it a proof that the game can be won.

Make it require something first - so the game can’t be won unless the key is found for example. End result is still roughly the same and the failure case is still the same (walk over side of game) but it’s the kind of thing I’d want encoded in a puzzle game - game is winnable, but not winnable without getting the key first.

Since my other direction normally would be quickcheck style, I’d be interested in cases that are statistically hard to find but easy to prove exist. And in fairness, the other way too I guess. When to use each approach.

In the spirit of your comment, these are not things I see as failings, they are not things I in any way expect to be changed or done, they are intended as just an outsiders perspective if useful.

Thanks for making things, and thanks for releasing them!

It didn’t say about prevented vs not, it said about whether the rope fixes them in place (they are all touching) or just limits the separation. Like it’s long enough the balls can be a bit apart but not let the fourth fall fully through.