It’s not useless, because you can, for example, ask multiple frontier models to do the formalization and see if they agree. And if they have surface-level differences in formalization, you can also ask them whether apparently-different definitions are equivalent.

This isn’t perfect of course - perhaps every single model is wrong. But you are too quick to declare that something isn’t useful for arriving at an answer. Reducing the surface area of what needs to be checked is good regardless.