Autoformalizing Chain of Thought: Representation, Verification, and Logical Shortcuts

Evaluating the logical validity of natural language chain-of-thought (CoT) reasoning remains challenging due to the stylistic variability and implicit assertions of informal text. To enable formal verification of natural language CoT reasoning, we establish two formalization pipelines by adopting Abstract Meaning Representation (AMR) and direct end-to-end prompting, grounding CoT rationales in the Lean theorem-proving language. To assess reasoning validity under formalization, we integrate an agentic prover that iteratively updates formalized rationales with proof via compiler feedback, and subject the generated proofs to altered rationales stress tests. Our analysis demonstrates a complementary trade-off between direct formalization and explicit semantic structure. Direct end-to-end prompting formalization strips away unnecessary contextualization while preserving essential logical cores. In turn, AMR's structural standardization provides a grounded semantic anchor for auto-formalization, keeping most semantic components. However, our stress tests reveal that while dependent type theory restricts candidate reasoning paths, formal verification alone does not fully eradicate logical shortcuts. Overall, our results suggest that auto-formalization is feasible beyond mathematics, but semantic faithfulness remains a central challenge for natural-language reasoning.