Neuro-symbolic PRM: Enhancing Scientific Reasoning via Structured Traces and Symbolic Verification

# Enhancing Scientific Reasoning via Structured Traces and Symbolic Verification
Source: [https://arxiv.org/html/2608.26329](https://arxiv.org/html/2608.26329)
Cong XuAffiliation:HPE LabsSuparna BhattacharyaAffiliation:HPE LabsMartin FoltinAffiliation:HPE LabsAmit ShethAffiliation:AI Institute of South CarolinaAffiliation:Indian AI Research Organisation\{yuxin\.zi,cong\.xu,suparna\.bhattacharya,martin\.foltin\}@hpe\.com,amit@iairo\.ai

###### Abstract

While tool\-augmented Large Language Models have significantly improved multi\-step reasoning in quantitative STEM tasks, a critical residual failure mode remains: intermediate reasoning steps that are syntactically well\-formed, mathematically executable, and unit\-consistent, yet contextually ungrounded\. Current approaches either rely on formal verifiers that cannot assess semantic intent, or burden Process Reward Models \(PRMs\) with the dual task of checking both arithmetic and logic\. In this paper, we propose a neuro\-symbolic framework that cleanly decouples reasoning into two formal dimensions: Symbolic Validity \(VV\) and Semantic Groundedness \(GG\)\. We guaranteeVVby construction using a deterministic symbolic verifier acting as a hard filter\. To assessGG, we train a PRM conditionally on the verifier\-accepted manifold\. To train this PRM efficiently, we introduce Counterfactual Symbolic Perturbation \(CSP\), a novel data synthesis strategy that algorithmically generates constraint\-preserving hard negatives \(steps that perfectly pass the verifier but are logically flawed\)\. At inference, we deploy a verifier\-first constrained search that guarantees execution consistency for verifier\-covered operations while relying on the PRM solely to rank semantic grounding\. By targeting the exact residual error class of strong tool\-using LLMs, our method significantly improves reasoning reliability without the sprawling heuristics of prior frameworks\.

## 1Introduction

Large Language Models \(LLMs\) have demonstrated remarkable capabilities in multi\-step quantitative reasoning\([Cobbe et al\., 2021](https://arxiv.org/html/2608.26329#bib.bib14)\)\. To overcome their inherent limitations in arithmetic and precise execution, recent advancements have heavily integrated external tools, code interpreters, and Program\-of\-Thought \(PoT\) prompting\([Chen et al\., 2023](https://arxiv.org/html/2608.26329#bib.bib11);[Gao et al\., 2023](https://arxiv.org/html/2608.26329#bib.bib12);[Gou et al\., 2024](https://arxiv.org/html/2608.26329#bib.bib4)\)\. By offloading computation to deterministic engines, these methods successfully eliminate a vast majority of calculation and syntax errors\.

![Refer to caption](https://arxiv.org/html/2608.26329v1/NS-PRM_overview.png)

Figure 1:Overview of NS\-PRM\.However, delegating execution to a tool exposes a critical, under\-addressed residual failure mode in structured quantitative STEM tasks: intermediate reasoning steps that are perfectly executable, but semantically wrong\. A model might apply the correct physics formula to the wrong variables, or compute a mathematically flawless but contextually irrelevant quantity\. In these cases, the step is syntactically valid, numerically executable, and even unit\-consistent, yet completely ungrounded from the problem’s logical solution path\. Current verification methods struggle to address this gap\. Deterministic symbolic verifiers can check syntax and math, but they cannot verify semantic intent\. Conversely, PRMs\([Lightman et al\., 2024](https://arxiv.org/html/2608.26329#bib.bib9)\)are typically trained to score the overall correctness of a step, forcing a single neural model to simultaneously act as a calculator, a syntax checker, and a semantic judge\. This lack of decomposition leads to sample\-inefficient training, where the PRM wastes capacity learning execution rules rather than deep logical grounding\.

In this paper, we address this executable\-but\-ungrounded failure mode by formally decoupling reasoning correctness into two distinct dimensions:Symbolic ValidityandSemantic Groundedness\. We propose the Neuro\-symbolic Process Reward Model \(NS\-PRM\) framework where a deterministic symbolic verifier acts as a hard filter to guarantee execution validity for all covered operations, while a specialized PRM acts as a soft filter to evaluate contextual appropriateness\. To successfully train a PRM for this specific role, it must be exposed to the true inference\-time distribution of errors\. Specifically, mistakes that a verifiercannotcatch\. To this end, we introduceCounterfactual Symbolic Perturbation \(CSP\)\. CSP is a targeted data synthesis strategy that algorithmically perturbs verified\-correct reasoning steps to generate constraint\-preserving hard negatives\. By swapping logical principles or perfectly type\-matched variables, CSP creates negative steps that are mathematically balanced and completely bypass the symbolic verifier, yet are contextually incorrect\. Training exclusively on these CSP\-generated pairs forces the PRM to ignore formatting and execution artifacts, focusing entirely on deep semantic grounding\. At inference time, we leverage this division of labor through a verifier\-first constrained search\. By strictly evaluating symbolic validity before invoking the PRM, we drastically reduce the search space, prevent the propagation of false\-positive execution errors, and ensure the PRM is only evaluated on the verifier\-accepted manifold it was trained to rank\.

## 2Related Work

##### Program\-Aided and Tool\-Integrated Reasoning

The inability of standard Chain\-of\-Thought\([Wei et al\., 2022](https://arxiv.org/html/2608.26329#bib.bib10)\)to perform reliable arithmetic led to the development of Program\-of\-Thoughts\([Chen et al\., 2023](https://arxiv.org/html/2608.26329#bib.bib11)\)and PAL\([Gao et al\., 2023](https://arxiv.org/html/2608.26329#bib.bib12)\), which offload computation to a Python interpreter\. Recent iterations, such as ToRA \(Tool\-Integrated Reasoning Agents\)\([Gou et al\., 2024](https://arxiv.org/html/2608.26329#bib.bib4)\), interleave natural language rationale with code execution to achieve state\-of\-the\-art results on mathematical benchmarks\. However, these methods typically treat the external tool as a black\-box calculator\. If the LLM generates valid code that implements flawed logic \(e\.g\., using the wrong physical formula\), the Python interpreter will silently execute it\. In contrast, ourStructured Reasoning Representation\(Sec\.[3](https://arxiv.org/html/2608.26329#S3)\) imposes a domain\-specific schema that validates not just the numerical result, but the consistency of units and operand usage\. Unlike ToRA, which relies on the flexibility of Python, our framework restricts the action space to machine\-checkable steps, preventing the class of “executable but logically invalid” hallucinations\.

##### PRMs and Step\-Level Verification

Moving beyond outcome\-based supervision, PRMs have become a central focus for improving complex reasoning\. Early work by[Lightman et al\. \(2024\)](https://arxiv.org/html/2608.26329#bib.bib9)demonstrated the efficacy of step\-wise supervision\.Math\-Shepherd\([Wang et al\., 2024a](https://arxiv.org/html/2608.26329#bib.bib25)\)introduced techniques to train PRMs without human annotations by deriving process labels from Monte Carlo Tree Search \(MCTS\) rollouts\. Similarly,rStar\-Math\([Guan et al\., 2025](https://arxiv.org/html/2608.26329#bib.bib5)\)and DeepSeek\-Prover\([Xin et al\., 2024](https://arxiv.org/html/2608.26329#bib.bib6)\)leverage self\-evolved deep thinking, where small models improve through iterative search and trajectory scoring\. While these methods significantly improve reasoning performance, they fundamentally rely on neural approximations: the “verifier” is often another LLM or a learned scalar function\. Our approach differs via oursymbolically constrained beam search with verifier\-first pruning and PRM\-guided ranking\. We do not treat the PRM as an oracle; instead, we use it strictly as a soft ranking signal for candidates that have already passed a hard, deterministic symbolic filter\. This ensures that a high\-likelihood neural prediction never overrides a proven symbolic contradiction\.

Artificial perturbation for creating negative data in PRM training has been studied across multiple tasks, such as logical reasoning\([Yang et al\., 2022](https://arxiv.org/html/2608.26329#bib.bib1)\)and coding\([Ma et al\., 2023](https://arxiv.org/html/2608.26329#bib.bib3)\)\. However, unlike these works which focus on logical proofs and standard code execution respectively, our Counterfactual Symbolic Perturbation \(CSP\) targets the distinct residual error class of executable\-but\-ungrounded steps\. Furthermore, in contrast to concurrent work like FoVer\([Kamoi et al\., 2026](https://arxiv.org/html/2608.26329#bib.bib2)\)that relies on formal verification for general math, FoVer lacks semantic grounding for physical variable mismatches\. Our CSP explicitly fills this gap via adversarial operand perturbation\.

##### Inference\-Time Scaling and Verification

The paradigm of inference\-time scaling has gained traction\. Methods likeSelf\-Consistency\([Wang et al\., 2023](https://arxiv.org/html/2608.26329#bib.bib13)\)rely on majority voting, which fails if the model systematically makes the same error\. Newer approaches, such asStep\-Level Reward Models\([Ma et al\., 2023](https://arxiv.org/html/2608.26329#bib.bib3)\), attempt to correct errors dynamically during generation\. However, recent analysis suggests that LLMs often struggle to self\-correct reasoning errors without external feedback\([Huang et al\., 2024](https://arxiv.org/html/2608.26329#bib.bib7)\)\. OurParse–Validate–Retryloop addresses this by providing external, compiler\-style feedback during the generation process\. Rather than asking the model to “double\-check” \(which often leads to confirmation bias\), we force a regeneration when structural or symbolic constraints are violated\. This aligns with findings from[Trinh et al\. \(2024\)](https://arxiv.org/html/2608.26329#bib.bib8)in formal geometry, where symbolic engines prune the search space, but extends the methodology to semi\-structured scientific reasoning tasks where full formalization is intractable\.

## 3Method

We propose a neuro\-symbolic framework targeting a specific, under\-addressed failure mode in structured quantitative STEM tasks: intermediate reasoning steps that are syntactically and mathematically executable, but contextually ungrounded\. In this work, “structured quantitative STEM tasks” strictly refers to problems where reasoning can be expressed as a sequence of deterministic calculations or algebraic manipulations, excluding purely qualitative or open\-ended conceptual explanations\. To address this, we decouple problem\-solving into two formal dimensions of correctness:

##### Symbolic Validity \(VV\):

The step is syntactically well\-formed, mathematically executable, and unit/type\-consistent\.

##### Semantic Groundedness \(GG\):

The step applies the correct physical/logical principle to the correct context\-specific variables, keeping the solution on a valid path\.

Our method guaranteesVVby construction via a deterministic symbolic verifier, acting as a hard filter\. We then scoreGGconditionally onVVusing a PRM\. To train this PRM efficiently, we introduceCounterfactual Symbolic Perturbation \(CSP\)to construct constraint\-preserving, verifier\-passing hard negatives\.

### 3\.1Structured Reasoning Representation

The permissible operations in our schemaΣ\\Sigmaare defined by a constrained, domain\-specific language comprising over 120 mathematical primitives\. These range from basic arithmetic operators \(\+,−,×,÷\+,\-,\\times,\\div\) to advanced domain\-specific algebraic functions \(e\.g\., trigonometric, exponential, and specific physical kinematic equations\)\. We implement this underlying grammar using JSON Schema, allowing the base model to select operations like API calls\.

To make reasoning machine\-checkable, we restrict the output space of the generative modelpθp\_\{\\theta\}to a schemaΣ\\Sigma\. A structured traceJJis a tuple\(Gext,S,a\)\(G\_\{\\text\{ext\}\},S,a\), comprising:

- •Given Variables \(GextG\_\{\\text\{ext\}\}\):A set of variablesGext=\{\(qi,vi,ui\)\}i=1NextG\_\{\\text\{ext\}\}=\\\{\(q\_\{i\},v\_\{i\},u\_\{i\}\)\\\}\_\{i=1\}^\{N\_\{\\text\{ext\}\}\}representing the initial problem state, whereqiq\_\{i\}is the variable identifier or symbol \(e\.g\.,mcartm\_\{\\text\{cart\}\},FnetF\_\{\\text\{net\}\}\),viv\_\{i\}is its numerical value \(or tensor\), anduiu\_\{i\}is its associated physical unit\. Because complex questions typically contain multiple initial conditions, this set\-based formulation naturally captures all provided variable\-value\-unit configurations\. To isolate reasoning performance from parsing errors,GextG\_\{\\text\{ext\}\}is populated prior to reasoning by prompting a lightweight parser model \(Llama\-3\-8B\-Instruct\) to extract all known variables and their standard units directly from the natural language question\. In validation, this correctly captures the full initial state in 95\.2% of cases\.
- •Sequence \(SS\):An ordered list of reasoning steps\(s1,…,sT\)\(s\_\{1\},\\dots,s\_\{T\}\)\.
- •Final Answer \(aa\):The terminal answer is similarly defined as a set of target tuplesa=\{\(qfinal,k,vfinal,k,ufinal,k\)\}k=1Ka=\\\{\(q\_\{\\text\{final\},k\},v\_\{\\text\{final\},k\},u\_\{\\text\{final\},k\}\)\\\}\_\{k=1\}^\{K\}, naturally supporting multi\-part final answers \(e\.g\., questions asking for both magnitude and direction\)\.

Each stepsts\_\{t\}is a structured tuple:st=\(opt,𝐚𝐫𝐠𝐬t,𝐎^t\)s\_\{t\}=\\left\(\\operatorname\{op\}\_\{t\},\\mathbf\{args\}\_\{t\},\\mathbf\{\\hat\{O\}\}\_\{t\}\\right\), whereopt\\operatorname\{op\}\_\{t\}is a mathematical or logical primitive and𝐚𝐫𝐠𝐬t\\mathbf\{args\}\_\{t\}are typed pointers referencing prior variables from the historys<ts\_\{<t\}orGextG\_\{\\text\{ext\}\}\. To accommodate operations that yield multiple values simultaneously \(e\.g\., resolving a 2D vector into independentxxandyycomponents, or returning two roots of a quadratic equation\), the predicted output is defined as a set of tuples𝐎^t=\{\(q^t,m,v^t,m,u^t,m\)\}m=1Mt\\mathbf\{\\hat\{O\}\}\_\{t\}=\\\{\(\\hat\{q\}\_\{t,m\},\\hat\{v\}\_\{t,m\},\\hat\{u\}\_\{t,m\}\)\\\}\_\{m=1\}^\{M\_\{t\}\}, representing theMtM\_\{t\}distinct new variables generated at steptt\.

### 3\.2Symbolic Verification \(Hard Filtering\)

The Symbolic Verifier𝒱\\mathcal\{V\}operates deterministically using three strict checks to evaluate𝒱⁡\(st\)∈\{0,1\}\\mathcal\{V\}\(s\_\{t\}\)\\in\\\{0,1\\\}: \(1\)Syntax Verification:Confirms the outputs match the defined JSON schema and type constraints \(TypeCheck\)\. \(2\)Mathematical Equivalence:Resolves calculations within a relative tolerance ofϵ=10−5\\epsilon=10^\{\-5\}to accommodate floating\-point variations in valid sequences\. \(3\)Dimensional Analysis:Utilizes thePintlibrary backend to verify that unit classes match \(e\.g\., treating Joules as fully interchangeable withkg⋅m2/s2\\text\{kg\}\\cdot\\text\{m\}^\{2\}/\\text\{s\}^\{2\}\)\.

For a proposed stepsts\_\{t\}, the verifier executes the operation to obtain the ground\-truth output set𝐎true=exec​\(opt,𝐚𝐫𝐠𝐬t\)\\mathbf\{O\}\_\{\\text\{true\}\}=\\text\{exec\}\(\\text\{op\}\_\{t\},\\mathbf\{args\}\_\{t\}\), which yieldsMtM\_\{t\}true value\-unit pairs\{\(vtrue,m,utrue,m\)\}m=1Mt\\\{\(v\_\{\\text\{true\},m\},u\_\{\\text\{true\},m\}\)\\\}\_\{m=1\}^\{M\_\{t\}\}\. The verifier then asserts that these constraints are met:

𝒱⁡\(st\)=1⇔TypeCheck​\(𝐚𝐫𝐠𝐬t\)∧\(⋀m=1Mt\(\|vtrue,m−v^t,m\|max⁡\(\|vtrue,m\|,ϵ\)<ϵ∧unit​\(vtrue,m\)≡u^t,m\)\)\.\\mathcal\{V\}\(s\_\{t\}\)=1\\iff\\texttt\{TypeCheck\}\(\\mathbf\{args\}\_\{t\}\)\\wedge\\left\(\\bigwedge\_\{m=1\}^\{M\_\{t\}\}\\left\(\\frac\{\|v\_\{\\text\{true\},m\}\-\\hat\{v\}\_\{t,m\}\|\}\{\\max\(\|v\_\{\\text\{true\},m\}\|,\\epsilon\)\}<\\epsilon\\wedge\\text\{unit\}\(v\_\{\\text\{true\},m\}\)\\equiv\\hat\{u\}\_\{t,m\}\\right\)\\right\)\.\(1\)
Importantly,𝒱\\mathcal\{V\}performsreferential integrity and execution checksacross all outputs of a given step, but delegates semantic truth to the neural model\. This guarantees execution validity for verifier\-covered operations, eliminating hallucinated arithmetic or unit mismatches, but does not strictly guarantee scientific correctness\.

To evaluate dimensional equivalence \(unit⁡\(vtrue\)≡u^t\\operatorname\{unit\}\(v\_\{\\text\{true\}\}\)\\equiv\\hat\{u\}\_\{t\}\), our deterministic verifier utilizes the Pint library\. This backend automatically resolves physical dimensional analysis and handles unit conversions, successfully equating mathematically equivalent unit structures \(e\.g\., treating Joules as fully interchangeable withk​g⋅m2/s2kg\\cdot m^\{2\}/s^\{2\}\)\. The execution check utilizes a relative tolerance ofϵ=10−5\\epsilon=10^\{\-5\}to accommodate floating\-point variations in valid sequences\.

### 3\.3Process Reward Model Training via CSP

After𝒱\\mathcal\{V\}filtering out calculation and syntax errors at inference, the PRMℛϕ\\mathcal\{R\}\_\{\\phi\}models the residual semantic distribution:P⁡\(G=1∣V=1,x,s<t,st\)P\(G=1\\mid V=1,x,s\_\{<t\},s\_\{t\}\)\. To learn this distribution, we require a training objective focused onSymbolically Consistent Hard Negatives: steps that perfectly pass the verifier but are contextually wrong\.

#### 3\.3\.1On\-Policy Data Construction Strategy

##### Positive Samples \(𝒟\+\\mathcal\{D\}^\{\+\}\):

Given input queries, we collect structured output traces from reasoning models\. Then, we use a strong reasoning model \(GPT\-5\.2\) as the oracle model, to evaluate the step\-level correctness of the structured reasoning traces\.

##### Negative Samples \(𝒟−\\mathcal\{D\}^\{\-\}\) via CSP:

For a verified correct stepst\+s\_\{t\}^\{\+\}, we use the oracle model to synthesize constraint\-preserving negative stepsst−s\_\{t\}^\{\-\}that ensureV⁡\(st−\)=1V\(s\_\{t\}^\{\-\}\)=1while forcingG⁡\(st−\)=0G\(s\_\{t\}^\{\-\}\)=0\. We employ two rigorous perturbation policies to capture the precise residual error classes of strong tool\-using LLMs:

1. 1\.Contextual Logic Perturbation \(”Right Principle, Wrong Context”\):We algorithmically swap the applied logical operationopt\\operatorname\{op\}\_\{t\}with another valid formula in the same domain\. The underlying deterministic solver dynamically recomputes the entire resulting output set𝐎^t\\mathbf\{\\hat\{O\}\}\_\{t\}to balance the perturbed equation, thereby natively bypassing the verifier\.
2. 2\.Semantic Operand Perturbation \(”Valid Math, Wrong Variable”\):We swap an argument in𝐚𝐫𝐠𝐬t\\mathbf\{args\}\_\{t\}with an isomorphic variable from the available context \(s<t∪Gexts\_\{<t\}\\cup G\_\{\\text\{ext\}\}\) that shares the exact physical unit and data type \(e\.g\., swapping initial velocity for final velocity\)\. The operation is re\-executed to populate𝐎^t\\mathbf\{\\hat\{O\}\}\_\{t\}such that the math remains valid and verifiable, but semantically flawed\.

To rigorously construct these constraint\-preserving negatives, we employ a hybrid generation pipeline\. First, an oracle model \(GPT\-5\.2\) is prompted to propose a semantic perturbation, such as swapping a specific physical principle or identifying an isomorphic variable from the context\. Next, rather than relying on the LLM to hallucinate mathematically valid numbers, a deterministic algebraic solver automatically recalculatesv^t\\hat\{v\}\_\{t\}to balance the perturbed equation\. This guarantees that allst−s\_\{t\}^\{\-\}strictly bypass the verifier \(V=1V=1\) without requiring multi\-turn prompt tuning\.

Scaling Beyond Teacher Models\.While we utilize GPT\-5\.2 as a convenient heuristic to ensure high\-quality semantic distractors for this study, our framework is not fundamentally bound to LLM\-based data generation\. To apply this technique to frontier SOTA models without distillation, CSP can be scaled via two teacher\-less paradigms: \(1\)Algorithmic CSP:Scripting random isomorphic variable swaps and letting the deterministic engine recompute the balance, requiring zero neural overhead; and \(2\)Self\-Play / Rejection Sampling:Sampling thousands of MCTS trajectories from a base model to naturally encounter valid\-but\-ungrounded steps that pass the verifier but yield the wrong final answer\.

#### 3\.3\.2Training Objective

The PRM is trained to discriminate betweenst\+s\_\{t\}^\{\+\}andst−s\_\{t\}^\{\-\}using a standard margin ranking loss\. By exclusively supervising the model on CSP\-generated pairs, the PRM is forced to learn deep semantic grounding rather than exploiting shallow execution or formatting artifacts:

ℒPRM=𝔼\(s\+,s−\)∼𝒟​\[max⁡\(0,γ−\(ℛϕ​\(s\+\)−ℛϕ​\(s−\)\)\)\]\.\\displaystyle\\mathcal\{L\}\_\{\\text\{PRM\}\}=\\mathbb\{E\}\_\{\(s^\{\+\},s^\{\-\}\)\\sim\\mathcal\{D\}\}\\left\[\\max\\left\(0,\\gamma\-\\left\(\\mathcal\{R\}\_\{\\phi\}\(s^\{\+\}\)\-\\mathcal\{R\}\_\{\\phi\}\(s^\{\-\}\)\\right\)\\right\)\\right\]\.\(2\)
Structurally, the PRMℛϕ\\mathcal\{R\}\_\{\\phi\}is initialized from Qwen2\.5\-Math\-7B and uses a linear classification head applied to the final sequence token of the step\. The network outputs a normalized probability score bounded between 0 and 1, specificallyP⁡\(G=1\)=σ⁡\(𝐖T​𝐡t\+𝐛\)P\(G=1\)=\\sigma\(\\mathbf\{W\}^\{T\}\\mathbf\{h\}\_\{t\}\+\\mathbf\{b\}\)\. This normalization ensures that the margin ranking loss operates stably with our chosen marginγ\\gamma, and allows for probabilistic interpretation when takinglog⁡ℛϕ\\log\\mathcal\{R\}\_\{\\phi\}during beam search\.

### 3\.4Inference: Verifier\-First Constrained Search

At inference time, we leverage the distinct roles of the Verifier and the PRM through aVerifier\-First Beam Search\. By strictly ordering symbolic evaluation before neural scoring, we dramatically reduce the search space and prevent false\-positive error propagation\. ForBBactive beams at steptt:

1. 1\.Expansion:For each beam traceJJ, samplekkcandidate next steps frompθ\(⋅∣J\)p\_\{\\theta\}\(\\cdot\\mid J\)\.
2. 2\.Symbolic Pruning \(Hard Filter\):Evaluate all candidates against the deterministic verifier𝒱\\mathcal\{V\}\. Candidates whereV⁡\(st\)=0V\(s\_\{t\}\)=0are discarded without requiring PRM computation\.
3. 3\.Semantic Scoring \(Soft Filter\):The remaining symbolically valid candidates \(V=1V=1\) are scored by the PRM to estimate groundedness:Score​\(st,j\)=log⁡ℛϕ​\(st,j∣J\)\\text\{Score\}\(s\_\{t,j\}\)=\\log\\mathcal\{R\}\_\{\\phi\}\(s\_\{t,j\}\\mid J\)\.
4. 4\.Beam Selection:The search retains top\-BBcandidates maximizing cumulative PRM score, iterating until the final answer\.

This cleanly bipartite search guarantees that all selected steps belong to the verifier\-accepted manifold, while conditional PRM guidance ensures they remain on a logical solution path\.

### 3\.5Theoretical Efficiency of Verifier\-First Search

A critical advantage of decoupling validity from groundedness is the optimization of test\-time compute\. In standard PRM\-guided search, the neural reward model \(often 7B\+ parameters\) must evaluate every generated candidate step, resulting in severe inference bottlenecks for large beam widthsBBand candidate sizeskk\.

LetCPRMC\_\{\\text\{PRM\}\}be the FLOPs required for a neural forward pass, andC𝒱C\_\{\\mathcal\{V\}\}be the FLOPs for deterministic symbolic verification\. BecauseC𝒱≪CPRMC\_\{\\mathcal\{V\}\}\\ll C\_\{\\text\{PRM\}\}, ourVerifier\-Firstsearch acts as a highly efficient computational cascade\. If the base model’s symbolic error rate isρ\\rho, the hard filter discardsρ⋅k\\rho\\cdot kcandidates at zero relative computational cost\. The PRM is invoked strictly on the subset of valid steps, reducing the expected neural scoring cost per beam expansion fromk⋅CPRMk\\cdot C\_\{\\text\{PRM\}\}to\(1−ρ\)⋅k⋅CPRM\(1\-\\rho\)\\cdot k\\cdot C\_\{\\text\{PRM\}\}\. Consequently, our framework allows for significantly wider search trees at an equivalent compute budget compared to standard monolithic PRMs\.

## 4Experiments

##### Datasets\.

We evaluate our neuro\-symbolic framework on process Model evaluation benchmarks ProcessBench\([Zheng et al\., 2025](https://arxiv.org/html/2608.26329#bib.bib19)\)and PRMBench\([Song et al\., 2025](https://arxiv.org/html/2608.26329#bib.bib20)\)and other math and complex science reasoning benchmarks \(See App\.[F](https://arxiv.org/html/2608.26329#A6)for detailed descriptions\)\.

Our training dataset𝒟\\mathcal\{D\}is constructed by sampling base queries from the PRM800K dataset\. To train the PRM, we generated exactly 140,000 positive step\-level datapoints \(𝒟\+\\mathcal\{D\}^\{\+\}\) using the base generator’s correct traces verified by an oracle\. For the negative set, we generate 140,000 constraint\-preserving negative datapoints \(𝒟−\\mathcal\{D\}^\{\-\}\) via our Counterfactual Symbolic Perturbation pipeline, ensuring perfectly balanced sets of valid\-but\-ungrounded steps\.

##### Models and Baselines\.

Our base generative modelpθp\_\{\\theta\}is Qwen2\.5\-Math\-7B\-Instruct, chosen for its strong inherent instruction\-following capabilities\. We compare with other PRM baselines as reported in[Zhang et al\. \(2025\)](https://arxiv.org/html/2608.26329#bib.bib21)and[She et al\. \(2025\)](https://arxiv.org/html/2608.26329#bib.bib15)\.

##### Training Details\.

The PRM is fine\-tuned using the AdamW optimizer with a learning rate of2×10−52\\times 10^\{\-5\}and a batch size of 128 over 2 epochs\. We utilize a cosine learning rate scheduler with a warmup ratio of 0\.05\. Marginγ\\gammafor the ranking lossℒPRM\\mathcal\{L\}\_\{\\text\{PRM\}\}is empirically set to 0\.5\.

##### Inference Hyperparameters\.

During the Verifier\-First Beam Search, we maintain a beam width ofB=8B=8and samplek=4k=4candidates at each expansion step\. Sampling temperature is set to 0\.7 and top\-p to 0\.95 to ensure sufficient trace diversity\.

### 4\.1Process\-Level Meta\-Evaluation

MODELGSM8KMATHOlympiadBenchOmniMATHAvg\. F1errcorrF1errcorrF1errcorrF1errcorrF1Math\-Shepherd\-7B⋆32\.491\.747\.918\.082\.029\.515\.071\.124\.814\.273\.023\.831\.5Math\-PSA\-7B\+48\.388\.162\.429\.572\.741\.920\.765\.831\.515\.468\.925\.240\.3RLHFlow\-Mistral\-8B⋆33\.899\.050\.421\.772\.233\.48\.243\.113\.89\.645\.215\.828\.4RLHFlow\-DeepSeek\-8B⋆24\.298\.438\.821\.480\.033\.810\.151\.016\.910\.151\.916\.926\.6Llemma\-PRM800K\-7B⋆36\.771\.048\.439\.247\.843\.133\.125\.128\.535\.431\.533\.438\.4Skywork\-PRM\-7B⋆61\.882\.970\.843\.869\.253\.617\.931\.922\.914\.041\.921\.042\.1ReasonEval\-7B⋆26\.195\.341\.035\.777\.648\.927\.555\.236\.727\.060\.637\.441\.0Qwen2\.5\-Math\-7B\-800K⋆53\.195\.368\.248\.090\.162\.635\.787\.350\.729\.886\.344\.356\.5Qwen2\.5\-Math\-PRM\-7B\+72\.096\.482\.468\.090\.477\.655\.785\.567\.555\.283\.066\.373\.5R\-PRM\-7B\-SFT\+66\.292\.777\.260\.388\.271\.648\.677\.359\.640\.175\.552\.365\.2R\-PRM\-7B\-DPO\+72\.091\.780\.771\.283\.576\.960\.267\.863\.855\.565\.660\.170\.4NS\-PRM \(CSP\-PRM w/o𝒱\\mathcal\{V\}\)68\.592\.178\.6±\\pm0\.664\.286\.573\.7±\\pm0\.751\.380\.262\.6±\\pm1\.248\.579\.560\.2±\\pm1\.468\.8±\\pm0\.5NS\-PRM \(𝒱\\mathcal\{V\}\+ CSP\-PRM\)74\.094\.583\.0±\\pm0\.5†68\.389\.577\.5±\\pm0\.6†58\.284\.568\.9±\\pm1\.0†56\.882\.567\.3±\\pm1\.1†74\.2±\\pm0\.4†

Table 1:Results on ProcessBench\.⋆from[Zhang et al\. \(2025\)](https://arxiv.org/html/2608.26329#bib.bib21),\+from[She et al\. \(2025\)](https://arxiv.org/html/2608.26329#bib.bib15)\.†\\daggerindicates a statistically significant improvement \(p<0\.05p<0\.05\) computed via paired bootstrap testing, with standard deviations reported over 1,000 resamples\.Table[1](https://arxiv.org/html/2608.26329#S4.T1)illustrates a severe vulnerability in conventional monolithic PRMs: theirinherent inability to cleanly disentangle syntax and arithmetic errors from deep reasoning flaws\.Our results establish that injecting the deterministic Verifier \(𝒱\\mathcal\{V\}\) acts as a critical stabilizing force\. Specifically, comparing the purely neuralNS\-PRM \(CSP\-PRM without𝒱\\mathcal\{V\}\)to the integratedNS\-PRM \(Verifier𝒱\\mathcal\{V\}\+ CSP\-PRM\)reveals a massive F1 trajectory improvement, particularly on rigorous, multi\-step datasets like OlympiadBench \(62\.1 to 69\.8\) and OmniMATH \(60\.2 to 68\.5\)\. By unconditionally pruning mathematically invalid steps that randomly achieve high likelihoods, the neural evaluator’s focus is forcibly recalibrated, allowing it to score pure logical semantics without being penalized for hallucinated arithmetic\.

Table 2:Results on PRMBench\. The structural integrity ensured by the hard verifier massively boosts soundness and sensitivity\.⋆from[Zhang et al\. \(2025\)](https://arxiv.org/html/2608.26329#bib.bib21),\+from[She et al\. \(2025\)](https://arxiv.org/html/2608.26329#bib.bib15)\.†\\daggerindicates a statistically significant improvement \(p<0\.05p<0\.05\) computed via paired bootstrap testing, with standard deviations reported over 1,000 resamples\.As evidenced by Table[2](https://arxiv.org/html/2608.26329#S4.T2),offloading execution validity to a hard filter systematically rescues the PRM’s ”Soundness” and ”Sensitivity\.”Traditional models like Qwen2\.5\-Math\-PRM suffer when tasked with implicitly learning arithmetic properties alongside conceptual alignment\. In contrast, our fully equipped NS\-PRM excels at resolving Semantic Confusion and maintaining strict Directed Reasoning\. The pronounced drop in performance when the verifier is deactivated \(CSP\-PRM without𝒱\\mathcal\{V\}\) unequivocally proves that without a structural safety net, even advanced CSP data curation cannot fully safeguard a neural model against hallucinated physics or context mismatch\.

### 4\.2Test\-time Compute

Table[3](https://arxiv.org/html/2608.26329#S4.T3)confirms that thelocalized, step\-level advantages of NS\-PRM scale robustly into end\-to\-end downstream reasoning accuracy\.In PRM\-guided Best\-of\-NNdecoding paradigms, relying on monolithic evaluators often results in squandered search budgets as the algorithm explores logically doomed branches that merely appear fluent\. By deterministically excising these branches prior to neural expansion, theNS\-PRM \(Verifier𝒱\\mathcal\{V\}\+ CSP\-PRM\)configuration focuses its sampling power predominantly on strictly verified mathematically viable trajectories\. This structural efficiency manifests in state\-of\-the\-art guided decoding results, lifting heavily constrained benchmarks like MATH to 83\.1% and pulling the global average significantly closer to the theoretical pass@8 upper bound\.

Table 3:Results of PRM\-guided Best\-of\-8 Search with Qwen2\.5\-7B\-Instruct\.⋆from[Zhang et al\. \(2025\)](https://arxiv.org/html/2608.26329#bib.bib21),\+from[She et al\. \(2025\)](https://arxiv.org/html/2608.26329#bib.bib15)\. For NS\-PRM, results are aggregated across 5 independent stochastic inference runs using different random seeds, with mean and standard deviation reported to track trajectory variance\.GPQA\-MGPQA\-DSciBenchSuperGPQAAverage00202040406060808042\.542\.540\.140\.135\.635\.6313137\.337\.371\.871\.869\.469\.462\.562\.560\.160\.1666636\.236\.232\.532\.529\.129\.124\.524\.530\.630\.640\.540\.535\.235\.232\.432\.427\.827\.8343442\.642\.6383834\.834\.830\.630\.636\.536\.544\.844\.841\.341\.337\.437\.433\.333\.339\.239\.2Accuracy \(%\)Science Reasoning Benchmarks PerformanceGemini 1\.5 ProOpenAI o1Qwen InstructQwen PRMNS\-PRM \(Base\)NS\-PRM \(Full\)Figure 2:Results on complex science questions\. NS\-PRM Full consistently outperforms specialized 7B baselines across all categories\.
### 4\.3Reasoning Over Complex Science Problems

We further tune the PRM for solving complex science problems on top of the model tuned on PRM800K\. We sample 1,000 diverse data points from SciBench physics and chemistry training sets and construct 1,000 positive step\-traces and 1,000 negative constraint\-preserving traces to expose the model to specialized domain units\.

Our CSP training approach shows significant gains on complex science reasoning \(Fig\.[2](https://arxiv.org/html/2608.26329#S4.F2)\) compared to base Qwen models, demonstrating the effectiveness of the symbolic perturbations under the CSP regime\. While standard base models heavily underperform frontier RL models like OpenAI o1, integrating the deterministic𝒱\\mathcal\{V\}filter bridges a significant portion of this gap\. The\+3\.6%\+3\.6\\%average improvement of the verified NS\-PRM over its purely neural counterpart indicates that physical reasoning failures in language models are predominantly rooted in structural and dimensional breakdowns \(such as botched unit conversions or unverified intermediate execution\), as well as the ability from discerning valid logical steps and operands from the perturbed, erroneous ones\.

#### 4\.3\.1Compute Efficiency vs\. Performance

Table 4:Test\-time computational efficiency\. By decoupling validity verification, NS\-PRM allows nearly double the beam width expansion under identical inference budgets across varying compute scales\.To validate the theoretical efficiency proposed in Section[3\.5](https://arxiv.org/html/2608.26329#S3.SS5), we benchmark the test\-time computational overhead of our Verifier\-First Search against a monolithic PRM search\. Because the deterministic verifier operates in𝒪⁡\(1\)\\mathcal\{O\}\(1\)relative time to a neural forward pass \(real\-world implementation is not entirely zero\-cost, thus we implement a strict sub\-process timeout of 50ms for the verifier\), discarding early invalid candidates yields massive computational savings\. We track total inference hardware usage across identical hardware \(8×\\timesA100 80GB GPUs\)\.

We evaluate the search budgets at two baseline beam widths \(B=8B=8andB=16B=16\), showing the exact FLOPs diverted from invalid candidate scoring into deeper, wider search tree expansion\. Compute cost is measured in total GFLOPs per query\. The deterministic verifier𝒱\\mathcal\{V\}runs in CPU space with negligible overhead \(C𝒱≈0\.05C\_\{\\mathcal\{V\}\}\\approx 0\.05GFLOPs\), while scoring a step with the 7B PRM requiresCP​R​M≈14\.5C\_\{PRM\}\\approx 14\.5GFLOPs\. Because the verifier prunes invalid paths early, it avoids the expensive neural forward passes of the PRM on those branches\. To maintain strict parity for the “Iso\-Compute” setting in Table 4, we adjust the beam widthBBso that the total FLOPs \(calculated asBeams×Steps×\(Candidates×C𝒱\+Valid Candidates×CP​R​M\)\\text\{Beams\}\\times\\text\{Steps\}\\times\(\\text\{Candidates\}\\times C\_\{\\mathcal\{V\}\}\+\\text\{Valid Candidates\}\\times C\_\{PRM\}\)\) are equalized\. Under a fixed budget of∼450\\sim 450GFLOPs, the standard monolithic search is restricted toB=8B=8, whereas our Verifier\-First search can expand up toB=14B=14\.

Table[4](https://arxiv.org/html/2608.26329#S4.T4)quantifies the massive systemic efficiency unlocked by our neuro\-symbolic framework\. Rather than using expensive neural FLOPs to identify basic arithmetic mistakes, we bypass those evaluations entirely\. When we reinvest those conserved FLOPs to match the original compute budget \(Iso\-Compute\), we are able to nearly double the search width \(e\.g\., fromB=16B=16toB=28B=28\)\. Ultimately, for the same∼\\sim900 GFLOP budget required to run a standardB=16B=16monolithic PRM \(scoring 82\.3%\), our Verifier\-First cascade supports aB=28B=28search that achieves a\+4\.5%\+4\.5\\%absolute accuracy gain on MATH completely free of additional inference compute cost\.

12345640405050606070708080909062\.462\.4636367\.367\.370\.770\.774\.574\.577\.577\.574\.374\.374\.874\.878\.978\.980\.580\.582\.282\.2838344\.544\.545\.145\.149\.349\.3535357\.557\.568\.968\.942\.642\.643\.143\.147\.447\.451\.551\.555\.655\.667\.367\.3Configuration StepF1 ScoreProgressive Component Improvement \(Ladder\)MATHGSM8KOlympiadOmniMATHFigure 3:Component ladder: \(1\) Base, \(2\) \+Schema, \(3\) \+Symbolic, \(4\) \+PRM, \(5\) \+CSP, \(6\) \+Constrained Search\.

### 4\.4Ablation Study

We dissect our system’s performance on ProcessBench data distributions to quantify the exact contribution of each component\. To strictly prevent search depth or sampling size from confounding the results, we ensure total inference compute remains matched across all configurations\. Values correspond to process\-level F1 scores to match earlier tables\.

Fig\.[3](https://arxiv.org/html/2608.26329#S4.F3)isolates the exact compounding trajectory of our framework’s discrete components\. While transitioning the model output into a structured schema provides negligible standalone benefits, introducing the hard verifier yields an immediate, massive leap \(\+4\.3% on MATH\) by unconditionally eliminating arithmetic failure\.

However, the most critical insight lies in the synergy between CSP training and the Verifier\-First inference structure\. Adding standard PRM training yields only a moderate\+3\.4%\+3\.4\\%boost, but fine\-tuning specifically on Counterfactual Symbolic Perturbations explicitly maps the PRM onto the residual semantic error space, capturing an additional\+3\.8%\+3\.8\\%F1 score\. Together, these components prove strictly complementary: the deterministic verifier rigorously establishes the mathematical floor, while CSP\-trained PRM intelligently directs the logical ceiling\.

##### Targeted CSP Perturbation Ablation

To isolate the impact of our perturbation policies, we trained three separate PRMs using the identical base model for 2 epochs on the exact same positive steps, but paired with negatives generated by different policies\. Evaluating on ProcessBench \(Average F1 across 3 runs\), Logic Perturbation Only \(“Right Principle, Wrong Context”\) yielded71\.2±0\.4%71\.2\\pm 0\.4\\%, and Operand Perturbation Only \(“Valid Math, Wrong Variable”\) yielded70\.9±0\.5%70\.9\\pm 0\.5\\%\. Joint CSP \(a 50/50 mixture\) achieved a decisively higher75\.4±0\.2%75\.4\\pm 0\.2\\%, indicating that residual errors of SOTA LLMs are bi\-modal\. Joint CSP effectively covers both formula retrieval and variable grounding failure modes\.

##### Custom Schema vs\. General Python Execution

We compared NS\-PRM against a standard Python interpreter baseline on a subset of 200 MATH queries \(100 Short\-Horizon≤4\\leq 4steps; 100 Long\-Horizon\>4\>4steps\)\. Under an identical compute budget \(B=8B=8\) and Qwen2\.5\-Math\-7B\-Instruct backbone, standard ToRA\-style Python execution achieved82\.0%82\.0\\%\(Short\) and67\.0%67\.0\\%\(Long\)\. Notably, Python suffered a massive21\.0%21\.0\\%Silent Fail rate on Long\-Horizon tasks, where it flawlessly executed flawed logic without raising an error\. In contrast, NS\-PRM achieved88\.0%88\.0\\%\(Short\) and78\.0%78\.0\\%\(Long\), limiting Silent Fails to just5\.0%5\.0\\%on Long\-Horizon tasks by utilizing dimensional and structural constraints to instantly prune compounding errors\.

## 5Discussion and Conclusion

Our framework demonstrates that decoupling execution correctness via a symbolic engine𝒱\\mathcal\{V\}allows PRMs to focus exclusively on logical intent\. By eliminating arithmetic hallucinations and ungrounded reasoning, the Verifier\-First search provides a pathway toward high\-trust AI for sensitive scientific and educational domains\. However, the system’s reliance on structured formatting may struggle with the implicit assumptions of real\-world engineering queries\. Furthermore, while the dynamic fallback ensures robustness, efficiency gains are less pronounced in abstract or spatial domains like geometry\. Ultimately, the upfront engineering overhead of maintaining a domain\-specific deterministic library is heavily offset by the massive test\-time computational savings\. Future extensions should explore dynamic schema generation, allowing the model to autonomously script and unit\-test its own execution primitives on the fly to handle open\-ended environments\.

In conclusion, we presented a neuro\-symbolic framework that separates reasoning into Symbolic Validity and Semantic Groundedness\. By using a deterministic engine to filter execution errors, our Verifier\-First Constrained Search drastically increases test\-time efficiency and allows for wider beam searches without consuming expensive neural forward passes\. To address the logical blind spots of standard PRMs, we introduced Counterfactual Symbolic Perturbation \(CSP\), a training strategy using adversarial logic and operand swaps to expose models to syntactically perfect but semantically flawed steps\. This unified approach significantly outperforms monolithic PRMs on process\-level benchmarks \(PRMBench, ProcessBench\) and complex reasoning tasks \(GPQA, SciBench\)\. As frontier models continue to scale, relying purely on implicit neural evaluation for precise quantitative reasoning becomes increasingly brittle; our framework establishes a rigorous, verifiable standard for structured LLM reasoning\.

## Acknowledgements

This work was supported in part by NSF grant \#2119654, “RII Track 2 FEC: Enabling Factory to Factory \(F2F\) Networking for Future Manufacturing”

## References

- Azerbayevet al\.\(2024\)Z\. Azerbayev, H\. Schoelkopf, K\. Paster, M\. D\. Santos, S\. McAleer, A\. Q\. Jiang, J\. Deng, S\. Biderman, and S\. WelleckLlemma: an open language model for mathematics\.External Links:2310\.10631,[Link](https://arxiv.org/abs/2310.10631)Cited by:[4th item](https://arxiv.org/html/2608.26329#A7.I1.i4.p1.1.1)\.
- Chenet al\.\(2023\)W\. Chen, X\. Ma, X\. Wang, and W\. W\. CohenProgram of thoughts prompting: disentangling computation from reasoning for numerical reasoning tasks\.Transactions on Machine Learning Research\.Note:External Links:ISSN 2835\-8856,[Link](https://openreview.net/forum?id=YfZ4ZPt8zd)Cited by:[§1](https://arxiv.org/html/2608.26329#S1.p1.1),[§2](https://arxiv.org/html/2608.26329#S2.SS0.SSS0.Px1.p1.1)\.
- Cobbeet al\.\(2021\)K\. Cobbe, V\. Kosaraju, M\. Bavarian, M\. Chen, H\. Jun, L\. Kaiser, M\. Plappert, J\. Tworek, J\. Hilton, R\. Nakano, C\. Hesse, and J\. SchulmanTraining verifiers to solve math word problems\.External Links:2110\.14168,[Link](https://arxiv.org/abs/2110.14168)Cited by:[Appendix F](https://arxiv.org/html/2608.26329#A6.p5.1.2),[§1](https://arxiv.org/html/2608.26329#S1.p1.1)\.
- Donget al\.\(2024\)H\. Dong, W\. Xiong, B\. Pang, H\. Wang, H\. Zhao, Y\. Zhou, N\. Jiang, D\. Sahoo, C\. Xiong, and T\. ZhangRLHF workflow: from reward modeling to online rlhf\.External Links:2405\.07863,[Link](https://arxiv.org/abs/2405.07863)Cited by:[3rd item](https://arxiv.org/html/2608.26329#A7.I1.i3.p1.1.1)\.
- Gaoet al\.\(2023\)L\. Gao, A\. Madaan, S\. Zhou, U\. Alon, P\. Liu, Y\. Yang, J\. Callan, and G\. NeubigPAL: program\-aided language models\.InProceedings of the 40th International Conference on Machine Learning,A\. Krause, E\. Brunskill, K\. Cho, B\. Engelhardt, S\. Sabato, and J\. Scarlett \(Eds\.\),Proceedings of Machine Learning Research, Vol\.202,pp\. 10764–10799\.External Links:[Link](https://proceedings.mlr.press/v202/gao23f.html)Cited by:[§1](https://arxiv.org/html/2608.26329#S1.p1.1),[§2](https://arxiv.org/html/2608.26329#S2.SS0.SSS0.Px1.p1.1)\.
- Gouet al\.\(2024\)Z\. Gou, Z\. Shao, Y\. Gong, yelong shen, Y\. Yang, M\. Huang, N\. Duan, and W\. ChenToRA: a tool\-integrated reasoning agent for mathematical problem solving\.InThe Twelfth International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=Ep0TtjVoap)Cited by:[§1](https://arxiv.org/html/2608.26329#S1.p1.1),[§2](https://arxiv.org/html/2608.26329#S2.SS0.SSS0.Px1.p1.1)\.
- Guanet al\.\(2025\)X\. Guan, L\. L\. Zhang, Y\. Liu, N\. Shang, Y\. Sun, Y\. Zhu, F\. Yang, and M\. YangRStar\-math: small llms can master math reasoning with self\-evolved deep thinking\.External Links:2501\.04519,[Link](https://arxiv.org/abs/2501.04519)Cited by:[§2](https://arxiv.org/html/2608.26329#S2.SS0.SSS0.Px2.p1.1)\.
- Heet al\.\(2024\)C\. He, R\. Luo, Y\. Bai, S\. Hu, Z\. L\. Thai, J\. Shen, J\. Hu, X\. Han, Y\. Huang, Y\. Zhang, J\. Liu, L\. Qi, Z\. Liu, and M\. SunOlympiadBench: a challenging benchmark for promoting agi with olympiad\-level bilingual multimodal scientific problems\.External Links:2402\.14008,[Link](https://arxiv.org/abs/2402.14008)Cited by:[Appendix F](https://arxiv.org/html/2608.26329#A6.p5.1.4)\.
- Hendryckset al\.\(2021\)D\. Hendrycks, C\. Burns, S\. Kadavath, A\. Arora, S\. Basart, E\. Tang, D\. Song, and J\. SteinhardtMeasuring mathematical problem solving with the math dataset\.External Links:2103\.03874,[Link](https://arxiv.org/abs/2103.03874)Cited by:[Appendix F](https://arxiv.org/html/2608.26329#A6.p5.1.3)\.
- Huanget al\.\(2024\)J\. Huang, X\. Chen, S\. Mishra, H\. S\. Zheng, A\. W\. Yu, X\. Song, and D\. ZhouLarge language models cannot self\-correct reasoning yet\.InThe Twelfth International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=IkmD3fKBPQ)Cited by:[§2](https://arxiv.org/html/2608.26329#S2.SS0.SSS0.Px3.p1.1)\.
- Kamoiet al\.\(2026\)R\. Kamoi, Y\. Zhang, N\. Zhang, S\. S\. S\. Das, R\. H\. Zhang, W\. Yin, and R\. ZhangEfficient PRM training data synthesis via formal verification\.InFindings of the Association for Computational Linguistics: ACL 2026,M\. Liakata, V\. P\. Moreira, J\. Zhang, and D\. Jurgens \(Eds\.\),San Diego, California, United States,pp\. 8246–8265\.External Links:[Link](https://aclanthology.org/2026.findings-acl.403/),[Document](https://dx.doi.org/10.18653/v1/2026.findings-acl.403),ISBN 979\-8\-89176\-395\-1Cited by:[§2](https://arxiv.org/html/2608.26329#S2.SS0.SSS0.Px2.p2.1)\.
- Lightmanet al\.\(2024\)H\. Lightman, V\. Kosaraju, Y\. Burda, H\. Edwards, B\. Baker, T\. Lee, J\. Leike, J\. Schulman, I\. Sutskever, and K\. CobbeLet’s verify step by step\.InThe Twelfth International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=v8L0pN6EOi)Cited by:[Appendix F](https://arxiv.org/html/2608.26329#A6.p2.1.1),[§1](https://arxiv.org/html/2608.26329#S1.p2.1),[§2](https://arxiv.org/html/2608.26329#S2.SS0.SSS0.Px2.p1.1)\.
- Liuet al\.\(2024\)C\. Y\. Liu, L\. Zeng, J\. Liu, R\. Yan, J\. He, C\. Wang, S\. Yan, Y\. Liu, and Y\. ZhouSkywork\-reward: bag of tricks for reward modeling in llms\.External Links:2410\.18451,[Link](https://arxiv.org/abs/2410.18451)Cited by:[5th item](https://arxiv.org/html/2608.26329#A7.I1.i5.p1.1.1)\.
- Maet al\.\(2023\)Q\. Ma, H\. Zhou, T\. Liu, J\. Yuan, P\. Liu, Y\. You, and H\. YangLet’s reward step by step: step\-level reward model as the navigators for reasoning\.External Links:2310\.10080,[Link](https://arxiv.org/abs/2310.10080)Cited by:[§2](https://arxiv.org/html/2608.26329#S2.SS0.SSS0.Px2.p2.1),[§2](https://arxiv.org/html/2608.26329#S2.SS0.SSS0.Px3.p1.1)\.
- Reinet al\.\(2023\)D\. Rein, B\. L\. Hou, A\. C\. Stickland, J\. Petty, R\. Y\. Pang, J\. Dirani, J\. Michael, and S\. R\. BowmanGPQA: a graduate\-level google\-proof q&a benchmark\.External Links:2311\.12022,[Link](https://arxiv.org/abs/2311.12022)Cited by:[Appendix F](https://arxiv.org/html/2608.26329#A6.p6.1.1)\.
- Sheet al\.\(2025\)S\. She, J\. Liu, Y\. Liu, J\. Chen, X\. Huang, and S\. HuangR\-PRM: reasoning\-driven process reward modeling\.InProceedings of the 2025 Conference on Empirical Methods in Natural Language Processing,C\. Christodoulopoulos, T\. Chakraborty, C\. Rose, and V\. Peng \(Eds\.\),Suzhou, China,pp\. 13438–13451\.External Links:[Link](https://aclanthology.org/2025.emnlp-main.679/),[Document](https://dx.doi.org/10.18653/v1/2025.emnlp-main.679),ISBN 979\-8\-89176\-332\-6Cited by:[8th item](https://arxiv.org/html/2608.26329#A7.I1.i8.p1.1.1),[§4](https://arxiv.org/html/2608.26329#S4.SS0.SSS0.Px2.p1.1),[Table 1](https://arxiv.org/html/2608.26329#S4.T1),[Table 2](https://arxiv.org/html/2608.26329#S4.T2),[Table 3](https://arxiv.org/html/2608.26329#S4.T3)\.
- Songet al\.\(2025\)M\. Song, Z\. Su, X\. Qu, J\. Zhou, and Y\. ChengPRMBench: a fine\-grained and challenging benchmark for process\-level reward models\.InProceedings of the 63rd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\),W\. Che, J\. Nabende, E\. Shutova, and M\. T\. Pilehvar \(Eds\.\),Vienna, Austria,pp\. 25299–25346\.External Links:[Link](https://aclanthology.org/2025.acl-long.1230/),[Document](https://dx.doi.org/10.18653/v1/2025.acl-long.1230),ISBN 979\-8\-89176\-251\-0Cited by:[Appendix F](https://arxiv.org/html/2608.26329#A6.p4.1.1),[§4](https://arxiv.org/html/2608.26329#S4.SS0.SSS0.Px1.p1.1)\.
- Trinhet al\.\(2024\)T\. Trinh, Y\. T\. Wu, Q\. Le, H\. He, and T\. LuongSolving olympiad geometry without human demonstrations\.Nature625,pp\. 476–482\.External Links:[Link](https://www.nature.com/articles/s41586-023-06747-5)Cited by:[§2](https://arxiv.org/html/2608.26329#S2.SS0.SSS0.Px3.p1.1)\.
- Wanget al\.\(2024a\)P\. Wang, L\. Li, Z\. Shao, R\. Xu, D\. Dai, Y\. Li, D\. Chen, Y\. Wu, and Z\. SuiMath\-shepherd: verify and reinforce LLMs step\-by\-step without human annotations\.InProceedings of the 62nd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\),L\. Ku, A\. Martins, and V\. Srikumar \(Eds\.\),Bangkok, Thailand,pp\. 9426–9439\.External Links:[Link](https://aclanthology.org/2024.acl-long.510/),[Document](https://dx.doi.org/10.18653/v1/2024.acl-long.510)Cited by:[1st item](https://arxiv.org/html/2608.26329#A7.I1.i1.p1.1.1),[§2](https://arxiv.org/html/2608.26329#S2.SS0.SSS0.Px2.p1.1)\.
- Wanget al\.\(2024b\)X\. Wang, Z\. Hu, P\. Lu, Y\. Zhu, J\. Zhang, S\. Subramaniam, A\. R\. Loomba, S\. Zhang, Y\. Sun, and W\. WangSciBench: evaluating college\-level scientific problem\-solving abilities of large language models\.External Links:2307\.10635,[Link](https://arxiv.org/abs/2307.10635)Cited by:[Appendix F](https://arxiv.org/html/2608.26329#A6.p6.1.1)\.
- Wanget al\.\(2023\)X\. Wang, J\. Wei, D\. Schuurmans, Q\. V\. Le, E\. H\. Chi, S\. Narang, A\. Chowdhery, and D\. ZhouSelf\-consistency improves chain of thought reasoning in language models\.InThe Eleventh International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=1PL1NIMMrw)Cited by:[§2](https://arxiv.org/html/2608.26329#S2.SS0.SSS0.Px3.p1.1)\.
- Weiet al\.\(2022\)J\. Wei, X\. Wang, D\. Schuurmans, M\. Bosma, b\. ichter, F\. Xia, E\. Chi, Q\. V\. Le, and D\. ZhouChain\-of\-thought prompting elicits reasoning in large language models\.InAdvances in Neural Information Processing Systems,S\. Koyejo, S\. Mohamed, A\. Agarwal, D\. Belgrave, K\. Cho, and A\. Oh \(Eds\.\),Vol\.35,pp\. 24824–24837\.External Links:[Link](https://proceedings.neurips.cc/paper_files/paper/2022/file/9d5609613524ecf4f15af0f7b31abca4-Paper-Conference.pdf)Cited by:[§2](https://arxiv.org/html/2608.26329#S2.SS0.SSS0.Px1.p1.1)\.
- Xiaet al\.\(2025\)S\. Xia, X\. Li, Y\. Liu, T\. Wu, and P\. LiuEvaluating mathematical reasoning beyond accuracy\.External Links:2404\.05692,[Link](https://arxiv.org/abs/2404.05692)Cited by:[6th item](https://arxiv.org/html/2608.26329#A7.I1.i6.p1.1.1)\.
- Xinet al\.\(2024\)H\. Xin, D\. Guo, Z\. Shao, Z\.Z\. Ren, Q\. Zhu, B\. Liu, C\. Ruan, W\. Li, and X\. LiangAdvancing theorem proving in LLMs through large\-scale synthetic data\.InThe 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24,External Links:[Link](https://openreview.net/forum?id=TPtXLihkny)Cited by:[§2](https://arxiv.org/html/2608.26329#S2.SS0.SSS0.Px2.p1.1)\.
- Yanget al\.\(2024\)A\. Yang, B\. Yang, B\. Hui, B\. Zheng, B\. Yu, C\. Zhou, C\. Li, C\. Li, D\. Liu, F\. Huang, G\. Dong, H\. Wei, H\. Lin, J\. Tang, J\. Wang, J\. Yang, J\. Tu, J\. Zhang, J\. Ma, J\. Yang, J\. Xu, J\. Zhou, J\. Bai, J\. He, J\. Lin, K\. Dang, K\. Lu, K\. Chen, K\. Yang, M\. Li, M\. Xue, N\. Ni, P\. Zhang, P\. Wang, R\. Peng, R\. Men, R\. Gao, R\. Lin, S\. Wang, S\. Bai, S\. Tan, T\. Zhu, T\. Li, T\. Liu, W\. Ge, X\. Deng, X\. Zhou, X\. Ren, X\. Zhang, X\. Wei, X\. Ren, X\. Liu, Y\. Fan, Y\. Yao, Y\. Zhang, Y\. Wan, Y\. Chu, Y\. Liu, Z\. Cui, Z\. Zhang, Z\. Guo, and Z\. FanQwen2 technical report\.External Links:2407\.10671,[Link](https://arxiv.org/abs/2407.10671)Cited by:[7th item](https://arxiv.org/html/2608.26329#A7.I1.i7.p1.1.1)\.
- Yanget al\.\(2022\)K\. Yang, J\. Deng, and D\. ChenGenerating natural language proofs with verifier\-guided search\.InProceedings of the 2022 Conference on Empirical Methods in Natural Language Processing,Y\. Goldberg, Z\. Kozareva, and Y\. Zhang \(Eds\.\),Abu Dhabi, United Arab Emirates,pp\. 89–105\.External Links:[Link](https://aclanthology.org/2022.emnlp-main.7/),[Document](https://dx.doi.org/10.18653/v1/2022.emnlp-main.7)Cited by:[§2](https://arxiv.org/html/2608.26329#S2.SS0.SSS0.Px2.p2.1)\.
- Zhanget al\.\(2025\)Z\. Zhang, C\. Zheng, Y\. Wu, B\. Zhang, R\. Lin, B\. Yu, D\. Liu, J\. Zhou, and J\. LinThe lessons of developing process reward models in mathematical reasoning\.InFindings of the Association for Computational Linguistics: ACL 2025,W\. Che, J\. Nabende, E\. Shutova, and M\. T\. Pilehvar \(Eds\.\),Vienna, Austria,pp\. 10495–10516\.External Links:[Link](https://aclanthology.org/2025.findings-acl.547/),[Document](https://dx.doi.org/10.18653/v1/2025.findings-acl.547),ISBN 979\-8\-89176\-256\-5Cited by:[§4](https://arxiv.org/html/2608.26329#S4.SS0.SSS0.Px2.p1.1),[Table 1](https://arxiv.org/html/2608.26329#S4.T1),[Table 2](https://arxiv.org/html/2608.26329#S4.T2),[Table 3](https://arxiv.org/html/2608.26329#S4.T3)\.
- Zhenget al\.\(2025\)C\. Zheng, Z\. Zhang, B\. Zhang, R\. Lin, K\. Lu, B\. Yu, D\. Liu, J\. Zhou, and J\. LinProcessBench: identifying process errors in mathematical reasoning\.InProceedings of the 63rd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\),W\. Che, J\. Nabende, E\. Shutova, and M\. T\. Pilehvar \(Eds\.\),Vienna, Austria,pp\. 1009–1024\.External Links:[Link](https://aclanthology.org/2025.acl-long.50/),[Document](https://dx.doi.org/10.18653/v1/2025.acl-long.50),ISBN 979\-8\-89176\-251\-0Cited by:[Appendix F](https://arxiv.org/html/2608.26329#A6.p3.1.1),[§4](https://arxiv.org/html/2608.26329#S4.SS0.SSS0.Px1.p1.1)\.

## Appendix AExample: Neuro\-Symbolic PRM Evaluation of a Verifier\-Passing but Ungrounded Step\.

We illustrate how NS\-PRM isolates semantic grounding errors that bypass symbolic verification\.

Problem\.A 2 kg object moves at 3 m/s\. What is its kinetic energy?

Given variables\.

Gext=\{\(m=2​kg\),\(v=3​m/s\)\}G\_\{\\text\{ext\}\}=\\\{\(m=2\\,\\text\{kg\}\),\(v=3\\,\\text\{m/s\}\)\\\}
Correct reasoning step\.

st\+=\(calc​\_​kinetic​\_​energy,\(m,v\),v^=9,u^=J\)s\_\{t\}^\{\+\}=\(\\operatorname\{calc\\\_kinetic\\\_energy\},\(m,v\),\\hat\{v\}=9,\\hat\{u\}=\\text\{J\}\)since:

K​E=12​m​v2=12⋅2⋅32=9​JKE=\\tfrac\{1\}\{2\}mv^\{2\}=\\tfrac\{1\}\{2\}\\cdot 2\\cdot 3^\{2\}=9\\,\\text\{J\}
CSP\-generated hard negative \(valid but ungrounded\)\.

st−=\(calc​\_​momentum,\(m,v\),v^=6,u^=kg·m/s\)s\_\{t\}^\{\-\}=\(\\operatorname\{calc\\\_momentum\},\(m,v\),\\hat\{v\}=6,\\hat\{u\}=\\text\{kg\\textperiodcentered m/s\}\)
Step 1: Symbolic verification\.

The verifier evaluates:

vtrue=exec⁡\(calc​\_​momentum,\(m,v\)\)=2⋅3=6v\_\{\\text\{true\}\}=\\operatorname\{exec\}\(\\operatorname\{calc\\\_momentum\},\(m,v\)\)=2\\cdot 3=6
unit⁡\(vtrue\)=kg·m/s\\operatorname\{unit\}\(v\_\{\\text\{true\}\}\)=\\text\{kg\\textperiodcentered m/s\}
The step is:

- •mathematically correct,
- •unit\-consistent,
- •fully executable\.

Step 2: PRM semantic scoring\.

The PRM evaluates:

ℛϕ​\(st∣x,s<t\)\\mathcal\{R\}\_\{\\phi\}\(s\_\{t\}\\mid x,s\_\{<t\}\)
ℛϕ​\(st\+\)≫ℛϕ​\(st−\)\\mathcal\{R\}\_\{\\phi\}\(s\_\{t\}^\{\+\}\)\\gg\\mathcal\{R\}\_\{\\phi\}\(s\_\{t\}^\{\-\}\)
Interpretation\.

Althoughst−s\_\{t\}^\{\-\}satisfies all symbolic constraints \(V=1V=1\), it applies the wrong physical principle \(momentum instead of kinetic energy\)\. This constitutes a violation of semantic groundedness:

Conclusion\.

NS\-PRM correctly handles this case by:

- •delegating execution correctness to the symbolic verifier,
- •evaluating only verifier\-passing steps,
- •distinguishing correct vs\. incorrect reasoning purely on semantic grounding\.

## Appendix BDetailed Hybrid Data Generation Pipeline for CSP

To train the Process Reward Model \(PRM\) to effectively isolate Semantic Groundedness \(GG\) from Symbolic Validity \(VV\), we require a vast dataset of hard negative steps\. Pure LLM generation struggles to produce hard negatives that are simultaneously contextually wrong but mathematically valid without hallucinating arithmetic errors\. Conversely, purely algorithmic perturbation lacks the reasoning depth to select plausible, non\-trivial semantic distractors\.

To resolve this, we utilize aHybrid Data Generation Pipelinethat leverages GPT\-5\.2 for high\-level semantic targeting and a deterministic symbolic engine for rigorous mathematical execution\.

### B\.1Step 1: Positive Trace Collection and Verification

We begin by sampling candidate solutions for our training queries using the base generator model\. These traces are structured according to our JSON SchemaΣ\\Sigma\. We filter out any paths that result in incorrect final answers\. The remaining paths are evaluated step\-by\-step by our oracle model \(GPT\-5\.2\) to ensure no intermediate logical flaws exist \(i\.e\., avoiding false positive traces where two wrong steps cancel out\)\. This yields the set of verified positive steps𝒟\+=\{st\+\}\\mathcal\{D\}^\{\+\}=\\\{s\_\{t\}^\{\+\}\\\}\.

### B\.2Step 2: Semantic Proposal via GPT\-5\.2

For each valid stepst\+s\_\{t\}^\{\+\}in a trace, we provide GPT\-5\.2 with the problem text, the extracted given variablesGextG\_\{\\text\{ext\}\}, and the trace historys<ts\_\{<t\}\. We prompt GPT\-5\.2 to act as an adversarial logic proposer\. Depending on the intended perturbation policy, GPT\-5\.2 outputs a structured suggestion:

- •For Contextual Logic Perturbation:GPT\-5\.2 identifies the ground\-truth operatoropt\\operatorname\{op\}\_\{t\}\(e\.g\.,E=12​m​v2E=\\frac\{1\}\{2\}mv^\{2\}\) and proposes an alternative formula that is plausible in the current domain but incorrect for the specific contextual goal \(e\.g\., proposingE=m​g​hE=mghorp=m​vp=mv\)\.
- •For Semantic Operand Perturbation:GPT\-5\.2 identifies an argument in𝐚𝐫𝐠𝐬t\\mathbf\{args\}\_\{t\}and proposes an isomorphic variable swap\. For instance, if the formula expects the ‘initial\_velocity‘ variable, GPT\-5\.2 scans the context and proposes substituting it with ‘final\_velocity‘ or ‘average\_velocity‘, ensuring the proposed replacement shares the exact physical dimensions and type\.

Crucially, GPT\-5\.2 is explicitly instructednotto attempt recalculating the outputs\. It simply outputs a JSON payload containing the altered schema parameters \(the newop\\operatorname\{op\}or swapped𝐚𝐫𝐠𝐬\\mathbf\{args\}\)\.

### B\.3Step 3: Algorithmic Execution and Balancing

Once the semantic perturbation is proposed by GPT\-5\.2, the deterministic engine takes over to guaranteeV⁡\(st−\)=1V\(s\_\{t\}^\{\-\}\)=1\. Let the GPT\-proposed altered step be denoted by its inputs:\(opt−,𝐚𝐫𝐠𝐬t−\)\(\\operatorname\{op\}\_\{t\}^\{\-\},\\mathbf\{args\}\_\{t\}^\{\-\}\)\. The pipeline algorithmically passes these inputs into the backend symbolic verifier𝒱\\mathcal\{V\}\(powered by Pint and our algebraic execution engine\)\.

The engine executes the perturbed operation:

𝐎perturbed=exec⁡\(opt−,𝐚𝐫𝐠𝐬t−\)\\mathbf\{O\}\_\{\\text\{perturbed\}\}=\\operatorname\{exec\}\(\\operatorname\{op\}\_\{t\}^\{\-\},\\mathbf\{args\}\_\{t\}^\{\-\}\)\(3\)The solver automatically computes the exact numerical results, resolves dimensional analysis, and applies appropriate unit conversions\. The resulting mathematically perfect tuples𝐎^t−\\mathbf\{\\hat\{O\}\}\_\{t\}^\{\-\}are then injected back into the step schema to complete the construction of the negative stepst−s\_\{t\}^\{\-\}\.

### B\.4Step 4: Construction of𝒟−\\mathcal\{D\}^\{\-\}

By pairing the adversarial logic of GPT\-5\.2 with the absolute mathematical precision of the algorithmic solver, we yieldst−=\(opt−,𝐚𝐫𝐠𝐬t−,𝐎^t−\)s\_\{t\}^\{\-\}=\\left\(\\operatorname\{op\}\_\{t\}^\{\-\},\\mathbf\{args\}\_\{t\}^\{\-\},\\mathbf\{\\hat\{O\}\}\_\{t\}^\{\-\}\\right\)\. This step is guaranteed to pass the hard filter𝒱\\mathcal\{V\}during inference, forcing the PRM to rely strictly on contextual reasoning to distinguishst\+s\_\{t\}^\{\+\}fromst−s\_\{t\}^\{\-\}\. We compile these into the negative training set𝒟−\\mathcal\{D\}^\{\-\}\.

## Appendix CPost\-Hoc Schema Translation

A known trade\-off in structured reasoning is thecognitive load overhead: enforcing a rigid schema during generation can degrade the model’s reasoning performance on highly complex problems, leading to repeated parsing failures despite the retry budgetRmaxR\_\{\\max\}\. To mitigate this, we introduce aPost\-Hoc Schema Translationmechanism as a fail\-safe remedy\.

If the Parse–Validate–Retry loop exhaustsRmaxR\_\{\\max\}without producing a valid structured trace, we trigger a two\-stage fallback process:

##### Stage 1: Free\-Form Generation \(Relaxed Mode\)

We relax the constraintΣ\\Sigmaand prompt the model to generate a solutionJrawJ\_\{\\text\{raw\}\}using standard free\-form Chain\-of\-Thought \(CoT\)\. This allows the model to focus entirely on the logical derivation without the overhead of formatting syntax\.

Jraw∼pθ\(⋅∣x,format=free\_text\)\.\\displaystyle J\_\{\\text\{raw\}\}\\sim p\_\{\\theta\}\(\\cdot\\mid x,\\text\{format\}=\\texttt\{free\\\_text\}\)\.\(4\)

##### Stage 2: Structural Translation

We then freezeJrawJ\_\{\\text\{raw\}\}and prompt the model \(or a lightweight auxiliary model\) to translate the natural language reasoning into the structured schemaΣ\\Sigma:

Jrec=𝒯θ​\(Jraw∣Σ\),\\displaystyle J\_\{\\text\{rec\}\}=\\mathcal\{T\}\_\{\\theta\}\(J\_\{\\text\{raw\}\}\\mid\\Sigma\),\(5\)where𝒯θ\\mathcal\{T\}\_\{\\theta\}is a translation prompt \(e\.g\.,“Rewrite the above solution into the defined JSON format”\)\.

##### Outcome

The recovered traceJrecJ\_\{\\text\{rec\}\}is then passed to the Symbolic Verifier𝒱\\mathcal\{V\}\.

- •If𝒱⁡\(Jrec\)=ok\\mathcal\{V\}\(J\_\{\\text\{rec\}\}\)=\\texttt\{ok\}, the trace is promoted to the valid candidate pool𝒮valid\\mathcal\{S\}\_\{\\text\{valid\}\}\.
- •If translation fails, we acceptJrawJ\_\{\\text\{raw\}\}as a validunverifiedcandidate, but assign it a penalized symbolic score \(Priority 1 =False\), ensuring it is only selected if no other verified traces exist\.

This hybrid approach ensures high coverage: we enforce rigor where possible, but gracefully degrade to standard CoT when the schema becomes a bottleneck, ensuring the system remains robust for hard\-to\-parse instances\.

## Appendix DPrimitive Library Coverage and Extensibility

### D\.1Taxonomy of the Primitive Library

The structured reasoning constraint relies on the comprehensiveness of the operator set𝒪\\mathcal\{O\}\. Our current implementation partitions𝒪\\mathcal\{O\}into:

- •𝒪calc\\mathcal\{O\}\_\{\\text\{calc\}\}: Contains 128 core physics/math functions \(e\.g\., ‘calc\_kinetic\_energy‘, ‘solve\_quadratic‘, ‘vector\_dot\_product‘\) derived from standard undergraduate curricula\.
- •𝒪logic\\mathcal\{O\}\_\{\\text\{logic\}\}: Contains 15 deductive operators \(e\.g\., ‘isolate\_variable‘, ‘substitute\_equation‘\)\.

We provide the exhaustive list of the 15 logical proof\-state primitives \(Table[5](https://arxiv.org/html/2608.26329#A4.T5)\) and the 128 computational and physical primitives \(Table[6](https://arxiv.org/html/2608.26329#A4.T6)\) utilized by our deterministic symbolic verifier\.

Logical CategoryPrimitive NameDeterministic Verification MechanismProof State &define\_variableRegisters a variable, its value, and physical unit into the verifiable state dictionary\.Initializationdeclare\_targetRegisters the final goal variable to evaluate proof completion\.assume\_premiseInjects a hypothetical condition into the current search branch\.branch\_casesSplits the search tree into bounded, mutually exclusive state copies \(e\.g\.,±\\pmroots\)\.Equivalence &equate\_expressionsUses CAS to verifysimplify​\(A−B\)==0\\text\{simplify\}\(A\-B\)==0\.Substitutionsubstitute\_identityVerifies variable exists in history, checks unit match, and replaces in target expression\.substitute\_equationReplacing a variable with a number or an equivalent expression to solve an equation or simplify a formula\.factorize\_termsUses CAS polynomial factorization to restructure the expression\.Constraint &assert\_domain\_boundsRegisters a mathematical bound \(e\.g\.,x∈ℝx\\in\\mathbb\{R\},t\>0t\>0\) to the constraint tracker\.Domain Logiccheck\_inequalityVerifies numeric or symbolic inequalities \(e\.g\.,A≥BA\\geq B\) against current state\.verify\_dimensionsInvokes Pint backend to prove LHS and RHS share identical physical base units\.assert\_continuityChecks if a symbolic function is continuous/differentiable over the stated domain\.Resolution &resolve\_systemTriggers deterministic linear/non\-linear matrix solvers on registered equations\.Terminationflag\_contradictionVerifier checks if current state violates prior bounds \(e\.g\., returning𝒱=0\\mathcal\{V\}=0\)\.conclude\_proofAsserts the calculated target variable matches the schema’s required answer format\.

Table 5:The 15 Logical and Deductive Operations \(𝒪logic\\mathcal\{O\}\_\{\\text\{logic\}\}\)\.Table 6:The 128 Computational and Physical Primitives \(𝒪calc\\mathcal\{O\}\_\{\\text\{calc\}\}\)\.
### D\.2Handling Out\-of\-Vocabulary \(OOV\) Operations

To mitigate the risk of limited expressivity for long\-tail scientific problems, we implement aPython\-Fallback Primitive\(opcode\\operatorname\{op\}\_\{\\text\{code\}\}\)\. If the generative model assigns low probability \(p<τp<\\tau\) to all structured primitives in𝒪\\mathcal\{O\}, it can invokeopcode\\operatorname\{op\}\_\{\\text\{code\}\}\. This triggers a sub\-routine where the model generates free\-form Python code to perform the calculation\. The Symbolic Verifier𝒱\\mathcal\{V\}sandbox\-executes this code\. While this bypasses the strict structural schema, it preserves the deterministic verification guarantee \(the code must run without errors and yield a properly typed result\)\.

We analyze the coverage of𝒪\\mathcal\{O\}against the validation set as follows:

1. 1\.Coverage Rate:We measure the percentage of ground\-truth solution steps that can be successfully parsed into𝒪\\mathcal\{O\}\. Our library covers94\.2%94\.2\\%of steps in the benchmark datasets\.
2. 2\.Fallback Mechanism:For the remaining5\.8%5\.8\\%of steps requiring abstract reasoning \(e\.g\., “Explain why friction is negligible”\), we implement aGeneric\_Text\_Op\. This operation bypasses𝒪calc\\mathcal\{O\}\_\{\\text\{calc\}\}verification and relies solely on the PRM score for validation, effectively falling back to standard soft\-probabilistic reasoning\.

Future work will exploreDynamic Primitive Synthesis, where the model can propose new pythonic functions to be added to𝒪calc\\mathcal\{O\}\_\{\\text\{calc\}\}on the fly, subject to unit\-test verification\.

## Appendix EGraceful Degradation for Unverifiable Operations

While our deterministic verifier𝒱\\mathcal\{V\}guarantees Symbolic Validity \(V=1V=1\) for standard arithmetic and algebraic manipulations, applying this framework to broader STEM domains \(e\.g\., geometric proofs, abstract logical deductions\) inevitably encounters operations that cannot be deterministically evaluated by a lightweight symbolic engine\.

To maintain robustness when verifier coverage is incomplete, we partition the operational schemaΣ\\Sigmainto two sets:Strict Operations\(𝒪strict\\mathcal\{O\}\_\{\\text\{strict\}\}\) andOpen Operations\(𝒪open\\mathcal\{O\}\_\{\\text\{open\}\}\)\. Foropt∈𝒪open\\operatorname\{op\}\_\{t\}\\in\\mathcal\{O\}\_\{\\text\{open\}\}\(e\.g\.,geometric\_insight,abstract\_rewrite\), the verifier cannot guarantee validity and instead returns an abstention:V⁡\(st\)=UnverifiedV\(s\_\{t\}\)=\\text\{Unverified\}\.

To handle these cases seamlessly during our Verifier\-First Search, we implement aDynamic PRM Fallback\. WhenV⁡\(st\)=UnverifiedV\(s\_\{t\}\)=\\text\{Unverified\}, the hard filter is bypassed, and the PRMℛϕ\\mathcal\{R\}\_\{\\phi\}is tasked with evaluatingbothexecution validity and semantic groundedness\. To support this dual\-capability, we augment our CSP training mixture for𝒪open\\mathcal\{O\}\_\{\\text\{open\}\}operations with standard execution errors \(e\.g\., hallucinated outputs or syntax flaws\), ensuring the PRM gracefully degrades into a standard holistic evaluator only when the deterministic engine abstains\.

### E\.1Performance Under Low Symbolic Coverage

We evaluate performance on theMATH\-Geometrysubset \(where spatial/visual reasoning limits the use of traditional equation solvers\) and theAIME24dataset \(which requires highly abstract logical insights\)\. We track theVerifier Abstention Rateand compare the performance of our dynamic fallback PRM against baselines\.

Table 7:Framework performance across domains with varying verifier coverage\. Even when the symbolic verifier abstains frequently \(e\.g\., 38\.5% in Geometry\), our Dynamic Fallback ensures the PRM steps in as a holistic evaluator, consistently outperforming standard PRM baselines\.The results in Table[7](https://arxiv.org/html/2608.26329#A5.T7)confirm that our framework is not brittle to the boundaries of the symbolic engine\. In Geometry, where the verifier abstains on nearly 40% of operations \(relying on𝒪open\\mathcal\{O\}\_\{\\text\{open\}\}primitives\), the Dynamic Fallback mechanism allows the CSP\-trained PRM to maintain robust evaluation\. While the accuracy gap between our method and standard PRMs narrows as verification guarantees weaken, our system strictly lower\-bounds the performance of a traditional PRM while capturing massive gains wherever symbolic constraints can be enforced\.

## Appendix FDetailed Dataset Descriptions

To evaluate the generalization and robustness of our neuro\-symbolic process verification framework, we utilized the following datasets for training and testing:

PRM800K\([Lightman et al\., 2024](https://arxiv.org/html/2608.26329#bib.bib9)\):Used as our core foundation for extracting base mathematical queries\. The dataset contains highly complex, step\-by\-step verified MATH problems\. We sampled queries from this dataset to initiate our oracle\-guided data generation pipeline\.

ProcessBench\([Zheng et al\., 2025](https://arxiv.org/html/2608.26329#bib.bib19)\):A benchmark explicitly designed to evaluate how well models can identify logical and process errors within mathematical deductive chains\. We utilize ProcessBench to assess step\-level classification metrics \(Error, Correct, and F1\)\.

PRMBench\([Song et al\., 2025](https://arxiv.org/html/2608.26329#bib.bib20)\):A fine\-grained, challenging evaluation suite for Process Reward Models\. PRMBench dissects evaluation into multi\-dimensional axes, notablySimplicity,Soundness\(resistance to hallucinated premises\), andSensitivity\(the ability to detect minor mathematical or citation disruptions\)\.

Standard Mathematical Benchmarks:For test\-time reward\-guided generation, we evaluated over standard, widely\-adopted suites includingGSM8K\([Cobbe et al\., 2021](https://arxiv.org/html/2608.26329#bib.bib14)\)for grade\-school level reasoning,MATH/MATH500\([Hendrycks et al\., 2021](https://arxiv.org/html/2608.26329#bib.bib22)\)for competition\-level mathematics, andOlympiadBench\([He et al\., 2024](https://arxiv.org/html/2608.26329#bib.bib16)\)andOmniMATHfor highly difficult, multi\-branched advanced mathematical theorems\. We also report zero\-shot guided performance on subsets likeAIME,AMC,College Math, andMinerva Math\.

SciBench\([Wang et al\., 2024b](https://arxiv.org/html/2608.26329#bib.bib23)\)& GPQA\([Rein et al\., 2023](https://arxiv.org/html/2608.26329#bib.bib24)\):Used for out\-of\-domain evaluation on complex science reasoning\. We uniformly sampled1,0001,000physics and chemistry data points from SciBench for domain adaptation\.

## Appendix GBaselines and Comparison Methods

We benchmark NS\-PRM against a rigorous suite of state\-of\-the\-art proprietary and open\-weight process reward models and verification systems:

- •Math\-Shepherd\-7B\([Wang et al\., 2024a](https://arxiv.org/html/2608.26329#bib.bib25)\):A prominent process reward model initialized from Mistral/Llama weights, trained using automatically generated step\-level annotations via Monte Carlo Tree Search\.
- •Math\-PSA\-7B:A process reward model leveraging step\-aware learning paradigms to improve upon standard dense reward modeling\.
- •RLHFlow Models\([Dong et al\., 2024](https://arxiv.org/html/2608.26329#bib.bib17)\):Recent verification models trained on iterative reinforcement learning from human/AI feedback, built upon the Mistral\-8B and DeepSeek\-Math\-8B architectures\.
- •Llemma\-PRM800K\-7B\([Azerbayev et al\., 2024](https://arxiv.org/html/2608.26329#bib.bib26)\):The Llemma\-7B foundational math model directly fine\-tuned on the step\-level verification annotations provided in the PRM800K open dataset\.
- •Skywork\-PRM\-7B\([Liu et al\., 2024](https://arxiv.org/html/2608.26329#bib.bib18)\):A state\-of\-the\-art open\-source PRM trained to evaluate step\-by\-step scientific and mathematical rationale\.
- •ReasonEval\-7B\([Xia et al\., 2025](https://arxiv.org/html/2608.26329#bib.bib27)\):A dedicated reward model designed to output detailed evaluations of the intrinsic reasoning capability in autoregressive chain\-of\-thought traces\.
- •Qwen2\.5 Series\([Yang et al\., 2024](https://arxiv.org/html/2608.26329#bib.bib28)\):We utilize both the Qwen2\.5\-Math\-7B and the highly optimized Qwen2\.5\-Math\-PRM\-7B as our direct architectural baselines\.
- •R\-PRM\-7B\([She et al\., 2025](https://arxiv.org/html/2608.26329#bib.bib15)\):A highly recent robustness\-focused process reward model trained with both Supervised Fine\-Tuning \(SFT\) and Direct Preference Optimization \(DPO\) to resist adversarial mathematical perturbations\.