Qi Liu, Xinhao Zheng, Renqiu Xia, Xingzhi Qi, Qinxiang Cao, Junchi Yan
展开摘要收起
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). This leaves constructive problem-solving (finding unknown terms that satisfy specific conditions) underexplored and disconnected from process-level verifiability. To bridge this gap, we introduce **FPS** (_**F**ormal **P**roblem-**S**olving_), a principled framework to encompass the end-to-end problem-solving process in Lean 4. In FPS, the answer is an unknown metavariable coupled with a proof obligation, forcing it to be mathematically derived and verified. We further present **D-FPS** (_**D**eductive **FPS**_), which structures solving into forward derivation and backward verification, aligning more closely with human reasoning steps. Three benchmarks of over 1,000 problems are constructed for evaluation: **FormalMath500**, **MiniF2F-Solving**, and **PutnamBench-Solving**. We further propose **RPE** (_**R**estricted **P**ropositional **E**quivalence_), a symbolic metric that evaluates semantic correctness beyond brittle string matching. Extensive experiments with state-of-the-art provers reveal that solving is significantly harder than proving, highlighting the ``alignment tax'' required to transition from loose validity checking to constructive, human-aligned reasoning. Code and data are available at [https://github.com/Purewhite2019/formal_problem_solving_main](https://github.com/Purewhite2019/formal_problem_solving_main).