Translate-Then-Prove: Logic-LM and LINC

📍 Where we are: Part VI · Natural-Language Reasoning — Chapter 20. Soft Reasoners built the measuring instrument and watched a statistical reader collapse to chance beyond its trained depths; this chapter takes the opposite route through the same instrument: translate the English into logic once, then let a prover that is sound by theorem do every inference step.

The soft reasoner of the last chapter was a monolith: English in, verdict out, every step in between statistical. When it failed at depth 2, nothing inside it could say which part had failed, because there were no parts. This chapter studies the architecture that creates the parts on purpose. A translate-then-prove pipeline splits the task at its one natural joint: a translator maps the English into a formal program, and a symbolic engine derives the answer from that program. Every property a neural network cannot certify (soundness, completeness, termination) is thereby concentrated in a component that has them by theorem, and every property language understanding cannot guarantee is concentrated in the translator, where it can at least be measured, repaired, or refused. Two published systems, Logic-LM and LINC (Logical Inference via Neurosymbolic Computation), realize this architecture with a large language model (LLM) as the translator, and they differ exactly at the failure joint: what to do when the translation does not go through. The companion module translate_prove.py rebuilds both answers at desk scale, on the very evaluation set the soft reasoner was scored on.

The simple version

Imagine a court whose judge is flawless but reads only Latin. You file your case in English, and a clerk translates it. If the clerk's Latin says what your English said, the ruling is guaranteed correct, so the court's entire error budget lives at the clerk's desk. Every case ends one of three ways: the clerk translates and the judge rules (correct, always); the clerk stumbles on a word and the court refuses the case rather than guess; or, worst, the clerk produces fluent Latin that quietly says something different, and the judge rules impeccably on the wrong case. Two remedies exist for the stumbles. One court sends the filing back with a note pinned to the offending word and lets the clerk retry: Logic-LM's repair loop. Another hires ten clerks, discards the translations that fail to parse, and rules on the majority of the rest: LINC's vote. Neither remedy can touch the third, quiet failure, and holding onto that fact is half of this chapter.

What this chapter covers

• The factorized architecture: translator → formal program → engine → verdict, the engine's soundness, completeness, and termination recalled from Volume 1, and the correctness factorization $P(\text{correct}) = P(\text{parse}) \times 1$ derived event by event (a lower bound in general, an equality here).
• The translator, quoted: the deterministic grammar over controlled English in translate_prove.py, and why a fixed closed grammar purchases a 100-percent-on-parsed guarantee a sampled LLM translation cannot give.
• The committed factorization exhibit: coverage, accuracy-on-parsed (exactly 1.0000, asserted), and overall accuracy per depth, beside the soft reasoner's columns on the identical 1,500 questions, with the crossover read honestly both ways.
• Self-refinement in miniature: the synonym-normalization repair pass and its committed coverage lift 0.8080 → 0.9293, next to the real system's error-message loop, its reported executable-rate lifts, and the honest limit that repair fixes syntax, rarely semantics.
• Abstention as an interface contract: LINC's error-filtered majority vote decoded, the companion's committed no-silent-errors assert, and a three-way failure-mode contrast table.
• The solver menu at real scale: logic programming, first-order provers, and SMT (satisfiability modulo theories) matched to benchmarks by the semantics of their labels, with the three-way True/False/Uncertain protocol named for the next chapter.
• The published headline contrast: where the pipeline dominates chain-of-thought and where it regresses, both quoted, both explained by the same factorization.
• The unsolved part: semantic translation errors are invisible to repair and voting alike, because nothing in the pipeline checks that the formula means the sentence.

The pipeline, factorized at the joint

The published architecture has three stages: problem formulation (a language model, prompted with a few worked examples, translates the English context and question into a program in a solver's formal syntax), symbolic reasoning (a deterministic solver executes the program), and result interpretation (the solver's verdict is mapped back to the answer label) [1]. LINC instantiates the same skeleton with first-order logic as the target language and a resolution prover as the engine [2]. In both, the language model performs no inference: its entire job is representation, and the multi-step deduction happens inside the solver. The companion pipeline fills each slot with something already on your desk: the translator is a deterministic grammar (next section), and the engine is Volume 1's backward chainer sld.provable, run on the ground program produced by ruletaker_lite.ground_program, the stratified closed-world compiler the previous chapter built (translate_prove.py lines 200–208):

def prove_statement(theory: dict, person: str, pred: str, neg: bool) -> bool:
    """The symbolic stage, exactly as the docstring factors it: compile the
    parsed theory with ruletaker_lite.ground_program (the stratified
    closed-world compiler resolves negation-as-failure against the stated
    facts), then ask Volume 1's BACKWARD chainer.  A positive question is
    True iff provable; a negated question is its closed-world complement."""
    facts, rules = rt.ground_program(theory)
    provable = sld.provable(("is", person, pred), sorted(facts), rules)
    return (not provable) if neg else provable

Three sentences recall why this engine can be trusted outright, each carrying a Volume 1 theorem. It is sound: every SLD (Selective Linear Definite-clause) derivation is a chain of resolution steps, each preserving truth in every model, so a found proof can never assert a falsehood (Resolution and SLD). It is complete on these programs: if a ground atom follows from a function-free definite program, SLD resolution finds a refutation, so "no proof found" genuinely means "not entailed", which the closed-world evaluation then reads as False (Inference and Proof). And it terminates here for the well-founded-descent reason Volume 1 made precise: every rule's body predicates sit in a strictly lower layer of the corpus vocabulary than its head, so the recursion has a measure that decreases at every call and the search cannot loop (Fixpoints gives the forward version; the layer index plays the role the acyclic citation chain played in Volume 1).

Now the factorization. Fix a question drawn from the evaluation distribution, and define three events. Let $A$ be the parse event: every sentence of the context and the question itself is accepted by the translator. Let $B$ be the faithfulness event: given a parse, the formal program means what the English meant. Let $C$ be the engine event: given a faithful program, the engine's verdict equals the program's semantic consequence. When all three happen, the pipeline answers correctly. Read $P(A)$ as the probability of the event $A$, and $P(B \mid A)$, the vertical bar pronounced "given", as the probability that $B$ happens given that $A$ already has. How probable is the route where all three happen? By the definition of conditional probability, $P(B \mid A) = P(A \text{ and } B)/P(A)$, so multiplying both sides by $P(A)$ gives $P(A \text{ and } B) = P(A)\cdot P(B \mid A)$; applying the same definition once more, this time to the joint event ($A$ and $B$) paired with $C$, gives $P(A \text{ and } B \text{ and } C) = P(A \text{ and } B)\cdot P(C \mid A, B) = P(A)\cdot P(B \mid A)\cdot P(C \mid A, B)$. That identity is the chain rule of probability (each factor conditions on the events before it), and it says the correct-via-all-three route contributes exactly $P(A)\cdot P(B \mid A)\cdot P(C \mid A, B)$ to the accuracy. In general this is a lower bound, not an equality:

$$P(\text{correct}) \;\ge\; P(A)\;\cdot\;P(B \mid A)\;\cdot\;P(C \mid A, B),$$

because further routes to a correct answer exist. The main one: an unfaithful program (event $A$ without event $B$) still parses and executes, and its verdict can match the gold label by pure coincidence. (In full generality there is a second extra route, a faithful program whose engine errs, event $\lnot C$ (read: not $C$, the engine event failing), yet lands on the gold label by luck; it vanishes here the moment $P(C \mid A, B) = 1$ is established below.) On a binary-label benchmark that coincidence term is generically nonzero: roughly half of the wrong-meaning programs land on the right label anyway. Equality holds when the coincidence route is empty, in particular when $P(\lnot B \mid A) = 0$, where $\lnot B$ (read: not $B$) is the event that the parse succeeded but faithfulness failed.

The paragraph above establishes $P(C \mid A, B) = 1$: soundness and completeness make the verdict equal entailment, termination makes the verdict exist, and the closed-world complement handles the negated questions. That is not an aspiration; it is the theorem-backed factor. So the bound becomes

$$P(\text{correct}) \;\ge\; P(A)\cdot P(B \mid A),$$

and the entire engineering question becomes the two remaining factors: coverage ($P(A)$, how much of the language the translator accepts) and faithfulness ($P(B \mid A)$, whether what it accepts, it renders truly). For the companion's translator the second factor is exactly $1$, for a reason the next section makes precise: the grammar's fixed one-reading-per-production design makes the faithfulness event sure (determinism guarantees only that the same input gets the same reading; that the reading is the meaning is what the closed grammar adds), so $P(\lnot B \mid A) = 0$ and the coincidence route is empty; and since a parse failure ends in an abstention that the scoring below counts as wrong, no correct answer can arrive through $\lnot A$ either, so the inequality closes to the equality the thesis promised:

$$P(\text{correct}) \;=\; P(\text{parse}) \times 1 .$$

Once the engine is trusted, end-to-end accuracy is parse accuracy. Contrast the soft reasoner: one undifferentiated function from text to label, no event to condition on, no factor equal to $1$ by theorem, no component certifiable separately. Its 0.9659 at depth 1 and its 0.5000 at depth 3 are facts about the whole, explainable only by more measurement. The pipeline's errors, by construction, all live in one place, and the committed numbers below show them living there.

The architecture factorized at its joint: the translator is the only fallible stage, the engine's factor is pinned to 1 by Volume 1's theorems, and the two published remedies (repair, abstain) act only on the parse factor. Original diagram by the authors, created with AI assistance.

The translator, quoted: a grammar instead of a guess

The companion's translator is a deterministic grammar over the controlled English the corpus generator emits, with closed lexicons for the people and the predicates; its entire specification fits in a comment (translate_prove.py lines 89–94):

# The parse table.  Three sentence forms, each anchored on closed lexicons:
#   fact/question:  "<person> is [not] <predicate>."
#   rule:           "If someone is <cond> [and <cond>]* then they are <pred>."
#                    with <cond> = "[not] <predicate>"
# Anything else — one unknown token suffices — is a ParseError, never a
# guess.  Same input, same parse, every time: the determinism is the point.

The statement parser is the grammar's first row as executable code (translate_prove.py lines 131–145): split on spaces, demand is in second position, strip an optional not, check both open slots against the frozen lexicons PERSONS and PREDS, built from the corpus module's name and predicate lists (translate_prove.py lines 96–97):

def parse_statement(sentence: str) -> tuple[str, str, bool]:
    """'<person> is [not] <predicate>.' -> (person, predicate, negated).
    Raises ParseError (with the offending token) on anything else."""
    toks = _tokens(sentence)
    if len(toks) < 3 or toks[1] != "is":
        raise ParseError(f"not a statement shape: {sentence!r}")
    person, rest = toks[0], toks[2:]
    neg = rest[0] == "not"
    if neg:
        rest = rest[1:]
    if person not in PERSONS:
        raise ParseError(f"unknown person {person!r}")
    if len(rest) != 1 or rest[0] not in PREDS:
        raise ParseError(f"unknown predicate {' '.join(rest)!r}")
    return person, rest[0], neg

parse_rule does the same for the rule template, and parse_theory maps a whole context, facts first, rules after (lines 148–185). Two design properties do all the load-bearing work. First, the translator is total in its verdicts: every input either parses or raises ParseError naming what it could not place (the offending token, or the malformed shape); there is no middle state. Second, it is deterministic and compositional: the same input always yields the same parse, and each grammar production has exactly one formal reading, fixed once in the code. Faithfulness, the factor $P(B \mid A)$ of the previous section, is therefore $1$ by construction: a sentence that parses is rendered by the one reading its production carries, and that reading was written to be the sentence's meaning.

This is precisely the guarantee a language-model translator cannot give, and the distinction deserves a careful sentence rather than a slogan. An LLM's translation is a sample from a learned distribution over programs conditioned on the text: even at temperature zero (the sampling temperature is the knob that widens or narrows the model's output distribution; at zero it is at its narrowest, and the model always picks its single highest-probability token) it is a greedy draw from that distribution (the per-token argmax, that is, the highest-probability token at each step, which is not even guaranteed to yield the program the distribution as a whole rates most probable, its mode), not a grammar's unique reading, and nothing ties the sampled program's semantics to the sentence's. For the LLM pipeline, $P(B \mid A)$ is an empirical quantity strictly below $1$: a program can be well-formed, executable, and wrong about what the English said. The honest bridge between this chapter's toy and the real systems is exactly here: our grammar makes $P(B \mid A) = 1$ visible by making it true, so everything else about the architecture (factorization, repair, abstention, crossover) can be studied in committed numbers; the real systems inherit the same algebra with a semantic-error term that does not vanish [1].

Here is the whole pipeline running once on the committed corpus. The demo picks the first non-negated depth-3 question with gold True, parses it, compiles the context, and hands the goal to the prover; this is the real output of python3 translate_prove.py:

[1] one worked pipeline pass: sentence -> program -> proof -> verdict
    question (as written):   'alice is influential.'
    parsed atom:             is(alice, influential)  negated=False
    SLD proof (Volume 1's backward chainer, on the compiled ground program):
         is(alice, influential)
           is(alice, senior)
             is(alice, visible)
               is(alice, cited)
             is(alice, cited)
    verdict: True   gold: True

Read the proof tree bottom-up: cited is a stated fact, one rule lifts it to visible, another composes visible (with cited again, the rule's second condition) into senior, a third reaches influential. That is depth-3 composition, the exact regime where the soft reasoner sat at 0.5000, executed as three rule applications (five resolution steps, counting the fact lookups) whose soundness is a theorem. The verdict is not a confidence; it is the conclusion of the auditable proof tree sld.prove has returned since Volume 1 (sld.py lines 63–75).

The factorization in committed numbers

A factorization is only worth deriving if it survives contact with data, so the companion makes the evaluation adversarial and measures every factor. The evaluation set is not new: corrupted_corpus imports the previous chapter's committed split directly, so the two architectures are scored on identical ground (translate_prove.py line 240):

    base = rt.run(verbose=False)              # the SAME split, deterministic

Those are the same 20 held-out theories and 1,500 questions on which the soft reasoner posted its per-depth column. On top of them, one seeded corruption: a fraction SYN_FRAC = 0.35 of the question sentences whose predicate has a "street name" are rewritten through a five-entry synonym table the strict grammar does not know (published becomes printed, funded becomes sponsored, productive becomes prolific, cited becomes referenced, senior becomes veteran; lines 112–118). This is the desk-scale stand-in for the gap every real pipeline faces: the world's English is larger than the translator's. In the committed run, 288 of the 1,500 questions are rewritten. Each question then flows through pipeline_answer (lines 211–228), the whole architecture in one screenful:

def pipeline_answer(theory_sentences: list[str], question: str,
                    use_repair: bool) -> bool | None:
    """The whole translate-then-prove pipeline for one question.  Returns
    True/False, or None — the LINC-style Error/abstention — whenever any
    sentence fails the grammar (after the repair round, if enabled).
    Nothing here ever guesses: parse or be silent."""
    try:
        theory = parse_theory(theory_sentences)
        person, pred, neg = parse_statement(question)
    except ParseError:
        if not use_repair:
            return None
        try:
            theory = parse_theory([repair(s) for s in theory_sentences])
            person, pred, neg = parse_statement(repair(question))
        except ParseError:
            return None                      # abstain: visibly, not wrongly
    return prove_statement(theory, person, pred, neg)

The scoring is the harshest available: abstain counts as wrong, earning no partial credit in the overall column, so the pipeline cannot look good by refusing everything hard. Here is the committed per-depth table, repair enabled, beside the soft reasoner's accuracy on the very same questions (the column n counts the evaluation questions at each depth; real output, section [3] of the run):

[3] the per-depth factorization table, beside the soft reasoner (same questions)
      depth   n     coverage   acc-on-parsed   overall   soft reasoner
      0       804   0.9266     1.0000          0.9266    1.0000
      1       352   1.0000     1.0000          1.0000    0.9659
      2       280   0.8321     1.0000          0.8321    0.5000
      3        64   1.0000     1.0000          1.0000    0.5000

The acc-on-parsed column is the factorization made visible: exactly $1.0000$ at every depth, not as a happy accident but as a committed assertion, re-checked on every run before and after repair; the module fails if a single parsed question is ever answered against gold (translate_prove.py lines 298–301):

    for tab in (before, after):
        for d, row in tab.items():
            assert row["acc_on_parsed"] == 1.0, \
                f"pipeline wrong on a parsed depth-{d} question ({row})"

So every number in the overall column is literally coverage × 1.0, and every end-to-end error is a coverage error. Even the table's shape is explained by the synonym lexicon: depth-3 questions ask only about influential, the sole depth-3 predicate, and it has no street name, so their coverage is exactly $1.0000$; depth-1 questions ask about productive or visible, and the only corruptible one, productive (rewritten to prolific), is repairable, so coverage returns to $1.0000$ after repair; depths 0 and 2 keep abstentions because referenced and veteran are the two synonyms the repair lexicon deliberately does not know.

Now read the crossover honestly, both ways. At depth 0 the soft reasoner wins, 1.0000 against 0.9266: these are questions whose answer is read off a stated fact, its training distribution, and it always answers, while the pipeline is silent on every unrepaired synonym. Always-answering beats exact-but-silent wherever the always-answerer's accuracy exceeds the exact system's coverage, the condition $P_{\text{soft}}(\text{correct}) \gt P(\text{parse}) \times 1$ instantiated at depth 0 as $1.0000 \gt 0.9266$. Already at depth 1 the inequality flips, $1.0000$ against $0.9659$, once repair has restored full coverage there; at depths 2 and 3 it reverses violently: $0.8321$ and $1.0000$ against a coin-flip $0.5000$, because composition is the engine's home ground and no amount of always-answering compensates for answering at chance. Weighted by the question counts, the totals come out $0.9293$ for the pipeline against $0.8773$ for the soft reasoner. Neither number dominates at every depth; the architecture question is which failure profile a deployment can live with, and that framing, not a winner declaration, is what the committed table teaches.

Self-refinement in miniature: repair the parse, retry

Logic-LM's defining robustness mechanism attacks the coverage factor directly. When the solver rejects the generated program, the system re-prompts the translator with the erroneous program, the solver's own error message, and demonstrations of common error-to-fix pairs, then retries, up to three rounds in the reported experiments [1]. The loop's effect is measured by the executable rate, the fraction of problems whose program runs at all, and the reported lifts, under the GPT-3.5 backbone, are substantial: on FOLIO, from 66.7 to 84.3 percent; on the ProofWriter subset, from 87.3 to 95.6; on AR-LSAT (the Analytical Reasoning section of the Law School Admission Test), the hardest formalization target, from 11.3 to only 21.8, a reminder that repair cannot conjure coverage that was never close [1].

The companion miniaturizes the loop as one deterministic round: a normalization lexicon mapping known off-grammar synonyms back into the grammar's vocabulary, deliberately partial so the unrepairable remainder stays visible (translate_prove.py lines 103–107 and 188–194):

REPAIR_LEXICON: dict[str, str] = {
    "prolific": "productive",
    "sponsored": "funded",
    "printed": "published",
}

def repair(sentence: str) -> str:
    """The one-round self-refinement pass: normalize every token the repair
    lexicon knows, then hand the sentence back to the SAME strict parser.
    Deterministic, like everything else here (Logic-LM re-prompts an LLM
    with the solver's error message; the shape — error, rewrite, retry — is
    what this keeps)."""
    return " ".join(REPAIR_LEXICON.get(t, t) for t in sentence[:-1].split(" ")) + "."

The shape is the published loop's shape: a failure signal from the symbolic side (here the ParseError naming the offending token, there the solver's error message) flows back to the translation side, which rewrites and resubmits to the same strict checker. The demo shows one repair succeeding and one failing, verbatim:

    the self-refinement round, where the strict grammar fails first:
    question (as written):   'bob is printed.'
    strict parse:            ParseError: unknown predicate 'printed'
    repair pass:             'bob is published.'  -> parses, proves, answers
    question (as written):   'alice is not referenced.'
    strict parse + repair:   ParseError both -> Error (abstain, stay silent)

And the committed before/after coverage table has exactly the shape of the published executable-rate table:

[2] the parse-rate table: coverage before vs after the repair pass
    288 of 1500 eval questions were rewritten through 5 synonyms;
    the repair lexicon knows 3 of them (deliberately partial).
      pass            coverage
      strict only     0.8080
      + repair        0.9293   (strictly higher, asserted; Logic-LM's Table-3 shape)

Both directions of that lift are asserted, not merely printed: the harness requires cov_after > cov_before (repair genuinely recovered something) and cov_after < 1.0 (the unrepairable synonyms did not silently vanish) (translate_prove.py lines 313–316). One honest limit rides along, and the published ablation is explicit about it: refinement driven by solver errors fixes syntax, rarely semantics. The executable rate keeps rising with more rounds, but accuracy quickly plateaus, stagnating after the first round or two in the published ablation, because a program that is semantically wrong yet syntactically fine never triggers the error message that would summon a repair [1]. Our miniature shows the same boundary by construction: repair acts only on sentences the parser has already rejected, so a sentence that parsed into the wrong meaning (impossible here, guaranteed possible for an LLM) would sail past it.

Abstention as an interface contract

LINC's answer to the failure joint is different: do not repair, diversify and filter. The translator samples $K = 10$ candidate translations of the same problem at temperature 0.8 (the sampling-temperature knob decoded in the translator section, here turned up so the ten draws differ); each is handed to the prover; any candidate that fails to parse or crashes the prover is tagged Error and dropped from the vote; the answer is the majority label among the survivors; and if all $K$ candidates error out, the example is scored wrong rather than guessed [2]. Parse failures are treated as what they are, non-answers. The companion's translator is deterministic, so sampling it $K$ times would produce $K$ identical parses; its version of the error filter is the degenerate $K = 1$ case, explicit abstention: an out-of-grammar sentence yields None, the pipeline stays silent, and no fallback answer is manufactured. What elevates this from a behavior to an interface contract is that the companion asserts it question by question (translate_prove.py lines 305–309):

    for q in eval_qs:
        v = pipeline_answer(theories[q["theory"]]["sentences"], q["text"],
                            use_repair=True)
        assert v is None or v == q["gold"], \
            f"a silent wrong answer slipped through on {q['text']!r}"

Every one of the 1,500 questions is re-run and checked: the output is either the gold answer or an abstention, never a silent wrong answer. The run's final table prints the contrast that guarantee buys:

[4] the failure-mode contrast (same evaluation set)
      system                       answers      silent errors      overall acc
      soft reasoner (always)       100.0%       yes (quietly wrong)   0.8773
      translate-then-prove         92.9%        never (asserted)     0.9293

The three designs now line up as three contracts at the same joint, and the failure-mode columns matter more than the accuracy column:

design	on parse failure	can it be silently wrong?	who consumes the failure
soft reasoner (monolith)	no such event exists; it always answers	yes, invisibly and confidently	nobody: the error surfaces only against gold labels
Logic-LM-style (repair, then answer or fall back)	feed the error back, retry up to 3 rounds; if still broken, fall back to a baseline answer	yes, through the fallback and through semantically wrong programs	the translator consumes the error message; the fallback hides the residue [1]
LINC-style (vote or abstain)	drop errored samples from the vote; all-error means no answer, scored wrong	not through parse failures (filtered), but yes through faithful-looking mistranslations	the vote consumes it; the abstention is visible downstream [2]

Note the asymmetry in the middle column: both remedies close the loud failure (the program that will not run) and neither closes the quiet one (the program that runs and lies). That asymmetry is the subject of the unsolved part.

The solver menu at the real scale

At desk scale one engine sufficed. At benchmark scale the engine must be chosen, by one principle: match the engine's semantics to the semantics of the benchmark's labels. Logic-LM is the clearest published exhibit, because it ships a per-dataset solver table rather than one universal logic [1]:

benchmark	label space	formulation	engine
PrOntoQA	True / False	logic program (Horn facts and rules)	Pyke, a logic-programming engine: chaining under closed-world negation
ProofWriter (open-world-assumption, OWA, subset)	Proved / Disproved / Unknown	logic program with an explicit truth-value argument	Pyke; a query that binds no value recovers the Unknown label
FOLIO	True / False / Uncertain	first-order logic	Prover9, a resolution theorem prover: open-world entailment
LogicalDeduction	multiple choice (order a list of objects under positional clues)	constraint satisfaction problem	python-constraint: finite-domain search for satisfying assignments
AR-LSAT	5-way choice	SMT specification	Z3: per-option satisfiability under the constraint set

Read the rows as semantics, not as tooling. A closed-world chaining engine decides provability from what is stated, the right meaning for a corpus whose False literally means "not derivable" (ours, and PrOntoQA's). An open-world prover decides entailment, and its native verdict is three-way: prove the goal and answer True, prove the goal's negation and answer False, prove neither and answer Uncertain. That dual-query protocol is exactly how LINC turns a two-outcome prover into the three-way label space FOLIO and open-world ProofWriter demand [2]; the next chapter treats it as a first-class object. For puzzle benchmarks whose answer is a configuration rather than an entailment, the natural formalism is declarative constraints: SatLM makes that variant the whole method, prompting the model to emit a declarative specification and handing it to an SMT solver, so the translator writes down what must be true and the solver searches for what satisfies it [3]. The architecture space even contains this chapter's pipeline inverted: LAMBADA keeps the control flow symbolic, a backward-chaining loop from the goal, and uses the language model as the inference primitive inside each step [4]. Across the whole menu, one invariant holds: whatever engine fills the slot, its verdict is backed by a guarantee that predates the pipeline by decades, and for the resolution provers in the table it is the original one, the soundness and completeness of the resolution principle itself, the same theorem the backward chainer built on Volume 1's twenty-line unifier inherits [5].

Where the pipeline wins, and where it loses

Read through the factorization, the published headline numbers stop being a scoreboard and become a diagnosis. The pipeline's home ground is deep multi-step deduction over language the translator can cover. On the ProofWriter open-world depth-5 subset, exactly the regime our depth-stratified table isolates, Logic-LM reports 79.66 percent against 68.11 for chain-of-thought (CoT) prompting under the same strongest backbone, and 71.45 against 48.33 under the weaker GPT-3.5 backbone, a gap that widens as required depth grows because the deduction is delegated to an engine that does not degrade with depth [1]. LINC's version is starker: on its balanced open-world ProofWriter subset, the strongest backbone scores 98.3 with the prover against 72.2 with chain-of-thought, and a 15.5-billion-parameter open model with a prover (82.5) beats the strongest backbone reasoning in free text (72.2), the cleanest published statement that representation plus a sound engine can outrun sheer model scale at deduction [2].

The losses are just as instructive, because they are coverage-and-faithfulness losses, not reasoning losses. On FOLIO, whose premises are human-written English rather than templated sentences, the strongest backbone's chain-of-thought (75.3) edges out the same backbone's prover pipeline (72.5), a gap reported as not statistically significant: the language outruns the translator, and the engine's exactness cannot buy back what the translation spent [2]. Logic-LM shows the same inversion on PrOntoQA, where the strongest backbone's chain-of-thought already reaches 98.79 and forcing a formalization step loses fifteen points (83.20): when the end-to-end statistical route is nearly perfect, the translation joint is pure added risk [1]. Both regressions are the factorization again, now as a decision rule. The pipeline wins at least when

$$P(\text{parse}) \cdot P(\text{faithful} \mid \text{parse}) \;\gt\; P_{\text{CoT}}(\text{correct}),$$

the engine's factor of $1$ multiplying whatever the translator delivers, against the monolith's single unfactored number. This is a sufficient condition rather than an exact criterion: the left side is a lower bound on the pipeline's accuracy, since a lucky unfaithful program can add to it. Deep composition drives the right side down and leaves the left side alone; hard, open English drives the left side down and leaves the right side alone. Our committed table is this inequality at desk scale, with the crossover sitting between depth 0 and depth 1.

The unsolved part

Both published remedies act on the same trigger: a visible failure. Repair fires when the solver emits an error; the vote filter fires when a sample fails to parse. Neither can fire on the failure that matters most: the translation that parses, executes, and means the wrong thing. A quantifier flipped, a conditional reversed, a predicate silently merged with its near-synonym: the resulting program is syntactically immaculate, the solver derives its consequences with perfect soundness, and the pipeline returns a confidently wrong answer wearing a valid proof. In the factorization this is the $P(\text{faithful} \mid \text{parse})$ term, and the uncomfortable fact is that nothing in the pipeline measures it. The engine checks the program against the program, never the program against the sentence. Repair cannot help, because there is no error message; voting helps only if the mistranslations are uncorrelated, and a translator that systematically misreads a construction misreads it in all $K$ samples. Formalization faithfulness has no oracle: no component of the pipeline can decide whether a formula means an English sentence, and a second translator recruited to check the first would face the same question about itself. Our companion made the term equal $1$ by construction, which is exactly why it could exhibit everything else cleanly, and exactly what no open-vocabulary translator can do. Nor is the problem hypothetical: the next chapter shows that even a benchmark's gold translations, written by expert annotators, fail a prover-in-the-loop self-check often enough that the published protocol had to repair the failures before it could trust its own labels.

Why it matters

Translate-then-prove takes the opposite corner from everything before it in this volume: the earlier chapters made logic differentiable so gradients could flow through it; this one keeps the logic crisp and moves all the learning to the boundary where language becomes program. The reward is the strongest correctness statement in the volume, an exactness factor of literally $1$ past the boundary; the price is an unmeasured quantity (faithfulness) plus a visible refusal mode (abstention). For Volume 5, this chapter hands over a live deployment question in committed numbers: on the same 1,500 questions, one system always answers and is quietly wrong 12.3 percent of the time, the other answers 92.9 percent of the time and is never silently wrong, by assertion. Which contract a hospital, a court, or an autonomous lab can live with is not a benchmark question, and Volume 5's chapters on calibration, abstention, and verifier-gated generation inherit it directly. The two pillars close the loop: the engine half is Volume 1's prover doing what Part I promised symbolic systems could do (be right, provably, within their language), and the translator half is Volume 3's lesson restated (learned representations buy coverage and pay in guarantees). The pipeline does not resolve that trade; it prices it.

Key terms

• Translate-then-prove: the architecture in which a translator maps natural language to a formal program and a symbolic engine derives the answer, concentrating all fallibility in the translation stage.
• Correctness factorization: $P(\text{correct}) \ge P(\text{parse}) \cdot P(\text{faithful} \mid \text{parse}) \cdot 1$, the engine factor pinned by soundness, completeness, and termination; an equality when faithfulness is sure, since then no unfaithful program can answer right by luck.
• Coverage: the probability $P(\text{parse})$ that the translator accepts an input; in the companion, the only source of end-to-end error, lifted by repair from 0.8080 to 0.9293.
• Executable rate: the published analogue of coverage, the fraction of problems whose generated program runs without a solver error; self-refinement lifts it (FOLIO 66.7 → 84.3) without comparably lifting accuracy.
• Self-refinement: feeding the solver's error message back to the translator for a bounded number of repair rounds; fixes syntax, rarely semantics.
• Error-filtered majority vote: sample $K$ translations, drop the unparseable ones, answer with the majority of the survivors, count all-error as wrong.
• Abstention: the pipeline's explicit refusal to answer when no translation survives; the companion's assert certifies abstentions never become silent wrong answers.
• Dual-query three-way protocol: ask the prover for the goal and for its negation; True if the first proves, False if the second, Uncertain if neither.
• Semantic translation error: a translation that parses and executes but does not mean the source sentence; invisible to repair and voting alike, and the reason $P(\text{faithful} \mid \text{parse})$ has no oracle.

Where this leads

This chapter scored two architectures on a corpus we generated ourselves, where gold labels were free because a prover wrote them. The field's real evaluations rest on benchmarks whose labels someone had to construct, balance, and verify. The next chapter, NL Reasoning Benchmarks (NL for natural language), takes the instruments themselves apart: how the generated corpora control depth, what FOLIO's human-written premises cost in label reliability (including the prover-in-the-loop self-check that even gold translations need), and what the three-way protocol demands of a benchmark before Uncertain can be a meaningful answer.

---

Companion code: examples/integration/translate_prove.py implements the whole pipeline: the grammar and lexicons (lines 89–145), the theory parser and the repair pass (lines 148–194), the prove step on Volume 1's backward chainer (lines 200–208), abstention (lines 211–228), the corrupted corpus imported from the soft reasoner's committed split (lines 235–254), and the asserts guarding the factorization, the no-silent-errors contract, and the coverage lift (lines 281–316). Run python3 examples/integration/translate_prove.py to reproduce every number in this chapter byte for byte; the run ends with SUMMARY translate_prove: corrupted=288/1500 coverage=0.8080->0.9293 acc_on_parsed=1.0000 overall=0.9293.