\documentclass{article}




\usepackage[preprint,nonatbib]{neurips_2025}








\usepackage[utf8]{inputenc} %
\usepackage[T1]{fontenc}    %
\usepackage{hyperref}       %
\usepackage{url}            %
\usepackage{booktabs}       %
\usepackage{amsfonts}       %
\usepackage{nicefrac}       %
\usepackage{microtype}      %
\usepackage{xcolor}         %
\usepackage{enumitem}
\usepackage{graphicx}
\usepackage{multirow}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{wasysym}
\usepackage{wrapfig}
\usepackage{makecell}

\usepackage{mathtools}
\usepackage{amsthm}

\usepackage{multirow} 
\usepackage{booktabs}

\usepackage{bussproofs}
\usepackage{comment}

\usepackage{enumitem}

\usepackage{soul} %
\usepackage{fontawesome5}

\usepackage{epigraph}
\newcommand{\zxh}[1]{{\color{purple}#1}}
\setlength{\epigraphwidth}{0.5\textwidth}

\definecolor{keywordcolor}{rgb}{0.7, 0.1, 0.1}   %
\definecolor{tacticcolor}{rgb}{0.0, 0.1, 0.6}    %
\definecolor{commentcolor}{rgb}{0.4, 0.4, 0.4}   %
\definecolor{symbolcolor}{rgb}{0.0, 0.1, 0.6}    %
\definecolor{sortcolor}{rgb}{0.1, 0.5, 0.1}      %
\definecolor{attributecolor}{rgb}{0.7, 0.1, 0.1} %
\usepackage{listings}
\def\lstlanguagefiles{lstlean.tex}
\lstset{
    language=lean,
    inputencoding=utf8,
    extendedchars=true,
    moredelim=[is][\colorbox{yellow}]{「}{」},
}

\newcommand\bigforall{\mbox{\Large $\mathsurround0pt\forall$}} 
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{assumption}[theorem]{Assumption}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\title{Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving}




\author{Qi Liu, Xinhao Zheng, Renqiu Xia, Xingzhi Qi, Qinxiang Cao$^{*}$, Junchi Yan$^{*\dagger}$ \\
Sch. of Computer Science \& Sch. of Artificial Intelligence, Shanghai Jiao Tong University \\
\small{\texttt{\{purewhite,void\_zxh,xiarenqiu,dennyqi123,caoqinxiang,yanjunchi\}@sjtu.edu.cn}}\\\\\vspace{-10pt}
\faGithub\ \small{\textcolor{magenta}{\url{https://github.com/Purewhite2019/formal_problem_solving_main}}}
}


\begin{document}

\maketitle

\begin{abstract}

\renewcommand{\thefootnote}{} %
\footnotetext{$^*$Correspondence. $^\dagger$Also affiliated with Shanghai Artificial Intelligence Laboratory.} %
\renewcommand{\thefootnote}{\arabic{footnote}}

As a seemingly self-explanatory task, \textit{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, \textbf{FPS} (\textit{\underline{F}ormal \underline{P}roblem-\underline{S}olving}), which utilizes existing FTP (formal theorem proving) environments to perform process-verified problem-solving; and \textbf{D-FPS} (\textit{\underline{D}eductive \underline{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: \textbf{FormalMath500}, a formalization of a subset of the MATH500 benchmark; \textbf{MiniF2F-Solving} and \textbf{PutnamBench-Solving}, adaptations of FTP benchmarks MiniF2F and PutnamBench.
For faithful, interpretable, and human-aligned evaluation, we propose \textbf{RPE} (\textit{\underline{R}estricted \underline{P}ropositional \underline{E}quivalence}), a symbolic approach to determine the \textit{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.
\end{abstract}

\vspace{-5mm}
\epigraph{\small\textit{``In five minutes you will say that it is all so absurdly simple.''}\quad\quad\textit{--- Sherlock Holmes}}{Sir Arthur Conan Doyle, \textit{The Adventure of Dancing Men}}
\vspace{-5mm}

\begin{figure*}[t!]
  \centering
  \includegraphics[width=1\linewidth]{figs.FPS.pdf}
  \caption {Advantages of Formal Problem-Solving (FPS) and Deductive-FPS (D-FPS). \textbf{(a)} Even with sophisticated enhancements, LLMs may make reasoning flaws; \textbf{(b) (c)} FPS and D-FPS perform process-level verified problem-solving inside formal theorem proving environments; \textbf{(c)} D-FPS decouples answer deduction and validation to improve readability; \textbf{(d)} Informal answer checking suffer from false negatives on complex objects; \textbf{(e)} Restricted Propositional Equivalence (RPE) evaluates answers with symbolic heuristic in formal verification for stronger expressiveness.}
  \vspace{-15pt}
\end{figure*}

\input{introduction}
\input{related}
\input{method}
\input{evaluation}
\input{experiment}
\input{conclusion}

\bibliographystyle{IEEEtran}
\bibliography{custom}

{
\small
}

\newpage
\appendix

\input{appendix.background}
\input{appendix.related_works}
\input{appendix.discussion_reasoning_pattern}
\input{appendix.template}
\input{appendix.exemplar_formulations}
\input{appendix.proofs}
\input{appendix.case_study_rpe}
\input{appendix.benchmark}
\input{appendix.case_study}
\input{appendix.prompts}
\input{appendix.env}
\input{appendix.limitations}
\input{appendix.ethics_statement}






 













    


    







\typeout{get arXiv to do 4 passes: Label(s) may have changed. Rerun}

\end{document}