Zhao, Z. (CSE) – TOWARD VERIFIABLE REASONING IN LLMS
Chain-of-thought (CoT) prompting can improve final-answer performance, but it does not guarantee that intermediate reasoning steps are faithful, valid, or checkable. This proposal studies how formal methods can make natural-language reasoning more reliable by translating CoT rationales into Lean artifacts, checking the resulting theorem statements and proofs, and using compiler feedback to diagnose and repair failures. The completed work evaluates direct zero-shot and few-shot auto-formalization pipelines for quantity- and logic-focused reasoning problems, measuring proof type-check rate, theorem-statement validity, assumption faithfulness, and repair behavior. The ongoing work extends this pipeline with AMR-guided semantic representations and altered-rationale stress tests. The planned work proposes […]