What I'm missing here is also type guarantees. I don't think you can do it without token level logic which forces the model to output the tokens from a predefined pool of tokens. A logic like this given some JSON schema is not that difficult to implement. If the LLM must output JSON schema compatible value then you can also add that it doesn't "hallucinate". Which is funny too because just guaranteeing the type does not mean the model does not hallucinate but this is another story.
The type is guaranteed because you only read the probability from your set of choice tokens
You don't actually use the "next token" that the model chooses
That's what the author is doing in this part
This works because the model is always producing probabilities for all tokens