Source-linked AI summary
Neuro-symbolic PRM: Enhancing Scientific Reasoning via Structured Traces and Symbolic Verification
Yuxin Zi, Cong Xu, Suparna Bhattacharya, Martin Foltin, Amit Sheth
TL;DR
Tool-augmented reasoning still permits executable but semantically ungrounded steps, while existing verifiers and PRMs do not cleanly separate execution validity from logical intent. The paper introduces NS-PRM, combining deterministic verifier filtering, CSP-generated hard negatives, and verifier-first search; it reports improved reliability and efficiency across process benchmarks and complex reasoning tasks.
Problem
Structured quantitative STEM reasoning still contains syntactically and mathematically executable steps that are contextually ungrounded, while verifiers miss semantic intent and PRMs must learn execution rules alongside grounding.
Method
NS-PRM separates Symbolic Validity from Semantic Groundedness using a deterministic hard-filter verifier, CSP hard negatives, and verifier-first constrained search with PRM ranking.
Results
NS-PRM significantly outperforms monolithic PRMs on PRMBench and ProcessBench and on GPQA and SciBench complex reasoning tasks.
Takeaways & Limitations
Verifier-first search removes execution errors and enables wider beam searches without consuming expensive neural forward passes, while CSP exposes semantically flawed but syntactically perfect steps.
Takeaways & Limitations
The verifier guarantees execution validity only for covered operations and does not strictly guarantee scientific correctness; structured formatting may struggle with implicit assumptions in real-world engineering queries.
Abstract
from arXiv · showhide
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 ($V$) and Semantic Groundedness ($G$). We guarantee $V$ by construction using a deterministic symbolic verifier acting as a hard filter. To assess $G$, 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.
1 Introduction
Tool augmentation removes many arithmetic and syntax errors but leaves executable reasoning steps that are semantically ungrounded. NS-PRM separates symbolic validity from semantic groundedness, using deterministic filtering and specialized neural ranking.
- Tool-augmented LLMs offload computation to deterministic engines, eliminating most calculation and syntax errors.
- Executable-but-ungrounded steps can use correct formulas with wrong variables or compute contextually irrelevant quantities.Such steps may remain syntactically valid, numerically executable, and unit-consistent.
- NS-PRM decouples reasoning correctness into Symbolic Validity and Semantic Groundedness.
- A deterministic symbolic verifier hard-filters execution validity, while a specialized PRM evaluates contextual appropriateness.This division targets errors that symbolic verification cannot catch.
2 Related Work
Prior approaches use tools, PRMs, learned verifiers, and external feedback to improve reasoning, but often rely on neural approximations or fail to address executable-but-ungrounded steps. NS-PRM instead combines symbolic verifier-first pruning with PRM-guided semantic ranking.
- Program-of-Thoughts, PAL, and ToRA offload computation to Python interpreters, but typically treat the external tool as a black-box calculator.
- PRM methods provide step-wise supervision and trajectory scoring, while related learned verifiers rely on neural approximations.
- NS-PRM uses symbolically constrained beam search with verifier-first pruning and PRM-guided ranking rather than treating the PRM as an oracle.A high-likelihood neural prediction cannot override a proven symbolic contradiction.
- CSP targets executable-but-ungrounded steps, unlike prior perturbation methods focused on logical proofs or standard code execution.
- Parse–Validate–Retry supplies external compiler-style feedback during generation to address weak self-correction by language models.
3 Method
The method represents quantitative reasoning as structured traces, separates symbolic validity from semantic groundedness, and assigns each dimension to a different mechanism. A deterministic verifier filters executable steps, while CSP-trained PRM ranking guides verifier-accepted search toward contextually valid reasoning.
- Structured Reasoning Representation: Structured quantitative STEM reasoning is restricted to deterministic calculations or algebraic manipulations represented in a schema-defined trace.The trace contains extracted given variables, an ordered sequence of reasoning steps, and a possibly multi-part final answer.
- Structured Reasoning Representation: Each reasoning step applies a typed operation to references from prior history or extracted givens and can generate multiple value-unit variables.The output is represented as a set of tuples to support operations such as vector decomposition or multiple quadratic roots.
- Symbolic Verification: The symbolic verifier deterministically checks schema and type conformity, mathematical equivalence within ϵ = 10^-5, and dimensional consistency.It executes covered operations and verifies all resulting outputs, including unit equivalences handled through Pint.
- Symbolic Verification: The verifier guarantees execution validity but delegates semantic truth to the PRM, so verifier acceptance does not guarantee scientific correctness.The PRM models semantic groundedness conditionally on verifier acceptance rather than rechecking arithmetic or units.
- Counterfactual Symbolic Perturbation: CSP creates verifier-passing hard negatives by perturbing the logical principle or swapping an isomorphic, unit- and type-compatible operand.A deterministic algebraic solver recomputes outputs after the oracle proposes a semantic perturbation, ensuring the negative remains mathematically executable.
- Verifier-First Search: The PRM is trained on CSP positive-negative pairs to learn semantic grounding, then ranks candidates only after verifier-first pruning.This search design keeps selected steps on the verifier-accepted manifold while using neural scoring to preserve a logical solution path and reduce evaluation bottlenecks.
4 Experiments
Across process evaluation, downstream reasoning, science benchmarks, efficiency tests, and ablations, NS-PRM combines deterministic verification with CSP-trained semantic ranking to improve reliability and search efficiency.
- Experimental Setup: 140,000 positive and 140,000 negative step-level datapoints form a balanced PRM training set of verifier-passing, constraint-preserving negatives.The positives come from oracle-verified correct traces, while negatives are generated through CSP.
- Process-Level Evaluation: 69.8 versus 62.1 F1 on OlympiadBench and 68.5 versus 60.2 on OmniMATH show large gains when the deterministic verifier is added to CSP-PRM.The integrated verifier-plus-CSP configuration is compared with the purely neural CSP-PRM configuration.
- Downstream Reasoning: 83.1% on MATH demonstrates state-of-the-art PRM-guided Best-of-8 decoding, with verified pruning focusing search on mathematically viable trajectories.Verifier-first pruning removes logically doomed branches before neural expansion.
- Complex Science Reasoning: +3.6% average improvement of verified NS-PRM over its purely neural counterpart appears on complex science reasoning benchmarks.The paper attributes the improvement to the deterministic validity filter bridging part of the gap to frontier reinforcement-learning models.
- Compute Efficiency: +4.5% absolute accuracy on MATH is achieved by a B = 28 verifier-first search at the same ∼900 GFLOP budget as a B = 16 monolithic PRM.The monolithic B = 16 configuration scores 82.3%, while verifier pruning enables nearly double the search width under matched compute.
- Ablation Study: 75.4 ± 0.2% ProcessBench F1 for Joint CSP exceeds Logic Perturbation Only at 71.2 ± 0.4% and Operand Perturbation Only at 70.9 ± 0.5%.The joint policy combines formula-retrieval and variable-grounding perturbations.
5 Discussion and Conclusion
The framework separates Symbolic Validity from Semantic Groundedness, combining deterministic execution filtering with PRM-based assessment of logical intent. It reports broader reliability and efficiency gains while acknowledging limits in implicit, abstract, and spatial settings.
- Structured formatting may struggle with implicit assumptions in real-world engineering queries, while efficiency gains are less pronounced in abstract or spatial domains such as geometry.
- Maintaining a domain-specific deterministic library creates upfront engineering overhead, though the paper states that test-time computational savings offset it.
- The framework separates reasoning into Symbolic Validity and Semantic Groundedness, using a deterministic engine for execution errors and CSP-trained PRMs for semantic flaws.
- Verifier-First Constrained Search increases test-time efficiency by enabling wider beam searches without consuming additional neural forward passes.
- The unified approach outperforms monolithic PRMs on PRMBench, ProcessBench, GPQA, and SciBench.
B Detailed Hybrid Data Generation Pipeline for CSP
The hybrid CSP pipeline combines model-generated semantic adversaries with deterministic execution to create hard negatives that remain mathematically valid but contextually flawed. Verified positive traces are perturbed, executed, and completed into negative training examples.
- The pipeline combines GPT-5.2 semantic targeting with a deterministic symbolic engine for rigorous mathematical execution.
- Candidate traces are schema-structured, filtered for correct final answers, and checked step-by-step to produce verified positive steps D+.
- For each valid step, GPT-5.2 receives the problem, extracted variables, and trace history, then proposes a structured adversarial perturbation.
- Contextual Logic Perturbation replaces the ground-truth operator with a plausible domain formula that is incorrect for the specific contextual goal.
- Semantic Operand Perturbation swaps an argument for an isomorphic variable with matching physical dimensions and type.
- GPT-5.2 outputs altered schema parameters without recalculating outputs, after which the symbolic engine computes exact results, resolves dimensions, and applies unit conversions.
B.4 Step 4: Construction of D−
The construction of D− completes adversarially perturbed steps with deterministic execution, producing negatives that pass the symbolic validity filter and therefore test semantic discrimination. A fallback mechanism preserves coverage when rigid schemas fail.
- Step 4: Construction of D−: The resulting negative step is guaranteed to pass the hard filter V, forcing the PRM to distinguish it through contextual reasoning.
- Post-Hoc Schema Translation: Rigid schemas can increase cognitive load and cause repeated parsing failures on highly complex problems despite the retry budget Rmax.
- Post-Hoc Schema Translation: After Rmax is exhausted, the system generates free-form CoT, translates it into schema Σ, and sends the recovered trace to verifier V.
- Post-Hoc Schema Translation: Verified translated traces enter Svalid, while failed translations remain penalized unverified candidates selected only when no verified traces exist.
- Post-Hoc Schema Translation: The hybrid fallback enforces rigor where possible while degrading gracefully to standard CoT for hard-to-parse instances.
- Operator schema: The structured operator set includes 128 computational and physical primitives and 15 logical proof-state primitives.
D.2 Handling Out-of-Vocabulary (OOV) Operations
The system handles out-of-vocabulary operations through Python execution and dynamic PRM fallback, preserving coverage while weakening deterministic guarantees for unverifiable steps. Current operator coverage reaches 94.2% of benchmark solution steps.
- A Python-Fallback Primitive invokes generated Python when all structured primitives receive probability below threshold τ, with sandbox execution preserving deterministic typed-result checking.
- The operator library parses 94.2% of benchmark solution steps, while the remaining 5.8% use a Generic Text Op and PRM-only validation.
- Broader STEM domains include operations that a lightweight symbolic engine cannot deterministically evaluate, such as geometric proofs and abstract logical deductions.
- For open operations, the verifier returns Unverified rather than guaranteeing validity.
- When verification abstains, Dynamic PRM Fallback evaluates both execution validity and semantic groundedness using CSP training augmented with standard execution errors.
E.1 Performance Under Low Symbolic Coverage
The framework remains robust when symbolic verification coverage is limited, using Dynamic Fallback to let the CSP-trained PRM evaluate operations outside verifier coverage. Geometry provides the clearest stress test, with frequent verifier abstention and a narrower advantage over standard PRMs.
- Evaluation setup: Evaluation targets MATH-Geometry and AIME24 while tracking Verifier Abstention Rate and comparing Dynamic Fallback against baselines.Geometry limits traditional equation solvers through spatial and visual reasoning, whereas AIME24 requires highly abstract logical insights.
- Verifier primitives: Table 6 catalogs 128 computational and physical primitives used by the symbolic system.These primitives are labeled Ocalc in the table description.
- Low symbolic coverage: 38.5% verifier abstention in Geometry demonstrates performance under frequent gaps in symbolic coverage.The framework is described as not brittle to the symbolic engine’s boundaries.
- Dynamic fallback: Dynamic Fallback lets the CSP-trained PRM maintain robust evaluation when the verifier abstains, relying on Oopen primitives.The PRM acts as a holistic evaluator when symbolic constraints cannot be enforced.
- Performance trade-off: The accuracy gap between the framework and standard PRMs narrows as verification guarantees weaken, while performance remains strictly lowerbounded by a traditional PRM.The largest gains occur where symbolic constraints can be enforced.
F Detailed Dataset Descriptions
The evaluation uses datasets spanning mathematical reasoning, step-level process verification, fine-grained PRM assessment, standard benchmark testing, and out-of-domain science reasoning. Training data and evaluation suites are assigned distinct roles across this spectrum.
- Scope: The dataset collection is used to evaluate generalization and robustness of the neuro-symbolic process verification framework.The datasets support training, testing, process classification, PRM evaluation, and science-domain assessment.
- Training foundation: PRM800K supplies complex, step-by-step verified MATH problems for base query extraction and oracle-guided data generation.It serves as the core foundation for extracting mathematical queries.
- Process evaluation: ProcessBench evaluates step-level identification of logical and process errors using Error, Correct, and F1 metrics.It is designed to assess errors within mathematical deductive chains.
- PRM evaluation: PRMBench evaluates PRMs across Simplicity, Soundness, and Sensitivity.Its axes cover resistance to hallucinated premises and detection of minor mathematical or citation disruptions.
- Mathematical benchmarks: Standard mathematical suites cover grade-school, competition-level, and advanced multi-branched reasoning, with zero-shot subsets including AIME, AMC, College Math, and Minerva Math.The listed suites include GSM8K, MATH/MATH500, OlympiadBench, and OmniMATH.
- Out-of-domain evaluation: SciBench and GPQA provide out-of-domain evaluation for complex science reasoning, including 1,000 uniformly sampled physics and chemistry points from SciBench.The SciBench sample is used for domain adaptation.
G Baselines and Comparison Methods
NS-PRM is compared with a broad suite of proprietary and openweight process reward models and verification systems. The baselines span diverse training strategies, architectures, and robustness objectives.
- Process reward baselines: The benchmark suite includes Math-Shepherd-7B, Math-PSA-7B, RLHFlow Models, and Llemma-PRM800K-7B.These baselines use Monte Carlo Tree Search annotations, step-aware learning, iterative reinforcement learning from feedback, or PRM800K annotations.
- Rationale evaluation: Skywork-PRM-7B and ReasonEval-7B evaluate scientific and mathematical rationales or intrinsic reasoning capability in autoregressive traces.Skywork is described as open-source, while ReasonEval outputs detailed evaluations.
- Architectural baselines: Qwen2.5-Math-7B and Qwen2.5-Math-PRM-7B serve as direct architectural baselines.Both models belong to the Qwen2.5 series used for comparison.
- Robustness baseline: R-PRM-7B is a robustness-focused model trained with SFT and DPO to resist adversarial mathematical perturbations.Its training objective provides a robustness-oriented comparison point.