WIP new GRPO dataset and task: formally-verified program correctness

[ocramz]

A new dataset and family of tasks to reward models that judge code snippets as "correct" in the deductive program verification sense [1][2].

We provide two API endpoints:

• program triple data generation : random program generation in a toy subset of Python, together with preconditions and postconditions. Additionally, the API endpoint returns the execution "trace" (how the variable environment is mutated after each statement).
• program triple verification : parse model completions and return verification answer.

The API endpoints are parametric, so it's possible to train the model on small ASTs and test on larger ones, or longer programs, etc. to do small-to-large generalization trials.

• ✅ add GRPO helpers to use the new API endpoints: src/open_r1/rewards/api/code/unfoldml/htgen.py and src/open_r1/rewards/code/htgen.py
• ✅ add unit/integration tests for the new API bindings
• ❓ FEEDBACK PLEASE : how to prompt a model under test using structured information? Should we use a specific templating format? Should the prompt be assembled inside the GRPO iterable dataset? for now we assemble the prompt in the dataset generator.

[1] https://en.wikipedia.org/wiki/Correctness_(computer_science)
[2] https://en.wikipedia.org/wiki/Hoare_logic

cc @Muhtasham @vumichien and @lewtun @qgallouedec ^^