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

TL;DR

The work formalizes problem-solving as a deterministic Markov decision process and introduces FPS and Deductive FPS (D-FPS) to enable end-to-end, process-verified problem-solving inside formal theorem proving environments like Lean 4. It provides rigorous formal definitions, proofs of soundness, completeness, and expressiveness, and introduces Restricted Propositional Equivalence (RPE) as a human-aligned evaluation metric. Three benchmarks—FormalMath500, MiniF2F-Solving, and PutnamBench-Solving—are constructed to enable faithful informal-formal comparisons and rigorous evaluation of baseline FTP models and prompting methods. Experimental results show that current baselines solve up to about 24% on FormalMath500 and 28% on MiniF2F-Solving, with proving performance substantially higher, underscoring gaps between solving and proving and highlighting the potential of D-FPS for human-aligned reasoning. The study proposes future directions in SFT data collection and improved integration of FPS/D-FPS capabilities to advance trustworthy, verifiable AI problem-solving.

Abstract

As a seemingly self-explanatory task, problem-solving has been a significant component of science and engineering. However, a general yet concrete formulation of problem-solving itself is missing. With the recent development of AI-based problem-solving agents, the demand for process-level verifiability is rapidly increasing yet underexplored. To fill these gaps, we present a principled formulation of problem-solving as a deterministic Markov decision process; a novel framework, FPS (Formal Problem-Solving), which utilizes existing FTP (formal theorem proving) environments to perform process-verified problem-solving; and D-FPS (Deductive FPS), decoupling solving and answer verification for better human-alignment. The expressiveness, soundness and completeness of the frameworks are proven. We construct three benchmarks on problem-solving: FormalMath500, a formalization of a subset of the MATH500 benchmark; MiniF2F-Solving and PutnamBench-Solving, adaptations of FTP benchmarks MiniF2F and PutnamBench. For faithful, interpretable, and human-aligned evaluation, we propose RPE (Restricted Propositional Equivalence), a symbolic approach to determine the correctness of answers by formal verification. We evaluate four prevalent FTP models and two prompting methods as baselines, solving at most 23.77% of FormalMath500, 27.47% of MiniF2F-Solving, and 0.31% of PutnamBench-Solving.

Figures (3)

• Figure 1: Advantages of Formal Problem-Solving (FPS) and Deductive-FPS (D-FPS). (a) Even with sophisticated enhancements, LLMs may make reasoning flaws; (b) (c) FPS and D-FPS perform process-level verified problem-solving inside formal theorem proving environments; (c) D-FPS decouples answer deduction and validation to improve readability; (d) Informal answer checking suffer from false negatives on complex objects; (e) Restricted Propositional Equivalence (RPE) evaluates answers with symbolic heuristic in formal verification for stronger expressiveness.
• Figure 2: Demonstrations of FPS and D-FPS. FPS: After initialization, an agent iteratively executes solution steps to transform solution states until all goals are solved. A direct answer and its soundness proof can be extracted. D-FPS: The whole process is further decoupled into a forward-solving part and an optional backward-proving part. Forward-solving enforces deductive reasoning for better human readability. The direct answer and the completeness proof can be extracted upon finishing forward-solving, while the soundness proof should be extracted after finishing backward-proving.
• Figure 3: Venn diagram of all problems solved by Proof Search, Whole-Proof Generation, and Hybrid CoT.

Theorems & Definitions (13)

• Definition 3.1
• Definition 3.2
• Definition 3.4
• Definition 3.5
• Theorem 3.6
• Theorem 3.7
• Theorem 3.8
• Theorem 3.9
• Definition 4.1
• proof