Resource-Aware Neuro-Symbolic Reasoning for Local Small Language Models

Technical Summary: Resource-Aware Neuro-Symbolic Reasoning for Local Small Language Models

Problem Statement
Small Language Models (SLMs) offer the advantages of local execution, including privacy, offline availability, and reduced operational costs. However, their limited capacity often necessitates strategies like repeated sampling (self-consistency) to achieve reliable reasoning, which multiplies local model calls, token generation, and serial latency. While neuro-symbolic approaches exist, they often assume general theorem-proving capabilities or ignore the specific resource constraints of consumer hardware. The central problem addressed is whether a bounded, verifiable neuro-symbolic pipeline can replace repeated local neural sampling for structured reasoning tasks without sacrificing accuracy, specifically within the constraints of local SLMs.

Methodology: The VFR-LLM Pipeline
The authors propose the Verifiable Formalization and Repair (VFR-LLM) pipeline, a five-stage architecture designed to offload reasoning from the neural model to a deterministic solver:

1. Formalization: The SLM translates a natural language problem into a typed finite-domain rule-and-constraint representation. This intermediate language includes grounded facts, safe Horn-style rules, and finite-domain constraints (e.g., ordering, absolute positions). Crucially, the model must provide source spans linking every extracted constraint to the original text.
2. Coverage Checking: A verification layer inspects the formalization to ensure every constraint is grounded in the source text and that no unsupported rules or unknown entities exist.
3. Solver Execution: A deterministic solver (an exact enumerative solver for the evaluated tasks) processes the formalized program to find a satisfying assignment (e.g., a total ordering of entities).
4. Repair: If the solver fails or diagnostics indicate formalization errors (e.g., inverted arguments or syntax issues), a deterministic repair module applies local edits based only on source spans and solver diagnostics. No additional model calls or gold answers are used during this step.
5. Answer Generation: The final answer is derived from the solver's output, linked back to the verified constraints.

The target formalism is intentionally modest: a Datalog-like language with finite domains, excluding function symbols and unbounded quantification to ensure the translation burden remains manageable for small models.

Key Contributions

1. Traceable Representation: Definition of a typed, finite-domain rule-and-constraint formalism that requires source spans for every extracted fact, enabling auditability of the translation step.
2. Verification and Repair Loop: Implementation of a pipeline that uses source-grounded validation and deterministic repair to identify and correct formalization failures before solver execution, rather than relying on repeated sampling.
3. Local Evaluation Matrix: A comprehensive evaluation using LM Studio on Apple Silicon (M3 Pro) with three model families: Qwen3-4B, Microsoft Phi-4-mini-reasoning, and Gemma-3n-E4B. The benchmarks include generated pure-precedence tasks, generated typed-precedence tasks, and two subsets derived from BIG-Bench Hard (BBH) Logical Deduction (pairwise and extended).
4. Resource-Aware Comparison: A rigorous comparison against serial self-consistency ($k=5$) and a cost-aware adaptive self-consistency baseline, measuring accuracy, model calls, total tokens, and serial latency.

Results
The empirical results reveal a bounded and model-dependent efficacy for the VFR-LLM approach:

• Qwen3-4B Performance:

  • Pure Precedence: Achieved 0.983 accuracy with one model call, significantly outperforming serial self-consistency (0.700 accuracy, 5 calls) and reducing total tokens by 34.4%.
  • BBH-Extended (Public Source): Achieved 0.933 accuracy versus 0.283 for self-consistency and 0.317 for direct answering. While total tokens increased slightly due to the length of the formalization, the method reduced model calls (1 vs. 5) and serial latency (11.32s vs. 16.54s).
  • Typed Constraints: Performance was "blocked" by direct answering, which remained more accurate and cheaper in these specific strata.

• Gemma-3n-E4B Performance:

  • Showed strong improvements on pure-precedence tasks (0.683 vs. 0.367 for self-consistency).
  • Results on BBH-extended tasks were marginal (0.375 vs. 0.350 for direct answering), with the accuracy gain not being statistically significant.
  • Typed constraints showed mixed results, with latency often higher than direct answering.

• Phi-4-mini-reasoning:

  • Demonstrated severe formalization failures on typed constraints, resulting in negative outcomes compared to direct answering.

• Robustness Checks:

  • Adaptive Baseline: Even when compared against a cost-aware adaptive self-consistency baseline (which reduces calls from 5 to ~4.2), VFR-LLM maintained a significant accuracy advantage on precedence and BBH-extended tasks for Qwen.
  • Traceability: High accuracy correlated strongly with high "fully traceable" rates (source-grounded constraints). Qwen achieved a 0.942 traceable rate on BBH-extended, while Gemma achieved only 0.292, explaining the performance gap.
  • Deterministic Ablations: The typed finite-domain solver solved 100% of the BBH-extended instances, whereas a precedence-only solver solved only 20.8%, confirming the necessity of the extended formalism for these tasks.

Significance and Claims
The paper explicitly avoids claiming that symbolic reasoning universally improves local LLM performance or reduces compute for all tasks. Instead, it establishes a bounded claim:

1. Conditional Resource Reduction: VFR-LLM is a viable, resource-aware alternative to serial self-consistency for structured tasks with explicit constraints (specifically ordering and finite-domain logic) where direct answering is insufficiently accurate.
2. Model Dependency: The success of the pipeline is heavily dependent on the SLM's ability to produce faithful, source-grounded formalizations. The method works well for Qwen on specific strata but fails or offers only marginal gains for Phi and Gemma in more complex typed scenarios.
3. Auditability: The primary contribution is not just accuracy, but the ability to provide an auditable reasoning trace and diagnose failures (e.g., distinguishing translation errors from solver failures) without the overhead of repeated neural generation.
4. No General Compute Reduction: The paper concludes that adding a symbolic layer does not automatically lower compute costs; in many cases (e.g., typed tasks with Qwen), direct answering remains the most efficient and accurate option. The method is best viewed as a diagnostic tool and a specialized alternative to repeated sampling for specific, bounded problem classes.