source/experiment.tex

\vspace{-5pt}
\section{Experiments}
\vspace{-5pt}\label{sec:experiment}

In this section, we evaluate baseline methods for FPS and D-FPS on the three benchmarks.  Given FPS's direct affinity to TP, we take two main TP paradigms, proof search and whole-proof generation, as baselines. Moreover, to provide a side-by-side comparison with traditional TP, we evaluate these methods' proving capability by proving $P(\bar a)$ (statement asserting the soundness of the ground-truth answer).
For D-FPS, due to its novel designs relative to traditional TP, we evaluate two chain-of-thought prompting methods: direct in-context learning and hybrid CoT.
Comprehensive experiments are conducted to analyze existing obstacles and future directions thoroughly.
Please refer to Appendix~\ref{app:hyperparam} for detailed hyperparameters and Appendix~\ref{app:env} for Lean 4 environment settings.


\vspace{-5pt}
\subsection{Baseline Methods}
\vspace{-5pt}
\noindent\textbf{Proof Search} methods sequentially construct a formal proof $\boldsymbol t$ by best-first search: proof states $S_i$ are nodes, tactics $t_i$ are edges, the terminal state ``\texttt{No goals}'' is the target node. Given an LLM $p_\theta(t_i\ |\ S_i)$, the normalized log-probabilities $v_i = \sum_{j\le i}\frac{\log p_\theta(t_j\ |\ S_j)}{|t_j|}$ is used as the value function. In this paradigm, InternLM2.5-Step-Prover~\cite{wu2024internlm2} and LeanSTaR~\cite{lin2025leanstarlearninginterleavethinking} are evaluated.

\noindent\textbf{Whole-Proof Generation} methods perform conditional generation: Given a formal statement $s_\text{f}$, an LLM $p(\boldsymbol t | s_\text{f})$ directly models the distribution of the whole proof $\boldsymbol t$. In this paradigm, DeepSeek-Prover-V1.5~\cite{xin2024deepseekproverv15harnessingproofassistant} and TheoremLlama~\cite{wang2024theoremllamatransforminggeneralpurposellms} are evaluated. 

\noindent\textbf{In-Context Learning (ICL)} constructs a forward formal solution by directly prompting DeepSeek-V3~\cite{deepseekai2024deepseekv3technicalreport} with $10$-shot demonstrations, each consisting of the original informal problem, the initial forward state, and a ground-truth forward solution. The demonstrations are randomly sampled from the MATH~\cite{hendrycks2021measuring} train set, with $2$ for each subject.

\noindent\textbf{Hybrid Chain-of-Thought (Hybrid CoT)} constructs a forward formal solution by alternatively generating informal thoughts and formal solution steps to combine the flexibility of informal reasoning and the rigor of formal verification. We conduct in-context learning on DeepSeek-V3~\cite{deepseekai2024deepseekv3technicalreport} with $10$-shot demonstrations identical to In-Context Learning. Those demonstrations are manually annotated with aligned informal reasoning steps.

\begin{table}[t!]
    \centering
    \caption{Experiment results of baseline methods. \textbf{Bold} numbers highlight the best values for each metric; \textit{Solved} indicates the portion that is successfully solved; \textit{Proven} indicates the portion whose statements (asserting the correctness of ground-truth answer) are proven; \textit{NE-Submitted} indicates the portion of problems whose submitted answers are incorrect under RPE.}
    \label{tab:experiment_results}
    \resizebox{0.85\linewidth}{!}{
    \begin{tabular}{lcccccc} \midrule
    \multicolumn{1}{l}{\textbf{Framework}} & \multicolumn{1}{l}{\textbf{Dataset}} & \textbf{Method} & \textbf{Model} & \textbf{Solved}$\uparrow$ & \textbf{Proven}$\uparrow$ & \textbf{NE-Submitted}$\downarrow$ \\ \midrule
    \multirow{12}{*}{\textbf{FPS}} & \multirow{4}{*}{\makecell{Formal-\\Math500}} & \multirow{2}{*}{\makecell{Proof\\Search}} & InternLM2.5-StepProver & \textbf{23.77\%} & \textbf{47.55\%} & 19.38\% \\
    &  &  & LeanSTaR & 23.51\% & 43.41\% & 20.93\%\\ \cmidrule{3-7}
     &  & \multirow{2}{*}{\makecell{Whole-Proof\\Generation}} & DeepSeekProver-V1.5  & 22.22\% & 46.51\% & \textbf{14.47\%}\\
     &  &  & TheoremLlama & 16.02\% & 4.39\% & 15.50\%\\\cmidrule{2-7}
     & \multirow{4}{*}{\makecell{MiniF2F\\Solving}} & \multirow{2}{*}{\makecell{Proof\\Search}} & InternLM2.5-StepProver  & \textbf{27.47\%} & 50.67\% & 13.60\% \\
    &  &  & LeanSTaR & 24.27\% & 49.33\% & 14.40\% \\ \cmidrule{3-7}
     &  & \multirow{2}{*}{\makecell{Whole-Proof\\Generation}} & DeepSeekProver-V1.5  & 22.40\% & \textbf{53.60\%} & 10.93\% \\
     &  &  & TheoremLlama & 13.07\% & 7.73\% & \textbf{8.80\%}\\\cmidrule{2-7}
     & \multirow{4}{*}{\makecell{PutnamBench\\Solving}} & \multirow{2}{*}{\makecell{Proof\\Search}} & InternLM2.5-StepProver & 0.00\% & \textbf{1.54\%} & 28.09\%  \\ 
   & & & LeanSTaR & 0.00\% & 0.93\% & 41.05\%  \\ \cmidrule{3-7}
     &  & \multirow{2}{*}{\makecell{Whole-Proof\\Generation}} & DeepSeekProver-V1.5   & \textbf{0.31\%} & \textbf{1.54\%} & 22.22\% \\
     &  &  & TheoremLlama & 0.00\% & 0.31\% & \textbf{16.67\%} \\\midrule
     \multirow{6}{*}{\textbf{D-FPS}} & \multirow{2}{*}{\makecell{Formal-\\Math500}} & ICL & DeepSeek-V3  & 13.70\% & - & \textbf{0.00\%}\\
     &  & Hybrid CoT & DeepSeek-V3 & \textbf{15.50\%} & - & 1.03\%\\ \cmidrule{2-7}
     & \multirow{2}{*}{\makecell{MiniF2F\\Solving}} & ICL & DeepSeek-V3  & \textbf{21.87\%} & - & \textbf{0.00\%}\\
     &  & Hybrid CoT & DeepSeek-V3  & 21.60\% & - &\textbf{0.00\%}\\ \cmidrule{2-7}
      & \multirow{2}{*}{\makecell{PutnamBench\\Solving}} & ICL & DeepSeek-V3  & \textbf{0.00\%} & - & \textbf{0.00\%}\\
     &  & Hybrid CoT & DeepSeek-V3  & \textbf{0.00\%} & - & 0.31\%\\\midrule
    \end{tabular}
    }
    \vspace{-15pt}
\end{table}

\vspace{-5pt}
\subsection{Results and Discussions}
\vspace{-5pt}
Experiment results are summarized in Table~\ref{tab:experiment_results}, where three indicators are reported:
\begin{itemize}[leftmargin=10pt, topsep=0pt,itemsep=1pt,partopsep=1pt, parsep=1pt]
    \item \textbf{Solved.} The portion of problems whose direct answers and proofs are successfully constructed and the direct answers are correct under RPE.
    \item \textbf{Proven.} The portion of problems for which the correctness of ground-truth answers $P(\bar a)$ is proven. \textit{Proven} and \textit{Solved} compare proving a proposition and solving an unknown in parallel.
    \item \textbf{NE-Submitted.} The portion of problems whose direct answers and proofs are successfully constructed, but the direct answers are not equivalent to ground-truths under RPE.
\end{itemize}

\noindent\textbf{Comparison between Solving and Proving.}  The best indicators between proof search and whole-proof generation do not vary much. However, comparisons between \textit{Solved} and \textit{Proven} exhibit consistently\footnote{The only exception is TheoremLlama, for which we have double-checked the experiments.} high discrepancies. SOTA methods can prove $47.55\%$ of FormalMath500 and $53.60\%$ of MiniF2F-Solving. However, the highest solving rates are $23.77\%$ and $27.47\%$, nearly half of proving. We speculate that the vast difference stems from two extra requirements of problem-solving: continuously handling coupled metavariables~\cite{aniva2024pantograph} and deriving unknowns based on existing conditions. This calls for future work in supervised fine-tuning (SFT) on problem-solving data.

\noindent\textbf{Comparison between FPS and D-FPS.} Methods under the D-FPS framework result in lower solving capability than those under FPS. This meets our expectations since D-FPS has more constraints than FPS and a larger gap to TP. Notably, D-FPS demonstrates significantly lower \textit{NE-Submitted} than FPS. This might be because existing models are pretrained or SFTed on TP data, which contains severe inductive bias to construct an arbitrary term corresponding to the target type as the proof term. However, FPS requires finding a \textit{correct} term, which should not only be sound and complete but also align with human intuition. A Venn graph of solved problems can be found in Appendix~\ref{app:case_study:coverage}, where D-FPS shows a strong complementarity to FPS. Preference model experiments can be found in Appendix~\ref{app:case_study:preference}, where D-FPS demonstrates a clear advantage over FPS on human-alignment (avg. $>0.75$ on two preference models). Case studies of model-generated solutions are in Appendix~\ref{app:case_study:case_study}.

Nearly zero \textit{NE-Submitted} rate of D-FPS depicts a promising picture of unsupervised problem-solving: even without a ground-truth answer, perfect inference-scaling~\cite{stroebl2024inference} with D-FPS can derive a sound, complete, and human-aligned answer.

\noindent\textbf{Comparison between Hybrid CoT and ICL.} For D-FPS, Hybrid CoT demonstrates slightly better solving capability than ICL, and other indicators hold statistically negligible differences. Error analysis of Hybrid CoT and ICL can be found in Appendix~\ref{app:case_study:dfps_error_dist}, which reveals that current LLMs' underfitting on D-FPS might be the primary cause of their relatively low solving rate.

More discussions about limitations and potential future works are in Appendix~\ref{app:limitation}.