BiVerify: Closing the Loop Between Backward and Forward Verification for Mathematical Self-Correction

Paper: 2611.11368
Authors: Rui Zou, Xin Zhao, Mengqi Wei, Ji-Rong Wen (Gaoling School of Artificial Intelligence, Renmin University of China; Central China Normal University)
Categories: cs.AI

The Gap

Despite rapid advances in frontier reasoning models (e.g., DeepSeek-R1, GPT-o-series, Gemini-Thinking), large language models (LLMs) continue to stumble on intricate, multi-step mathematical problems. A critical bottleneck is their inability to reliably self-correct: when asked to reflect on their own mistakes, LLMs frequently fall into hallucinations, “confirming” invalid solutions or rewriting correct answers into incorrect ones (negative damage transitions $C \to W$).

Existing verification paradigms predominantly operate in a single direction, each harboring fatal structural blind spots:

1. Backward Verification (Answer-to-Constraint): Starts from the proposed final answer and substitutes it back into the original problem constraints (e.g., ProgCo).
   The Blind Spot: Passing surface-level constraints does not guarantee that the reasoning path was logically valid, nor does it guarantee objective completeness (e.g., finding all valid roots, non-trivial boundary solutions, or global extrema).
2. Forward Verification (Premise-to-Conclusion): Reads the solution step by step from problem conditions, verifying each deduction sequentially (e.g., Process Reward Models / PRMs).
   The Blind Spot: On long reasoning chains, forward checkers suffer from error accumulation and cognitive drift, frequently losing sight of global boundary constraints or accepting plausible-sounding but mathematically vacuous intermediate claims.

                    THE UNIDIRECTIONAL VERIFICATION DILEMMA

  Problem q: Solve f(x) = 0 under global constraints C

  [Backward Verification]:
  Answer a_0 ──> Check against constraints C?
  ├── Pros: Bypasses complex intermediate algebraic drift.
  └── Cons: Blind to faulty reasoning paths and missing root sets (e.g., missed x_2).

  [Forward Verification]:
  Condition q ──> Step 1 ──> Step 2 ──> ... ──> Step K
  ├── Pros: Checks local logical entailment (q ∧ c_1 ... |= c_k).
  └── Cons: Accumulates verification error on long chains; easily overlooks global invariants.

  Missing Piece: How to close the loop between both directions without invalidating states?

The Increment

One sentence: Renmin University researchers propose BiVerify, an agentic mathematical verification system that establishes a formal state machine coordinating backward constraint checking and forward claim entailment over the exact same solution candidate, dynamically managing direction switching, candidate updates, and state resets while offloading exact calculations to shared symbolic tools.

                          BIVERIFY BIDIRECTIONAL ARCHITECTURE

                                 Problem q + Response y_0
                                            │
                                            ▼
                          Extract Candidate Answer a_0: C_0 = (q, y_0, a_0)
                                            │
                        ┌───────────────────┴───────────────────┐
                        │                                       │
                        ▼                                       ▼
             [Backward Verification]                 [Forward Verification]
             Constraint Decomposition                Claim Extraction: K_t = {c_{t,i}}
             Adjudication: A^B_ver                   Step Entailment: q ∧ c_{<i} |= c_i
                        │                                       │
                        └───────────────────┬───────────────────┘
                                            │
                                            ▼
                               [Bidirectional Scheduler S]
                                State: Σ_t = (C_t, B_t, F_t, d_t)
                                            │
              ┌─────────────────────────────┼─────────────────────────────┐
              │ B_t = Pass ∧ F_t = Pass     │ s_t = Pass ∧ ¬Accept        │ s_t = Fail
              ▼                             ▼                             ▼
       [TERMINAL ACCEPT]            [SWITCH DIRECTION]            [UPDATE / REFINE]
       Candidate is certified!      d_t ──> Other(d_t)            Generate Proposal Ĉ_t
                                                                  Reset: B = F = Unknown!

Core Framework & Mechanisms

1. Bidirectional Scheduling State Machine

BiVerify formulates verification as a closed-loop discrete dynamical system. For candidate $C_t = (q, y_t, a_t)$ at turn $t$, the scheduling state is: $\Sigma_t = (C_t, B_t, F_t, d_t)$ where $B_t, F_t \in \{\text{Unknown}, \text{Pass}, \text{Fail}\}$ represent the directional verification verdicts, and $d_t \in \{B, F\}$ is the active direction.

The system enforces a strict Joint Acceptance Criterion: $\text{Accept}(C_t) \iff B_t = \text{Pass} \wedge F_t = \text{Pass}$ Crucially, pass states are candidate-bound: if candidate $C_i$ passes backward checks and an updated proposal $C_j$ ($j \neq i$) passes forward checks, neither is accepted. Prior verification records are wiped whenever a candidate is updated, preventing cross-candidate state pollution.

The scheduling transition function $S(\Sigma_t, s_t, \hat{C}_t)$ follows: