Can symbolic solvers fix how LLMs reason about logic?

LLMs are strong at understanding natural language and formulating problems in context; they are unreliable at executing precise multi-step logical inference. Natural language reasoning approaches (CoT and variants) inherit the flexibility of NL but also its ambiguity and the LLM's tendency toward hallucination and error propagation. Symbolic solvers are precise and deterministic but require symbolic formulations that NL problems don't naturally provide.

Logic-LM bridges this by dividing the cognitive labor according to each system's strengths:

1. LLM as formulator: Uses in-context learning to translate natural language problems into symbolic representations
2. Symbolic solver as executor: Performs deterministic inference on the symbolic formulation — precise, interpretable, verifiable
3. Self-refinement loop: When the symbolic solver returns an error message, the LLM uses that error to revise the symbolic formulation

The self-refinement loop is architecturally important: it creates a structured feedback signal that is qualitatively different from LLM self-critique. Error messages from a symbolic solver are machine-verifiable and specific — "variable X is unbound," "formula is inconsistent." LLM self-critique on natural language is vague and susceptible to the same hallucination errors as the original generation.

This is an architectural response to Can large language models translate natural language to logic faithfully?. That note establishes the failure; Logic-LM partially addresses it by not requiring perfect formalization — errors are caught and corrected by the solver's feedback loop rather than passed silently to the output.

The trade-off: flexibility requires good NL-to-symbolic translation, which remains an LLM weak point. The self-refinement loop mitigates but doesn't eliminate translation errors. Logic-LM is an improvement, not a solution — it works well for tasks where symbolic formulation is tractable and ill-defined for open-ended reasoning.

The LLM-Modulo framework generalizes this to planning. Kambhampati's LLM-Modulo extends the generate-test-critique pattern to a full architecture: LLMs generate candidate plans, a bank of hard critics (model-based, sound) and soft critics (possibly LLM-based, for style) evaluate them, and a Backprompt Controller pools critiques and diversifies prompts for the next generation attempt. LLMs play multiple roles — guessing candidates, translating formats, helping users flesh out specifications, helping experts acquire domain models — but are never ascribed planning or verification abilities. "Plans coming out of such a compound system will constitute a better corpus of synthetic data for any fine tuning phase." The architecture parallels Logic-LM but at a higher level of abstraction: where Logic-LM offloads logical execution, LLM-Modulo offloads plan verification to external critics that provide formal soundness guarantees. See Can large language models actually create executable plans?.