Xingzhi Qi

Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving

Large language models (LLMs) have achieved remarkable progress in mathematical reasoning, yet persistently suffer from hallucinations and erroneous logic. While formal theorem proving (FTP) shows promise in process-level reliability, it is limited to _verification_ (checking known propositions). Thi…