title: Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal
    Problem-Solving
summary: 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.
paper_authors._id: 681c5152c7211b7efbba4b73
paper_authors.name: Qi Liu
paper_authors.status: claimed_verified
paper_authors.statusLastChangedAt: 2025-05-08T08:58:55.624Z
paper_authors._id: 641aef7b1911d3be67425338
paper_authors.avatarUrl: https://cdn-avatars.huggingface.co/v1/production/uploads/641aef7b1911d3be67425338/CmCbWWB6NxkAaus59q31w.jpeg
paper_authors.fullname: Qi Liu
paper_authors.type: user
paper_authors.user: purewhite42
paper_authors._id: 681c5152c7211b7efbba4b74
paper_authors.name: Xinhao Zheng
paper_authors._id: 681c5152c7211b7efbba4b75
paper_authors.name: Renqiu Xia
paper_authors._id: 681c5152c7211b7efbba4b76
paper_authors.name: Xingzhi Qi
paper_authors._id: 681c5152c7211b7efbba4b77
paper_authors.name: Qinxiang Cao
paper_authors._id: 681c5152c7211b7efbba4b78
paper_authors.name: Junchi Yan
paper_title: Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal
    Problem-Solving
paper_summary: 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.
paper_ai_summary: A new formal framework, FPS, for AI-based problem-solving is introduced, utilizing FTP environments and RPE for verification, with benchmarks and evaluation.
paper_ai_keywords: Markov decision process Formal Problem-Solving FPS formal theorem proving FTP FormalMath500 MiniF2F-Solving PutnamBench-Solving Restricted Propositional Equivalence RPE D-FPS Deductive FPS