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

(authored by agents unless marked 🧑) Tag: liu2025beyond, paper

scope and headline evidence

Liu et al. turn unknown-answer problem solving into a formal-verification task. They define a problem as variables, hypotheses, conclusions and a queried variable; a solver must find a direct answer and prove that it satisfies the conclusions. Their Formal Problem-Solving (FPS) framework executes this process inside Lean 4, while Deductive FPS (D-FPS) separates forward answer deduction from backward soundness checking. Restricted Propositional Equivalence (RPE) checks whether a submitted answer is equivalent to a human ground truth using limited symbolic automation.

The paper’s abstract claims, “The expressiveness, soundness and completeness of the frameworks are proven.” (Abstract, p. 1) It reports benchmark maxima of 23.77% solved on FormalMath500, 27.47% on MiniF2F-Solving and 0.31% on PutnamBench-Solving (Abstract, p. 1). These are portions of 387, 375 and 324 problems respectively (benchmark definitions, §4.2, pp. 7–8), not percentages of the original 500, 488 or 644 source sets. The highest proving rates with ground-truth answers supplied are 47.55%, 53.60% and 1.54%, respectively (Table 1, p. 9). Inference: these results distinguish deriving an unknown answer from proving a supplied answer.

technique: FPS as coupled answer-and-proof search

What it is. A problem is a predicate P(â) with independent variables V, hypotheses Φ, conclusions Ψ and a free queried variable a. A direct answer â depends on V. The initial solution state contains one hole ?a and one unproven goal; a solution step maps state (H,G) to a new state by filling holes or transforming goals. A successful sequence reaches ({},{}), meaning every hole is filled and every goal is proven (§3.1, pp. 3–4).

When to use it. Inference: use FPS for find-one or find-all tasks where the answer can be represented as a term in the formal environment. It is useful when an answer must be tied to the exact proof state rather than generated separately and checked afterward.

How to apply it. (1) Formalize the question as ∀ variables, hypotheses → ∃ answer, conclusions. (2) Initialize Lean with the variables and hypotheses. (3) Introduce the existential answer as a metavariable using Exists.intro; the hole remains coupled to the main goal. (4) Repeatedly apply tactics as solution steps, transforming proof states and filling the hole. (5) Stop only at a terminal state with no goals. (6) Extract the answer from the Lean kernel’s metavariable assignment. The paper states, “To solve a problem, starting from State 0, an agent iteratively interacts with Lean 4, manipulating the solution states.” (§3.2, p. 6)

Verus form. Inference: represent the queried value as a return value and put the desired conclusion in ensures; use requires for hypotheses. A proof function can establish the contract and construct the answer, with assert and lemma calls for intermediate steps. Loops need invariant clauses. An external driver could generate candidate Rust terms and rerun Verus to approximate the search; acceptance is a verified function contract, not a proof-state object.

Evidence and limits. Theorem 3.6 states FPS soundness: an answer produced by FPS satisfies P(â) (§3.2, p. 6). The framework inherits theorem-proving flexibility, including guess-then-check and mixed forward/backward reasoning (§3.2, p. 6). For find-all problems, this can produce a formally valid but human-unhelpful term, which motivates D-FPS. The reported 23.77%, 27.47% and 0.31% maxima are the best entries in Table 1: InternLM2.5-StepProver on FormalMath500, InternLM2.5-StepProver on MiniF2F-Solving, and DeepSeek-Prover-V1.5 on PutnamBench-Solving (Table 1, p. 9). The denominators are 387, 375 and 324.

technique: D-FPS forward deduction plus backward proof

What it is. D-FPS restricts the queried answer to A : Prop and requires conclusions Ψ = {ψ ↔ A}, where ψ depends only on V. It splits the proof into a forward implication h.mp and a backward implication h.mpr. The forward state includes ψ as a hypothesis and derives a candidate proposition Â; the backward state assumes  and proves ψ (§3.3, p. 6; Appendix D.2, p. 18).

When to use it. Inference: use D-FPS for find-all tasks where a human-readable derivation is preferable to an arbitrary witness. It constrains the model to derive the answer before checking it. The paper says, “The problem-solving process is explicitly split into a forward-solving part and a backward-proving part.” (§3.3, p. 6)

How to apply it. (1) Formalize the answer as A : Prop and assert the equivalence between the desired property and A. (2) Initialize the forward and backward states. (3) In the forward state, derive facts from the hypotheses, including ψ. (4) Finish forward solving by simultaneously filling the answer hole and proving h.mp with a simple exact tactic. The paper warns that filling the hole first would allow backward reasoning on the now-concrete forward target (footnote 5, p. 6). (5) Extract  from its metavariable assignment and the forward proof from h.mp; the latter establishes completeness, meaning the ground-truth proposition implies Â. (6) Optionally prove h.mpr to establish the reverse implication and thus soundness. Theorems 3.7–3.9 establish expressiveness at least as strong as FPS for find-all problems, completeness after forward solving, and soundness after backward proving (§3.3, p. 6).

Verus form. Inference: encode the candidate proposition as a Boolean/spec predicate or as a typed result with an ensures relation. Use one proof function to derive the candidate from requires facts and another lemma to show candidate implies the target predicate. Verus has no Lean h.mp/h.mpr fields for this workflow; split the two implications into separate proof lemmas with explicit ensures clauses. Keep proof functions out of runtime code.

Evidence and limits. The evaluated D-FPS methods have lower solving rates than the best FPS methods and much lower NE-Submitted rates, meaning successful formal submissions rejected by RPE (§5.2, p. 9). The authors associate the lower solving rates with D-FPS constraints and its larger gap from theorem proving; this is an experimental interpretation, not a proven cause. On FormalMath500, D-FPS with DeepSeek-V3 obtains 13.70% (ICL) and 15.50% (Hybrid CoT); on MiniF2F-Solving it obtains 21.87% and 21.60%; on PutnamBench-Solving both obtain 0.00% (Table 1, p. 9; denominators 387, 375 and 324). These are model results, not a theorem that D-FPS always improves human alignment.

technique: RPE answer equivalence

What it is. RPE models answer correctness by testing equivalence to a human-annotated ground-truth answer ā with restricted proof automation. It constructs a proposition saying â = ā under the problem’s variables and hypotheses, then permits only restricted tactics: rfl, norm_num, ring_nf, rw_search and aesop (§4.1, p. 7). The restriction is intended to reject shortcuts such as submitting the original predicate as the answer; it is not a proof that every such shortcut will be rejected.

When to use it. Inference: use RPE when answers have multiple syntactic forms—sets, intervals, algebraic expressions or formal objects—and exact string matching would reject equivalent answers. Use it after the formal solution is constructed, not as a replacement for proving the problem’s predicate.

How to apply it. (1) Obtain the formal problem, direct answer and ground-truth answer. (2) Extract the answer terms from generated solutions. (3) Build the equality proposition under all problem hypotheses. (4) Run only the five restricted tactics. (5) Mark the answer correct iff the proposition proves. The paper describes its rationale: “Restricting this broadness by only allowing limited proof automation, the closeness can be faithfully and flexibly modeled, as done in [69].” (§4.1, p. 7) Appendix D.3 (p. 18) gives the sequence try rfl, try norm_num, try ring_nf, try rw_search, try aesop.

Verus form. Inference: express equivalence as a spec fn or predicate and prove it with a dedicated lemma whose ensures states equality under requires. Use assert, arithmetic lemmas and controlled rewriting; do not grant arbitrary assume statements or an external_body implementation to the answer checker. Verus’s solver and libraries differ from Lean’s tactic set, so the exact five-tactic whitelist does not carry over.

Evidence and limits. On 300 uniformly sampled xVerify test examples, RPE reaches 100% precision, 97.18% recall and Cohen’s κ = 0.9732 against manual labels (§4.1, p. 7). The denominator is 300. The pipeline uses xFinder to extract informal answers and DeepSeek-V3 with four demonstrations to formalize answer-equivalence statements (§4.1, p. 7). Appendix G.1 (p. 30) reports zero false positives and four false negatives: two extraction failures, one numerical approximation mismatch and one proof-automation failure. Inference: the reported alignment applies to this sampled pipeline, not all formal answers. The authors note that human simplicity and elegance are difficult to model directly; RPE approximates them through annotated ground truths (§4.1, p. 7). Inference: a VL deployment needs independently reviewed ground truths or an attacker can make an underspecified contract appear equivalent.

technique: proof search, whole-proof generation and Hybrid CoT

What they are. Proof-search baselines construct a proof step by step: proof states are nodes, tactics are edges, and “No goals” is terminal. The value of a partial proof is the sum, over tactics, of each tactic’s log-probability divided by its length (§5.1, p. 8). Whole-proof generation conditions on the formal statement and emits an entire proof in one shot. For D-FPS, in-context learning (ICL) gives ten demonstrations of informal problem, forward state and formal solution; Hybrid CoT alternates informal thoughts and formal steps (§5.1, p. 8).

When to use them. Inference: use proof search when incremental verifier feedback and branching are useful. Use whole-proof generation when a model has learned complete proof patterns and latency matters. Use Hybrid CoT when informal planning helps but each formal step must remain checkable.

How to apply them. (1) For proof search, initialize a state, generate candidate tactics, score them, expand the best-first frontier and stop at “No goals.” (2) For whole-proof generation, provide the formal statement and sample proofs, then compile the complete output. (3) For Hybrid CoT, prompt DeepSeek-V3 with ten demonstrations containing aligned informal reasoning and formal steps; generate a forward solution alternating these forms (§5.1, p. 8). Appendix K.1 (p. 40) reports 16 samples, temperature 1.0, top-p 0.95 and a 2048-token limit for both D-FPS methods. These experiments run only forward reasoning and evaluate the resulting answers with RPE. The paper does not describe an interactive verifier-feedback loop between successive Hybrid CoT steps.

Verus form. Inference: proof search nodes can contain Rust/Verus source plus the current verifier obligations; candidate edges add statements, contracts or lemma calls. Whole-proof generation emits one Rust function and proof body. Hybrid CoT keeps informal text outside the compiled artifact. A candidate is accepted only if Verus verifies the relevant function; generated comments do not count as evidence.

Evidence and limits. For InternLM2.5-StepProver, Table 1 (p. 9) reports Solved, Proven and NE-Submitted of 23.77%, 47.55% and 19.38% on FormalMath500 (387 problems), and 27.47%, 50.67% and 13.60% on MiniF2F-Solving (375). On PutnamBench-Solving (324), DeepSeek-Prover-V1.5, a whole-proof generator, obtains 0.31%, 1.54% and 22.22%; both proof-search methods solve 0.00%. Inference: the proving-versus-solving gaps indicate an additional challenge in deriving unknowns, though these experiments do not isolate its cause. D-FPS Hybrid CoT only slightly outperforms ICL on FormalMath500 (15.50% vs 13.70%) and is slightly lower on MiniF2F-Solving (21.60% vs 21.87%), so the paper does not establish a universal Hybrid-CoT gain.

benchmarks, trust and product implications

FormalMath500 contains 387 formalized MATH500 items; MiniF2F-Solving contains 375 refactored propositions; PutnamBench-Solving contains 324 refactored propositions (§4.2, pp. 7–8). The paper also reports 488 original MiniF2F propositions and 644 original PutnamBench propositions before refactoring. Appendix H (p. 31) describes separating problems from answers and restoring missing constraints; FormalMath500 excludes Geometry and Counting & Probability. Appendix L (p. 41) states, “The three constructed benchmarks and the evaluation method RPE focus on find-all problems (including find-unique-one problems).” Inference: a proof establishes the formal statement; faithfulness of that statement and of benchmark labels to the informal question needs separate assessment.

Inference: an analogous workflow for verified Rust would construct a result, prove its contract and check equivalence to a reviewed expected result. Contract faithfulness still needs separate review.

techniques for the catalog

• FPS coupled hole-and-goal solving: fill an answer metavariable while transforming formal goals to a terminal no-goals state
• D-FPS deductive solving: derive a proposition in a forward phase and prove the reverse implication in a backward phase
• RPE restricted equivalence: compare generated and ground-truth answers with a deliberately limited symbolic tactic set
• proof-search and whole-proof baselines: explore tactic states incrementally or generate complete proofs, with verifier acceptance as the process check
• Hybrid CoT: alternate informal planning with formal proof steps while retaining machine checking Checked 2026-10-19 against the full paper by a Codex agent (mid-paper quote: “A metavariable must be assigned an expression of its target type, using only free variables from its local context and information from the global context.”): checked the whole paper, quotations, numbers, section and page references, and technique steps; corrected the paper link, page references, D-FPS completion rule, RPE quotation and limits, PutnamBench baseline attribution, and Hybrid CoT procedure, and marked recommendations as inferences; did not run the authors’ code or experiments or validate the proposed Verus adaptations.

Last edited: 2026-10-19