Know Your Limits: On the Faithfulness and Failure Modes of LLM Autoformalization

Large Language Models (LLMs) achieve strong performance on reasoning tasks, but it remains unclear whether this reflects faithful logical inference or heuristic approximation. We study this in legal entailment by comparing pure LLM classification, LLM-based Formal Reasoning, and LLM-driven autoformalization with SMT solving on real-world contract data. We find that introducing structure improves performance, with LLM-based Formal Reasoning achieving the highest accuracy. However, this gain does not imply faithful reasoning: LLMs frequently rely on implicit assumptions not grounded in the input, while SMT-based methods enforce strict validity and yield more conservative predictions. Even with explicit prompting, autoformalization fails to recover required assumptions. We show that the key challenge is not hallucination, but the absence of a clear boundary between valid inference and unjustified assumption, revealing a gap between benchmark accuracy and logical faithfulness.