> if AI (or humans) have mistranslated a natural language statement to a formal statement, we should not rely on AI to correctly translate the formal statement back into natural language.

Perhaps we must not rely on it and find a way to make sure that it cannot fail, but I like to point out that this are two different problems and it seems to me that the current crop of so called AIs are pretty good at distilling excerpts. Perhaps that's the easier problem to solve?