\vspace{-5pt}
\section{Evaluation} \label{sec:benchmark}
\vspace{-5pt}
In this section, we first define the \textit{correctness} of formal answers. Then, we propose \textbf{RPE} (\textit{\ul{R}estricted \ul{P}ropositional \ul{E}quivalence}), which determines the correctness of direct answers by propositional equality with restricted proof automation. Finally, for a comprehensive evaluation, we construct three benchmarks, \textbf{FormalMath500}, \textbf{MiniF2F-Solving}, and \textbf{PutnamBench-Solving}, whose difficulty ranges from grade school math to undergraduate competitions.

\vspace{-5pt}
\subsection{Metric}
\vspace{-5pt}
\label{sec:rpe}
\noindent \textbf{Correctness.}
Even though the soundness (and completeness, for find-all problems) of answers resulting from FPS and D-FPS are formally verified, shortcuts still exist. For example, one can cheat FPS by directly constructing answer terms based on the problem predicate or by separately proving Prop.~\ref{eq:satisfiable_dtt} and applying the axiom of choice to it. For D-FPS, one may assign the answer hole with $\bigwedge_{i=1}^q \psi_i$ itself to form a tautology. Therefore, the correctness of an answer should not only be sound (and complete) but also aligned with human preference.
\begin{definition}\label{def:correctness}
A direct answer $\hat a$ for problem $(V, a, \Phi, \Psi)$ is \textbf{\textit{correct}} if: 1) $P(\hat a)$ holds; 2) Answering $(V, a, \Phi, \Psi)$ with $\hat a$ aligns with human intuition. 
\end{definition}
\noindent \textbf{Restricted Propositional Equivalence.}
We design \textbf{RPE} (\textit{\ul{R}estricted \ul{P}ropositional \ul{E}quivalence}) to automatically, flexibly, and faithfully model correctness in human preference: Given a formal problem $(V, a, \Phi, \Psi)$, its ground-truth answer $\bar a$, and a direct answer $\hat a$, RPE holds if and only if $\forall_{i=1}^n (v_i : T_i), \bigwedge_{i=1}^p\phi_i, \hat a = \bar a$ can be proven by restricted proof automation $\mathcal T$.

The idea behind RPE is intuitive. Human preferences, e.g., simplicity and elegance, are too complicated to model without prior. Fortunately, they can be captured in the human-annotated ground-truths. Therefore, it is easier to determine whether a direct answer $\hat a$ is ``human-aligned'' by its ``closeness'' to the ground-truth answer $\bar a$. For this purpose, Propositional equality~\cite{moura2021lean}, i.e., whether $\hat a = \bar a$ can be proven, is too broad. (e.g., They cannot discriminate aforementioned tautology answer $\bigwedge_{i=1}^q \psi_i$). Restricting this broadness by only allowing limited proof automation, the closeness can be faithfully and flexibly modeled, as done in \cite{liu2025rethinking}. 

The restricted proof automation $\mathcal T$ includes the following. The code template is in Appendix~\ref{app:RPE}.
\begin{itemize}[leftmargin=10pt, topsep=0pt,itemsep=1pt,partopsep=1pt, parsep=1pt]
    \item \texttt{rfl} proves equalities up to definitional equality~\cite{moura2021lean};
    \item \texttt{norm\_num} prove equalities by normalizing numerical expressions;
    \item \texttt{ring\_nf} proves equalities in commutative rings;
    \item \texttt{rw\_search} proves equalities by repeatedly rewriting using lemmas in Mathlib 4~\cite{mathlib4};
    \item \texttt{aesop}~\cite{limperg2023aesop} is a symbolic heuristic that prioritizes normalizing and provability-preserving.
\end{itemize}

\noindent \textbf{Validation of RPE.}
To fairly and comprehensively evaluate RPE, we uniformly sampled 300 examples from the test set of xVerify~\cite{chen2025xverifyefficientanswerverifier}, each consisting of an informal problem, an informal solution generated by a diverse group of SOTA LLMs, the ground-truth informal answer, and a manually-annotated correctness label. We use xFinder~\cite{yu2025xfinder} to extract informal answers from the informal solutions and use DeepSeek-V3~\cite{deepseekai2024deepseekv3technicalreport} with 4-shot demonstrations to transform the informal answers and corresponding ground-truths into RPE statements $\forall_{i=1}^n (v_i : T_i), \bigwedge_{i=1}^p\phi_i, \hat a = \bar a$. 
(See Appendix~\ref{app:prompt:rpe_benchmark} for detailed prompt)

RPE demonstrates strong alignment with human annotators, reaching \ul{$100\%$ precision, $97.18\%$ recall, and $0.9732$ Cohen's kappa}~\cite{bhlpage55377146}. Case analysis of failures in this experiment and rejected answers in the following experiments can be found in Appendix~\ref{app:case_rpe}.


\vspace{-5pt}
\subsection{Benchmarks}
\vspace{-2pt}

We construct three datasets with broad topics and diverse difficulty, each containing four fields: informal problem, informal ground-truth answer, formal problem, and formal ground-truth answer. See Appendix~\ref{app:benchmark} for the processing details and Appendix~\ref{sec:exemplar_formalizations:benchmark} for examples.

\noindent\textbf{FormalMath500} is a formalized subset of the prevalent MATH500 benchmark~\cite{lightman2023let}, including 387 data points:
123 about \texttt{Algebra},
92 about \texttt{Intermediate Algebra},
62 about \texttt{Number Theory},
65 about \texttt{Prealgebra}, and
45 about \texttt{Precalculus}.
They cover a wide range of difficulties annotated by \cite{hendrycks2021measuring}:
38 of \texttt{Level 1},
67 of \texttt{Level 2},
87 of \texttt{Level 3},
96 of \texttt{Level 4}, and
99 of \texttt{Level 5}.

\noindent\textbf{MiniF2F-Solving} is a refactored subset of MiniF2F~\cite{zheng2022minif2fcrosssystembenchmarkformal}, which is composed of 488 propositions up to high-school competition-level. We rewrite these propositions to fit in the FPS and D-FPS framework, resulting in 375 data points with:
30 from \texttt{AIME},
140 from \texttt{MATH-Algebra},
82 from \texttt{AMC},
3 from \texttt{IMO}, and
120 from \texttt{MATH-Number Theory}.

\noindent\textbf{PutnamBench-Solving} is a refactored subset of PutnamBench~\cite{tsoukalas2024putnambench}, which consist of 644 propositions from undergraduate-level competitions. PutnamBench is a pioneer at using a \texttt{sorry} placeholder to factor out the direct answers from problem propositions. After refactoring, the subset contains 324 data points with:
9 about \texttt{Abstract Algebra},
138 about \texttt{Algebra},
122 about \texttt{Analysis},
14 about \texttt{Combinatorics},
28 about \texttt{Geometry},
25 about \texttt{Linear Algebra},
49 about \texttt{Number Theory},
8 about \texttt{Probability}, and
4 about \texttt{Set Theory}. (One problem may cover multiple subjects.)