Programs, Solvers, and Symbolic Scaffolds

A language model can recognize the structure of a problem and still lose the answer to arithmetic, a malformed query, or one invalid proof step. Executable reasoning separates those jobs. The model proposes a program, query, constraint system, or proof; a runtime interprets that artifact under specified rules; and a task-level check decides whether the result answers the original request. The runtime makes some failures visible, but it does not make the translation correct. A precisely executed solution to the wrong formalization is still wrong.

This pattern matters because natural language and formal systems fail differently. Language is forgiving enough to express an underspecified problem. A program or proof must satisfy a grammar and interface before it can run. Moving work into an executable artifact therefore creates better places to test the system, while leaving a semantic gap between what the user meant and what the artifact says.

The artifact contract

The useful abstraction is not “the model calls Python.” It is a typed boundary between a probabilistic translator and a controlled executor:

$$p \sim q_\theta(p \mid x,C), \qquad r = E_\Gamma(p), \qquad r=(s,o,\tau,u).$$

Here $x$ is the original request; $C$ is the artifact contract, including the grammar, types, allowed operations, input schema, and output schema; $q_\theta$ is the model's distribution over artifacts under parameters $\theta$; $p$ is one sampled artifact; $\Gamma$ is the pinned execution environment, including runtime and dependency versions, data snapshot, permissions, and resource limits; $E_\Gamma$ is the executor in that environment; and $r$ is its structured result. Its four fields are status, value, trace, and resource usage: status $s$, typed output $o$, execution trace $\tau$, and resource usage $u$. Typical statuses include ok, parse_error, type_error, policy_violation, runtime_error, and timeout.

Even a deterministic program is deterministic only relative to that environment. A SQL query reads a particular database snapshot. Python code inherits floating-point rules, package versions, locale, and time sources. A solver may reach unknown or exhaust its budget. Reproducibility requires recording $\Gamma$, not merely saving the generated text.

The contract should be narrow enough to validate before execution. A calculator task may accept a small expression language rather than arbitrary Python. A reporting task may accept a read-only query over an allowlisted schema. A proof service may accept one theorem statement and one proof term, with imports fixed by the service. A smaller language reduces both ambiguity and authority.

A valid execution is not yet a valid answer

Three checks answer three different questions:

1. Well-formedness: does $p$ satisfy contract $C$? Parsing, schema validation, type checking, import policy, and static restrictions belong here.
2. Execution success: did $E_\Gamma$ finish with status ok inside its permission and resource budget?
3. Task agreement: do the artifact, assumptions, inputs, and result still match $x$?

An acceptance rule can make that separation explicit:

$$\operatorname{Accept}(x,p,r) = W_C(p) \land [s=\texttt{ok}] \land A(x,p,r).$$

$W_C(p)$ is the well-formedness predicate induced by contract $C$; $s$ is the executor status contained in $r$; and $A(x,p,r)$ is the task-agreement check. The brackets around $s=\texttt{ok}$ denote the Boolean truth of that condition. Accept is true only when all three conditions hold.

The first two checks are often mechanical. The third is the hard one. A program can run perfectly while using the wrong tax rate. A query can be valid SQL while joining customer and account identifiers incorrectly. A proof can establish a theorem whose quantifiers do not match the informal claim. Exact execution contains a wrong formalization; it does not repair it.

This runnable example keeps the translation visible as a small data artifact. The task asks how many boxes hold three fifths of 240 bolts when each box holds 12. Both artifacts execute, but only one preserves the fraction stated in the problem.

from fractions import Fraction

problem = {"total": 240, "fraction": "3/5", "per_box": 12}

artifacts = [
    (
        "wrong but runnable",
        {"total": 240, "fraction": "2/5", "per_box": 12},
    ),
    (
        "correct artifact",
        {"total": 240, "fraction": "3/5", "per_box": 12},
    ),
]

def execute(artifact):
    packed = artifact["total"] * Fraction(artifact["fraction"])
    boxes = packed / artifact["per_box"]
    if boxes.denominator != 1:
        raise ValueError("the result is not a whole number of boxes")
    return boxes.numerator

def check_task(problem, artifact, result):
    for field in ("total", "fraction", "per_box"):
        if artifact[field] != problem[field]:
            return f"contract rejects: {field} mismatch"
    expected = execute(problem)
    if result != expected:
        return "contract rejects: result mismatch"
    return "contract accepts"

for label, artifact in artifacts:
    result = execute(artifact)
    verdict = check_task(problem, artifact, result)
    print(f"{label}: executes to {result}; {verdict}")

The output is wrong but runnable: executes to 8; contract rejects: fraction mismatch and correct artifact: executes to 12; contract accepts. This checker works because the example already exposes the task as structured fields. For a free-form legal, medical, or business request, constructing $A$ can be harder than executing $p$. Human review, independent tests, source-grounded constraints, or abstention may still be necessary.

What each runtime establishes

“Tool use” groups together systems with very different semantics. The right question is not whether a tool is formal, but what its successful return actually establishes.

An SMT solver, short for satisfiability modulo theories solver, extends Boolean satisfiability with theories such as arithmetic, arrays, or bit-vectors. It can give a model for a satisfiable encoding, establish unsatisfiability for supported fragments, or return unknown. A computer algebra system manipulates expressions under domain assumptions. Neither system understands the user's intention outside the encoding.

Proof assistants offer a narrower and stronger boundary. In Lean, tactics and automation construct proof terms, then a small kernel checks those terms against the formal environment (Moura and Ullrich 2021). This architecture reduces the trusted checking core, but the guarantee remains relative to the theorem statement, definitions, imports, and axioms. It also does not make an untrusted proof package safe to build; tactics and other metaprograms can execute code before the final kernel check.

Retrieval belongs in the table to mark a category boundary. ReAct interleaves reasoning, actions, and observations, which can ground a trajectory in external evidence (Yao et al. 2023). The observation is new information, not a certificate. A web page can be stale, a tool can fail, and an action can change state. Retrieval therefore needs source validation and authorization, not only execution.

What the program-aided methods demonstrated

Gao and colleagues introduced Program-Aided Language Models (PAL) in 2022 and published the work at ICML 2023. PAL prompts a model to express intermediate reasoning as a Python program, then delegates execution to the interpreter. Its evidence covered thirteen mathematical, symbolic, and algorithmic tasks (Gao et al. 2023). The result supports a focused claim: when decomposition can be written as code, external execution can remove local calculation work from the model.

Program of Thoughts (PoT), published by Chen and colleagues in TMLR in 2023, uses a similar split for numerical reasoning. Its evaluation covered five math word-problem datasets and three financial question-answering datasets (Chen et al. 2023). PoT can interleave explanatory text and program statements, but only the executed statements receive interpreter semantics. Comments and prose remain ordinary model output.

Faithful Chain-of-Thought, introduced by Lyu and colleagues in 2023, generalizes the artifact beyond Python. It translates a request into a chain containing task-specific symbolic language, then uses Python, Datalog, or a PDDL planner to execute the symbolic portion. The paper evaluated math word problems, planning, multi-hop question answering, and relational inference (Lyu et al. 2023). These domains expose useful formal intermediates. The results do not establish that arbitrary open-ended reasoning can be translated or checked the same way.

The shared contribution is an interface, not a new source of truth. The model still chooses variables, operations, relations, and assumptions. The runtime gives those choices explicit consequences. That is valuable precisely because a failed parse, violated type, counterexample, or rejected proof can return structured feedback to the controller.

Faithfulness has three meanings

Executable reasoning is often called faithful, but three claims must remain separate.

• Execution faithfulness means the returned value was mechanically derived from the executed artifact. If the system obtains $r=E_\Gamma(p)$ with status ok and renders its typed output $o$ without an unchecked model-generated bypass, then $p$ is causally upstream of the answer.
• Semantic faithfulness means $p$ correctly represents the original request, including its entities, units, assumptions, and constraints. Execution alone does not establish this claim.
• Narrative faithfulness means any explanation accurately describes the artifact and execution trace. A model-written explanation can still be post-hoc or contradict the code.

Faithful CoT strengthens the first property. It does not expose the model's hidden computation or explain why the translator selected $p$. Correct translation is required for task correctness, not for the narrower causal fact that the executor produced the answer from the artifact.

This distinction changes the final presentation step. Returning model.generate(explain(result)) without a check opens a new path for the model to alter a correct result. A production system should render typed values deterministically, or extract the answer from generated prose and verify that it equals the executor output. The explanation may be flexible; the answer binding should not be.

Repair is a controlled search loop

Execution feedback can improve a candidate, but a repair loop needs the same discipline as the search controller in Chapter 25. First classify the failure:

• parse, schema, or type failures concern the artifact contract;
• policy failures concern forbidden imports, operations, or authority;
• runtime, timeout, and resource failures concern execution in $\Gamma$;
• failed task checks concern the translation or its assumptions;
• presentation failures concern the binding from typed output to user-visible answer.

Each attempt should retain the immutable request, produce a versioned artifact, and receive a structured diagnostic for one failure class. The controller needs an attempt budget and an overall cost or wall-clock limit. Every repaired artifact must pass the full contract again; a syntax repair does not inherit semantic approval from the previous version. If no candidate passes, the system should abstain or fall back rather than return the last runnable artifact.

Diagnostics are also an input boundary. Do not feed raw secrets, arbitrary tool output, or unrestricted compiler logs back into the model. Normalize errors, remove sensitive values, cap their size, and label untrusted text. A repair prompt is still a prompt, and tool output can carry instructions the controller should not follow.

Formal proof is strong after formalization

A proof kernel makes its guarantee precise. Let $K$ be a sound kernel, $\Delta$ a formal environment of definitions and axioms, $\pi$ a proof term, and $\varphi$ the proposition being checked. Then

$$K(\Delta,\pi,\varphi)=\operatorname{accept} \quad\Longrightarrow\quad \Delta\vdash\varphi.$$

The turnstile $\vdash$ means that $\varphi$ is derivable from $\Delta$. This is a strong statement about the formal object. It says nothing by itself about whether $\varphi$ faithfully translates an informal problem, whether $\Delta$ contains acceptable axioms, or whether the surrounding build process was safe. For high-assurance checking, the theorem statement and allowed environment must come from a trusted source, and generated proofs should be built in isolation and rechecked by the kernel or an independent checker.

Recent theorem-proving systems show both the strength and the cost of this boundary. In the 2024 International Mathematical Olympiad evaluation, AlphaProof proved three of the five non-geometry problems, whose statements experts manually formalized. AlphaGeometry 2 solved the geometry problem. The combined AlphaProof and AlphaGeometry 2 system scored 28 of 42 points, equivalent to a silver medal. The hardest problems used multi-day computation (Hubert et al. 2026). The live evaluation therefore did not measure informal-to-formal translation: experts formalized the non-geometry statements before proof search.

DeepSeek-Prover-V2 also starts from formal Lean statements. The 671-billion-parameter model proved 82.4% of the 244-problem miniF2F test set with 32 samples per theorem and 88.9% with a Pass@8192 budget, meaning that at least one of up to 8,192 generated proofs was accepted (Ren et al. 2025). Pass@8192 is not per-sample accuracy, and the benchmark does not measure informal-to-formal translation. These qualifiers do not weaken the accepted proofs. They locate what the experiment measured: proof generation after a formal statement and checker already exist.

The executor is a security boundary

Generated artifacts are untrusted code, even when their purpose is arithmetic. A timeout alone is not a sandbox. A production executor should enforce a narrow authority envelope:

• isolate each run under an unprivileged identity in a disposable environment;
• deny network access and filesystem access by default, exposing only explicit inputs;
• enforce CPU, memory, output, and wall-time limits, plus process and syscall controls;
• pin the runtime, dependencies, schemas, and data snapshot used by the artifact;
• use read-only database credentials, allowlisted schemas, and query cost and row limits;
• keep authorization for messages, payments, deployments, and writes outside the code sandbox;
• record provenance, including the request, artifact hash, environment version, inputs, status, trace, resource use, checker version, and final rendering;
• validate outputs against their schema and task check before release.

These controls serve correctness as well as security. A pinned environment makes a result reproducible. Least privilege limits the damage from a mistaken translation. Provenance lets an operator distinguish a translator error from a runtime change, stale data, a checker failure, or a presentation bug. Chapter 56 develops the authority boundary in detail, while Chapter 41 places it inside the larger agent runtime.

Programs and solvers turn part of reasoning into an observable computation. They do not decide which observations deserve trust or how intermediate work should be scored. The next chapter examines that missing component directly: outcome checkers, process supervision, learned judges, and formal verifiers.

Further reading