Pseudo-Formalization for Automatic Proof Verification

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

scope and claim

This paper proposes a natural-language proof representation and an LLM checking procedure. A Pseudo-Formal proof is a sequence of modules, each with premises, a conclusion, and a proof, plus a directed acyclic invocation graph and a scope-inheritance forest. Block Verification (BV) checks modules independently; a calibration model combines module reports. This is a proof-review technique, not machine-checked formal verification. The paper explicitly trades certainty for applicability: “Pseudo-Formalization gives up the correctness guarantee in exchange for being applicable to mathematics that current formal libraries cannot express” (Section 6, p. 13). The authors state that each step calls “a single off-the-shelf LLM with no fine-tuning” (Section 3, p. 5).

technique 1: represent proofs as modules and two graphs

Use this when a long natural-language argument is difficult to review as one context. For every module, write (P, c, π): premises, conclusion, and proof. Add an edge in invocation DAG G when one proof invokes another conclusion. Add an edge in scope forest T when a module inherits premises from a parent. A verifier reconstructs a module’s full premises from its own premises plus all ancestor scopes. Require G to be acyclic and T to be a forest; the first prevents circular arguments and the second prevents conflicting inherited scopes (Definition 1, Section 2, p. 3).

The paper defines: “A Pseudo-Formal proof is a sequence of modules V = {vi = ( Pi , ci , πi ) : i ∈ [n]}, equipped with a directed acyclic graph (DAG) G for the invocation dependency and a forest T for scope inheritance.” (Definition 1, p. 3). The paper’s own procedure in this part is only Definition 1 plus the verification order of Section 2 (p. 4): verify the nodes of G “in reverse order of its topological sort”, so that every child a node invokes is already verified. The prompts of Appendix C.2 (pp. 21-23) show how the authors ask the translator to build the tree: at most two layers (propositions, lemmas) below the theorem, numbered sequentially, with no trivial decompositions and with assumptions restated when tracing back through several statements would be needed. For their Hard2Verify runs the paper notes that “tree depth is capped at 3” (Section 4.1, p. 9). Good Pseudo-Formal Proofs (Definition 2, Appendix A, p. 18) have bounded depth of T and bounded length of each conclusion, premises and proof.

Inference: Practical steps for a user of this technique are: split the argument into premises, conclusion and proof text; give each module a stable identifier; record invoked modules in G and inherited context in T. The paper does not list these as steps.

Inference: For Verus, this maps naturally to lemma contracts: module premises become requires, conclusions become ensures, and child lemmas become explicit calls in a proof function. Scope inheritance should be made explicit in parameterized predicates because Verus has no Pseudo-Formal scope forest. This inference does not make the LLM prose a verified proof.

technique 2: block verification with calibration

Use this to check each local argument while preserving enough context to understand dependencies. Run the block verifier once per module, showing full inherited premises, the module conclusion and proof, and child premises/conclusions while assuming child correctness. It returns accept or an error description. A calibrator then receives all reports and a desired strictness threshold and emits a final verdict or locations in the original proof.

The paper states: “To verify a node ( Pi , ci , πi ) of the Pseudo-Formal proof we simply (1) realize the full premises Pfull of the node using the inheritance forest T, and (2) check that πi serves as a valid proof of ci from Pfull”, adding that the check must confirm that “whenever πi invokes the conclusion of a child node, it has proven the premises of said child hold before doing so.” (Section 2, p. 4). It also states: “the block-verification LLM is invoked once per node v = ( P, c, π ).” (Section 3.2, p. 5). The calibrator “receives the full list of per-module error reports together with a natural language description of the desired strictness threshold, and emits a final verdict” (Section 3.2, p. 6). In the experiments the calibrator does more than aggregate: for Hard2Verify it maps block errors back to the original steps, and the “No Calibrator” ablation, which keeps the same block flags but does no independent re-grading, “falls below the plain LLM-as-judge baseline” (Appendix B, p. 20). In the block-verifier prompt (Appendix C.5, pp. 25-26) the established results are to be treated as correct and not re-verified, so in practice the module checks do not depend on the order in which they run.

Theoretical support (Theorem 1, Section 2, p. 4; formal version Theorem 2, Appendix A, pp. 18-19): for a Good Pseudo-Formal proof, block-wise verification can be simulated by O(n) calls to a fixed-size Transformer with context length independent of n. The proof relies on the chain-of-thought Transformer simulation result of Merrill and Sabharwal [22] and assumes the module verifier halts in time linear in the length of its input. The authors say it should be viewed “as a theoretical tool” to model context rot (Section 2, p. 4). Inference: it says nothing about whether an actual LLM verifies a block correctly.

Inference: In a Verus pipeline, the corresponding safe operation is to compile each module into a lemma and let Verus check it, then use a separate reporting layer to aggregate failures. An LLM acceptance report is evidence for triage only; it is not a substitute for Verus’s solver and kernel checks.

technique 3: faithful translation and self-repair

Use this when the input is ordinary prose and needs decomposition. A translation LLM rewrites the proof into the module format. Optionally run a self-repair loop: show the original proof and current rewrite, ask for discrepancies, and patch them, or exit the loop if there are none. The paper says this loop is optional: “Self-repair is not fundamental to our method, but it is a simple and effective way to improve the quality of the translation.” (Section 3.1, p. 5). A representative example (IMO 2024 P6, Figure 2, p. 5) isolates an invalid strengthening, from “S cannot contain both d and −d” to “all nonzero elements of S have the same sign”, into one lemma, allowing BV to flag it.

The paper’s process is: “(1) An LLM translates Π into a Pseudo-Formal proof Π̂, with an optional self-repair loop that compares Π̂ against Π and patches discrepancies.” (Section 3, p. 4). The next steps are independent block verification, calibration, and repeated runs. The appendices describe the implementation of this step as a faithfulness check on the rewrite followed by regeneration: on Hard2Verify, each component is checked against the original proof in its own call, and the rewriter is called at most 3 times (Appendix C.3-C.4, pp. 23-25); on arXiv papers a single faithfulness call covers the whole rewrite and the rewriter is called at most 5 times (Appendix E, pp. 30, 33-35). If the rewrite is still flagged after the last attempt, the pipeline proceeds to block verification anyway. In the Hard2Verify ablation, dropping the faithfulness check lowers performance “by a small amount” while saving roughly a quarter of the cost (Appendix B, p. 19). Translation remains a failure point: “In practice producing a faithful Pseudo-Formal rewrite is not trivial.” (Section 7.1, p. 14).

Inference: For Verus, translation should generate compilable Rust specifications and proof obligations, then Verus must reject any mismatch. Faithfulness checking can compare source spans and generated contracts, but it cannot prove semantic equivalence without a formal relation.

technique 4: pessimistic parallel scaling and benchmark measurement

Run the stochastic translation, block checks, and calibration independently k times. Accept only if every run accepts; for error finding, take the union of flagged errors. The paper says that increasing k makes “recall tends to rise with k while precision tends to fall”, exposing a precision-recall operating curve (Section 3.3, p. 6). The paper reports Hard2Verify with 200 proofs from 80 olympiad/Putnam problems (Section 4.1, p. 6); ArxivMathGradingBench with 100 arXiv papers and 109 known errors (Section 1, p. 3), with author-disclosed error locations (Section 4.2, p. 9); and FirstProofGradingBench with 16 referee-agreed proofs (13 flawed, 3 correct) and 24 deduplicated errors (Section 5, pp. 11-12).

The paper says: “we accept a proof only if every one of the k runs accepts it (a single flagged error suffices to reject).” (Section 3.3, p. 6). On Hard2Verify with GPT-5.4 mini, PF+BV and the baseline both recover around 90% of the errors (Figure 3 caption, p. 7), and at k=8 PF+BV flags 28% fewer false steps per proof than baseline (Section 4.1, p. 8). At the whole-proof level, PF+BV outperforms the baseline in recall by a large margin “but does not dominate in terms of precision” (Section 4.1, p. 8). On ArxivMathGradingBench even at k=8 “both verifiers leave roughly 40% of annotated ground-truth errors uncaught” and precision is low (Section 4.2, p. 10). On FirstProofGradingBench (GPT 5.5, one PF per proof reused across the parallel BV runs), a single run recovers 0.66 of referee-identified errors at 0.77 precision, versus baseline 0.54 recall at 0.76 precision; PF recall rises to 0.71 with more runs (Section 5, p. 12). ArxivMathGradingBench precision is a lower bound because undisclosed real errors count as false positives.

Cost: PF is much more expensive per rollout. Table 3 (Appendix G, p. 57) reports $264.24forHard2VerifyPFversus$30.07 for the baseline, and $772.17versus$75.60 on arXiv. The authors state the PF improvement “cannot be attained by simply scaling inference-time compute”.

Inconsistency in the paper: the Section 1 and Section 4.2 text and Table 3 use 100 arXiv papers, but Appendix D (pp. 29-30) says that after removing papers with a non-permissive license or a false-positive comment “This leaves us with the 35 papers we use for the final dataset”, and Figure 5 uses “a 35 problem subset”. Section 4.2 gives 2023 to 2025 as the date range while Appendix D gives January 1 to July 30, 2025. The study does not resolve this.

Inference: For agent-written verified Rust, this method is a medium-to-high review aid but a low assurance mechanism: it may expose omitted premises and local jumps, yet it cannot establish executable correctness. Product risk remains that a fluent but wrong module passes all LLM runs, especially when translation changes meaning.

trust, limitations, and what not to redo

The theoretical context result assumes “Good Pseudo-Formal Proofs,” with concise nodes and bounded scope depth; it “takes the existence of such a proof as given” (Section 7.1, p. 14) and does not prove that an LLM can produce one faithfully. The benchmarks are mathematical only. ArxivMathGradingBench labels only author-disclosed locations, so precision is a lower bound; FirstProof is small (16 proofs). Trusted parts include every LLM translator, verifier, calibrator, prompt, model version, and the LLM used to match predicted errors to benchmark labels (GPT 5.4 mini for arXiv, GPT 5.5 for FirstProof; the authors checked eight FirstProof matches and disagreed with two, Appendix F.10, p. 56). No Coq, Lean, Verus, or proof kernel checks the natural-language proof. Inference: VL should not treat PF+BV as a replacement for compiling and proving Rust contracts; its reusable idea is dependency-aware decomposition and independent checking of local obligations.

techniques for the catalog

• pseudo-formal module decomposition — represent prose proofs as premise/conclusion/proof modules with invocation DAG and scope forest
• block verification — check each module with inherited context and already checked child conclusions
• translation self-repair — compare an LLM rewrite against source prose and patch discrepancies
• pessimistic parallel checking — union errors or require all independent runs to pass to trade precision for recall Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “We use an LLM judge (GPT 5.4 mini in the case of our experiments) to decide if the errors outputted by the verifier match those of the ground truth labels.”): read the whole text including appendices A-G; checked every quotation word for word, all numbers (200 proofs, 80 problems, 100 papers, 109 errors, 16 proofs, 13/3, 24 errors, 0.66/0.77/0.54/0.76, 28%, around 90%), and page and section references against the PDF pages; changed wrong page numbers (Definition 1 is p. 3, the verification quote p. 4, Section 3.3 p. 6), a capitalized quotation, an invented paraphrase in quotation marks in the IMO example, the unsupported “steps” lists (now marked Inference), and added the appendix details on faithfulness checking, calibration, cost, the whole-proof precision caveat, and the 100-versus-35 paper inconsistency; did not check the cited external papers, the released benchmarks or code, the figure curves beyond what the text and captions state, or the proof of Theorem 2 beyond reading it.

Last edited: 2026-10-17