Papers by Chengwu Liu
Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification (2025.acl-long)
Copied to clipboard
Chengwu Liu, Ye Yuan, Yichun Yin, Yan Xu, Xin Xu, Zaoyu Chen, Yasheng Wang, Lifeng Shang, Qun Liu, Ming Zhang
| Challenge: | Chain-of-Thought prompting is a de facto method to elicit reasoning capabilities from large language models (LLMs). |
| Approach: | They propose a step-aware formal verification framework Safe to address hallucinations in CoT prompting . they propose 'formal step' as a benchmark for step correctness theorem proving with 30,809 formal statements. |
| Outcome: | The proposed framework shows significant performance improvement while offering interpretable and verifiable evidence. |
Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4 (2026.acl-long)
Copied to clipboard
Chengwu Liu, Yichun Yin, Ye Yuan, Jiaxuan Xie, Botao Li, Siqi Li, Jianhao Shen, Yan Xu, Lifeng Shang, Ming Zhang
| Challenge: | Existing approaches to solving mathematical problems fall into two broad categories: informal methods and formal methods. |
| Approach: | They propose to use LLM natural-language reasoning to discover answers . they introduce Discover And Prove framework that rewrites Hard Mode statements into Easy Mode ones for existing ATP provers. |
| Outcome: | The proposed framework can be used to prove hard mode statements on ATP benchmarks. |