Can't the non-deterministic LLM produce deterministic software? Assuming it is not allowed to modify the theorem proving software.