Technical Summary: SymboUQ

Problem Statement

Large Language Models (LLMs) often generate fluent reasoning traces for spatial reasoning tasks, yet the intermediate relational steps may fail to support the final conclusion. A single incorrect directional or containment relation can corrupt the inferred spatial configuration while leaving the explanation seemingly coherent. Existing uncertainty quantification (UQ) methods rely on token-level statistics, semantic agreement, or internal representations, which may correlate with correctness without directly evaluating spatial semantics. Conversely, formal verifiers provide stronger semantic evidence but suffer from partial applicability: a claim may be successfully parsed into a formal language (symbolizable) yet yield an "unknown" or "not-evaluable" outcome due to insufficient premises or context inconsistencies. Consequently, parse coverage alone is an insufficient proxy for the amount of usable evidence a verifier provides.

Methodology: SymboUQ

The authors propose SymboUQ, a symbolic uncertainty quantification framework that estimates final-answer reliability by distinguishing between symbolizability (whether a claim can be translated into the verifier's formal language) and semantic determinacy (whether executing that claim yields a definite entailment or contradiction verdict). The framework consists of three core components:

1. Layout Auditor

The Layout Auditor executes ordered spatial claims sequentially against a trusted scene description.

• Constraint Generation: It maps natural language statements into a canonical relation system (triples of subject, relation, object) covering direction, containment, distance, and topology.
• Execution & Verdicts: It maintains an active context (the trusted scene plus preceding symbolizable claims) and evaluates each claim $c_k$ against this context. Claims receive one of four statuses:
  • Entailed ($en$): The claim follows from the active context.
  • Contradicted ($co$): The claim conflicts with the active context.
  • Unknown ($un$): The claim is symbolizable but the context lacks sufficient information to resolve it.
  • Not Evaluable ($no$): The active context is already infeasible (due to prior contradictions), preventing further evaluation.
• Evidence Extraction: The auditor extracts features related to feasibility, conflict detection, and bounded repair costs (removing generated relations to restore feasibility while keeping the trusted scene fixed).

2. Determinacy Profile

This module generates a label-free profile $\phi(r)$ characterizing the "effective executable coverage" of a reasoning trace, independent of verdict polarity.

• Symbolizability ($\pi(r)$): The fraction of claims that can be parsed into the formal language.
• Unknown Rate ($\nu(r)$): The fraction of parsed claims that remain unresolved (unknown).
• Semantic Determinacy ($d(r)$): The fraction of parsed claims that receive a definite verdict ($en$ or $co$) under a feasible context. Crucially, claims marked "not evaluable" reduce determinacy, as they represent a loss of usable evidence.
• Verifier Applicability ($\delta(r)$): Defined as $\pi(r) \times d(r)$, representing the fraction of all claims that are both symbolizable and semantically determinate.

3. Determinacy-Aware Reliability Composer (DARC)

DARC integrates heterogeneous reliability signals (constraint-based, representation-based, and decoding-based) conditioned on the trace's applicability profile.

• Candidate Bank: It utilizes a bank of pre-trained or training-free estimators (e.g., token entropy, neural probes, constraint solvers).
• Target Adaptation: Using a labeled validation split from the target domain, DARC screens candidates (removing near-random scores) and orients them (flipping scores if the AUROC is $<0.5$).
• Applicability-Conditioned Composition: DARC constructs feature vectors that interact candidate scores with the determinacy profile. Specifically, it uses interaction terms like $\delta(r) \cdot s_j(r)$ to modulate the contribution of constraint-based evidence based on semantic determinacy. This allows the model to down-weight symbolic evidence when determinacy is low while preserving raw scores from neural/decoding sources. The final reliability score $p(r)$ is computed via a logistic function with $\ell_2$ regularization.

Key Contributions

1. Conceptual Distinction: The work distinguishes textual symbolizability from semantic determinacy, providing a principled basis for determining when verifier-derived evidence is informative. It argues that parse coverage alone is insufficient because it does not account for unresolved or blocked claims.
2. Technical Framework: SymboUQ introduces a three-stage pipeline (Layout Auditor, Determinacy Profile, DARC) that explicitly handles the "unknown" and "not-evaluable" regimes of formal verification, integrating them with neural signals.
3. Empirical Performance: The framework demonstrates consistent improvements over strong baselines across diverse spatial reasoning benchmarks and LLM backbones.

Experimental Results

The authors evaluated SymboUQ on five spatial reasoning benchmarks (StepGame, SpaRTQA, SpaRTUN, SpaceNLI, SpaRP) using four frozen LLM backbones (Mistral-7B, Llama-3.1-8B, Gemma-2-9B, Qwen3-8B).

• Performance: SymboUQ achieved the strongest overall performance in trace ranking (AUROC) and probability estimation (class-balanced Brier loss). It showed an average 8% relative improvement in AUROC and a 7% relative reduction in class-balanced Brier loss compared to the strongest external baseline.
• Ablation Studies:
  • Applicability Awareness: Removing the determinacy-aware interactions (using only score stacking) resulted in a performance drop of 0.032–0.052 AUROC, confirming that conditioning on applicability is critical.
  • Determinacy vs. Parse Coverage: Analysis showed that constraint-score separation increases monotonically with semantic determinacy but not with parse coverage, validating that determinacy is a better characterizer of verifier utility.
  • Context Semantics: Using an "assumed context" (allowing unverified hypotheses) rather than a strictly "grounded context" provided significant gains, as it allows the system to detect self-contradictions within the generated chain.
• Efficiency: The method is computationally efficient, processing approximately 159 traces per second with a small number of trainable parameters (8.13M) and requiring only a short training time (9 minutes) on the target validation split.

Significance

The paper claims that SymboUQ addresses a critical gap in LLM reliability estimation: the disconnect between the ability to parse a claim and the ability to semantically resolve it. By treating "unknown" and "not-evaluable" outcomes as distinct from "contradicted" and explicitly modeling the loss of evidence due to context infeasibility, the framework provides a more faithful measure of verifier applicability. The results suggest that for spatial reasoning, reliability estimation benefits significantly from integrating formal verification signals with neural signals, provided the integration is conditioned on the trace's semantic determinacy rather than merely its parseability. The work establishes that symbolic uncertainty quantification can be effectively applied to free-form reasoning traces without requiring ground-truth labels for intermediate steps during the auditing process.