Beyond Executability: Schema-Adaptive Alignment for Faithful Natural-Language-to-Symbolic Reasoning

Formalize-then-solve pipelines improve LLM reasoning by translating natural-language problems into symbolic artifacts and delegating inference to external solvers. However, we identify a hidden reliability gap: a generated artifact may be syntactically executable while still violating the schema-level commitments it declares. We call this failure mode Silent Schema Inconsistency. Such errors are especially dangerous because they do not necessarily trigger parser errors, solver crashes, or execution feedback, leaving execution-driven refinement structurally blind to the underlying semantic mismatch. To address this problem, we propose Schema-Adaptive Constraint Alignment (SACA), an oracle-free, feedback-free, and inference-free pre-execution alignment layer for LLM-generated symbolic artifacts. Instead of asking whether an artifact can run, SACA asks whether it obeys its own declared schema: it detects the artifact schema, extracts a schema-specific constraint closure, and deterministically aligns recoverable violations before solver execution. We instantiate SACA for rule-style and CSP-style artifacts, enabling predicate-declaration completion, predicate-signature alignment, and domain–ordinal normalization. Across ProntoQA, LogicalDeduction, and ProofWriter, SACA improves symbolic reasoning by repairing distinct schema-level inconsistencies while introducing zero additional LLM calls. On LogicalDeduction, SACA improves FARA-CF from 70.0% to 91.0% on the diagnostic subset and improves Logic-LM from 54.7% to 80.7% on the full 300-example development split. Moreover, 7B symbolic-execution systems equipped with SACA outperform a larger 14B prompt-only model on structurally constrained settings, while SACA itself adds less than 0.5 ms of latency per example. These results show that reliable neuro-symbolic reasoning requires not only executable artifacts, but also systematic pre-execution enforcement of the schemas those artifacts declare.