Turn everyday sentences into formal logic and a machine can verify the math, yet still check a claim the original never made.
Can natural language to formal logic translation ever be fully trustworthy?
This explores whether turning everyday language into formal logic (the step that lets a computer prove or check things) can ever be reliable enough to trust, or whether something is always lost or mistranslated along the way.
This explores whether turning everyday language into formal logic can ever be reliable enough to trust. The short answer from the corpus: probably not fully, but the reasons why matter more than the verdict. The biggest problem isn't broken logic. LLMs reliably produce logic that is well-formed and runs, yet often says something different from the original sentence Can large language models translate natural language to logic faithfully?. The errors cluster in predictable places: which words a 'not' or 'every' applies to, how precise a quantifier is ('most' vs. 'all'), and how finely a concept gets split into predicates. A logic checker will happily verify that wrong translation, so a formal proof can give you false confidence. The math checks out, but it's checking the wrong claim.
The root of the problem sits before any logic gets written. Translating faithfully means first noticing that a sentence could mean two things, and models are poor at that: GPT-4 correctly untangled only about a third of deliberately ambiguous sentences, against roughly 90% for humans Can language models recognize when text is deliberately ambiguous?. Formal logic forces you to choose one reading. A translator that can't see there was a choice will make it silently. This links to a deeper finding: LLMs seem to reason through meaning and association rather than by manipulating symbols, and their performance collapses when the familiar meaning is stripped away, even with the correct rules in front of them Do large language models reason symbolically or semantically?. In other words, the tool you're asking to produce clean symbols is not itself a symbolic thinker.
There's also a scale problem people tend to miss. Translating one sentence on its own looks like it works mostly because it quietly relies on huge prebuilt libraries of definitions (like Lean's Mathlib) Can autoformalization work on individual statements alone?. Real formalization means building a whole consistent web of definitions and supporting facts. Trustworthiness is a property of that whole web, not of any single translated line. A theoretical ceiling applies too: any computable LLM will hallucinate on infinitely many inputs, so outside safeguards are required, not optional Can any computable LLM truly avoid hallucinating?.
The more hopeful work changes the question from 'can translation be perfect?' to 'how should trust be divided up?' One approach generates formal verifiers (including provably correct Lean and z3 checkers) straight from written policy documents Can we automatically generate formal verifiers from policy text?. That moves the trust question to one inspectable artifact a human can review once, rather than every individual translation. Another keeps the formal model in charge of the reasoning and limits the LLM to translating in and out Can separating causal models from language models improve reasoning?. The most counterintuitive result: going only part of the way often works better. Adding selected symbolic structure to natural language beats both plain language and full formalization by 4–8%, because full formalization throws away meaning the logic has no room for Why does partial formalization outperform full symbolic logic?. Lighter-weight structure helps in a similar way. Prompting models to state the hidden assumptions in an argument catches gaps that ordinary step-by-step reasoning skips over Can structured argument prompts make LLM reasoning more rigorous?.
So 'fully trustworthy' is probably the wrong goal. The corpus suggests the weak point is always the bridge between meaning and symbols. Formal methods can guarantee everything downstream of that bridge and nothing upstream of it. The practical skill is knowing where the bridge sits in your system and putting human attention there.
Sources 9 notes
LLMs generate well-formed logical expressions that are semantically incorrect, with errors clustering at scope ambiguity, quantifier precision, and predicate granularity. The asymmetry suggests LLMs understand formal language better than they can generate it.
AMBIENT benchmark shows GPT-4 correctly disambiguates only 32% of cases versus 90% for humans. This failure spans lexical, structural, and scope ambiguity—revealing that LLMs cannot hold multiple interpretations simultaneously, a fundamental gap hidden by standard benchmarks.
When semantic content is decoupled from reasoning tasks, LLM performance collapses even with correct rules in context. Models rely on parametric commonsense and token associations rather than formal logical manipulation, constraining reasoning to training distribution semantics.
Real formalization requires theory-level work: even one theorem needs a coherent web of axioms, definitions, and lemmas. Statement-level approaches only succeed by borrowing from prebuilt libraries like Mathlib, hiding the actual complexity involved.
Three formal theorems prove that any computable LLM must hallucinate on infinitely many inputs, and internal mechanisms like self-correction cannot eliminate this mathematical constraint. External safeguards are therefore necessary, not optional.
Show all 9 sources
interwhen automatically generates code-based verifiers—including provably correct Lean and z3 checkers—from prose policy documents. This inverts the usual neuro-symbolic division: the LLM both translates policy to formal logic and extracts verifier inputs from reasoning traces.
Causal Reflection separates causal reasoning into a formal dynamic model with a Reflect mechanism for revision, relegating the LLM to structured inference and language rendering. This architecture sidesteps asking LLMs to perform causal reasoning directly, addressing both spurious-correlation failures and RL's explanation gap.
QuaSAR and Logic-of-Thought both achieve 4-8% accuracy gains by enriching natural language with selective symbolic elements rather than replacing it. Full formalization loses semantic information; pure language lacks structure. Augmentation preserves both.
Applying Toulmin's argument model as explicit prompting steps (CQoT) improves LLM reasoning by forcing models to identify warrants and backing rather than skipping implicit premises. The method catches failures that standard chain-of-thought prompting allows.
Papers this line draws on 8
The research behind the notes this line reads — ranked by how closely each paper relates.
- Probing Structured Semantics Understanding and Generation of Language Models via Question Answering
- Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning
- Beyond Accuracy: Evaluating the Reasoning Behavior of Large Language Models -- A Survey
- Large Language Models are In-Context Semantic Reasoners rather than Symbolic Reasoners
- Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations
- Large Language Models as Planning Domain Generators
- Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases
- GSM-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models