Neuro-symbolic PRM: Enhancing Scientific Reasoning via Structured Traces and Symbolic Verification
Organizations: AI Institute of South Carolina · HPE Labs · Indian AI Research Organisation
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 () and Semantic Groundedness (). We guarantee by construction using a deterministic symbolic verifier acting as a hard filter. To assess , 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.
Figures & tables
| MODEL | GSM8K | MATH | OlympiadBench | OmniMATH | Avg. F1 | ||||||||
| err | corr | F1 | err | corr | F1 | err | corr | F1 | err | corr | F1 | ||
| Math-Shepherd-7B ⋆ | 32.4 | 91.7 | 47.9 | 18.0 | 82.0 | 29.5 | 15.0 | 71.1 | 24.8 | 14.2 | 73.0 | 23.8 | 31.5 |
| Math-PSA-7B + | 48.3 | 88.1 | 62.4 | 29.5 | 72.7 | 41.9 | 20.7 | 65.8 | 31.5 | 15.4 | 68.9 | 25.2 | 40.3 |
| RLHFlow-Mistral-8B ⋆ | 33.8 | 99.0 | 50.4 | 21.7 | 72.2 | 33.4 | 8.2 | 43.1 | 13.8 | 9.6 | 45.2 | 15.8 | 28.4 |
| RLHFlow-DeepSeek-8B ⋆ | 24.2 | 98.4 | 38.8 | 21.4 | 80.0 | 33.8 | 10.1 | 51.0 | 16.9 | 10.1 | 51.9 | 16.9 | 26.6 |
| Llemma-PRM800K-7B ⋆ | 36.7 | 71.0 | 48.4 | 39.2 | 47.8 | 43.1 | 33.1 | 25.1 | 28.5 | 35.4 | 31.5 | 33.4 | 38.4 |
| Model | Simplicity | Soundness | Sensitivity | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| NR | NCL | Avg | ES | SC | DC | CI | Avg | PS | DR | MS | Avg | |
| Math-Shepherd-7B ⋆ | 44.0 | 50.3 | 47.1 | 49.4 | 44.5 | 41.3 | 47.7 | 45.7 | 47.2 | 48.6 | 86.1 | 60.7 |
| Math-PSA-7B + | 47.6 | 55.1 | 51.3 | 56.5 | 49.4 | 47.1 | 54.2 | 51.8 | 51.7 | 54.1 | 88.9 | 64.9 |
| RLHFlow-Mistral-8B ⋆ | 46.1 | 47.3 | 46.7 | 56.6 | 55.1 | 54.4 | 63.8 | 57.5 | 51.5 | 56.2 | 97.9 | 68.5 |
| RLHFlow-DeepSeek-8B ⋆ | 46.4 | 48.9 | 47.6 | 55.7 | 55.0 | 53.2 | 66.2 | 57.5 | 49.0 | 55.4 | 99.8 | 68.1 |
| Llemma-PRM800k-7B ⋆ | 49.3 | 53.4 | 51.4 | 56.4 | 47.1 | 46.7 | 53.3 | 50.9 | 51.0 | 53.5 | 93.6 | 66.0 |
| Setting | AIME | AMC | MATH | Olympiad | College | Minerva | Avg. |
|---|---|---|---|---|---|---|---|
| pass@1 | 11.2 | 47.8 | 73.0 | 38.0 | 38.6 | 37.2 | 41.0 |
| major@8 | 20.0 | 57.5 | 79.6 | 47.0 | 41.5 | 42.7 | 48.1 |
| pass@8 (Upper) | 33.3 | 82.5 | 88.8 | 58.5 | 47.5 | 57.7 | 61.4 |
| Math-Shepherd-7B + | 13.3 | 52.5 | 74.6 | 38.5 | 36.5 | 41.2 | 42.8 |
| Math-PSA-7B + | 6.7 | 57.5 | 79.8 | 42.5 | 41.0 | 39.3 | 44.5 |
| RLHFlow-Mistral-8B + | 10.0 | 57.5 | 73.4 | 37.5 | 38.0 | 41.2 | 42.9 |
| Search Configuration | Beams ( ) | PRM Fwd Passes | GFLOPs/Query | Rel. Wall-clock | MATH Acc. |
|---|---|---|---|---|---|
| Monolithic PRM Baseline | 8 | 1.00x | 450 | 1.00x | 81.0% |
| NS-PRM (Verifier + CSP-PRM) | 8 | 0.72x | 324 | 0.78x | 82.6% |
| NS-PRM (Near-Iso-Compute) | 11 | 0.99x | 446 | 1.04x | 83.8% |
| Monolithic PRM Baseline | 16 | 2.00x | 900 | 1.95x | 82.3% |
| NS-PRM (Verifier + CSP-PRM) | 16 | 1.44x | 648 | 1.50x | 84.2% |
| NS-PRM (Near-Iso-Compute) | 22 | 1.98x | 891 | 2.05x | 85.6% |
Appendix figures & tables3 assets
Supplementary material from the paper’s appendix.
Appendix
| Logical Category | Primitive Name | Deterministic Verification Mechanism |
| Proof State & | define_variable | Registers a variable, its value, and physical unit into the verifiable state dictionary. |
| Initialization | declare_target | Registers the final goal variable to evaluate proof completion. |
| assume_premise | Injects a hypothetical condition into the current search branch. | |
| branch_cases | Splits the search tree into bounded, mutually exclusive state copies (e.g., roots). | |
| Equivalence & | equate_expressions | Uses CAS to verify . |
| Substitution | substitute_identity | Verifies variable exists in history, checks unit match, and replaces in target expression. |
| Domain | Supported Primitives |
|---|---|
| Arithmetic & Number Theory (22) | add , subtract , multiply , divide , modulo , power , square_root , nth_root , abs , exp , ln , log_base , gcd , lcm , floor , ceil , is_prime , prime_factors , calc_percentage , calc_ratio , base_conversion , scientific_notation_eval |
| Algebra & Polynomials (18) | solve_linear , solve_quadratic , solve_cubic , solve_system_2d , solve_system_3d , poly_roots , poly_eval , poly_add , poly_multiply , poly_divide , partial_fractions , binomial_expansion , matrix_add , matrix_mult , matrix_det , matrix_inv , eigenvalues , vector_dot_product |
| Geometry & Trigonometry (22) | calc_distance , calc_midpoint , calc_slope , calc_area_2d , calc_volume_3d , calc_surface_area , calc_perimeter , pythagorean_eval , sin , cos , tan , arcsin , arccos , arctan , sinh , cosh , tanh , law_of_sines , law_of_cosines , degrees_to_radians , vector_mag , cross_product |
| Calculus & Sequences (14) | derive_1st , derive_2nd , integrate_def , integrate_indef , limit_eval , taylor_series_expansion , arithmetic_progression_sum , geometric_progression_sum , infinite_series_sum , calc_gradient , divergence , curl , solve_ode_1st_order , solve_ode_2nd_order |
| Combinatorics & Statistics (12) | factorial , nCr (combinations), nPr (permutations), calc_probability , expected_value , variance , std_dev , median , mean , mode , covariance , normal_dist_cdf |
| SciBench Physics: Mechanics & Waves (20) | calc_velocity , calc_acceleration , newtons_second_law , calc_momentum , conservation_of_momentum , calc_kinetic_energy , calc_potential_energy , conservation_of_energy , calc_work , calc_power , calc_torque , calc_angular_velocity , calc_centripetal_force , calc_friction , hookes_law_spring , kinematics_eq_1 , kinematics_eq_2 , kinematics_eq_3 , wave_speed_eq , snells_law |
| Dataset | Abstention Rate | Standard PRM800K | Ours (Dynamic Fallback) |
|---|---|---|---|
| MATH500 (Algebra/Calc) | 4.2% | 85.1% | 89.6% |
| MATH500 (Geometry) | 38.5% | 68.3% | 71.5% |
| AIME 2024 | 26.1% | 26.7% | 33.3% |
Scientific Reasoning in Language Models
Scientific reasoning in language models studies how AI systems use evidence, domain knowledge, and tools to solve problems and support discovery.
See all 144 papers