Case packet
Neutral case identifier: case-8444045b653617
The possible directed relationship from Artifact A to Artifact B is under review.
Artifact A
Formal symbolic systems assess explanatory-reach only through causal and proof obligations
[Reach-assessment] is not intrinsically an LLM-only or natural-language-only capability. A formal symbolic system can contribute to it once the candidate commitment's claimed generality has been translated into an obligation the system can check — a causal mechanism that should survive interventions or environment shifts, an identifiable causal effect under stated assumptions, or a theorem over a formally specified domain.
The shift is from asking "does this sentence sound like a good generalization?" to asking "what formal consequence must hold if this generalization is genuine?" What such a check establishes is bounded by the translation that produced it, which the last section takes up.
The causal route
Causal theories have explanatory-reach because they do not merely fit one observed distribution. A structural causal model states mechanisms whose implications extend to interventions and counterfactuals; [causal representation learning] frames this as the difference between statistical models of one distribution and causal models that represent distributions under possible interventions.
That is the route formal reach-assessment can use: a proposed commitment is accepted not because it predicts the training cases, but because the mechanism it asserts supports the intended intervention, counterfactual, or shift claims. [Invariant prediction] tests whether candidate predictors keep their predictive relation across environments — one that holds across environments A and B but breaks once C is included is flagged as non-invariant and excluded, rather than accepted on A/B fit alone. [Causal-learn], a Python library for causal discovery, collects algorithms that infer causal structure from observational data under method-specific assumptions. [DoWhy], a causal-inference library, makes the same boundary operational by requiring declared assumptions before identification, estimation, and partial validation or refutation tests.
So a system that learns by causal theories can have reach-assessment, but the warrant is assumption-relative. It must represent the candidate theory, the target intervention or counterfactual class, the discovery or identification assumptions, and the acceptance tests that distinguish mechanism from correlation. Three pieces of apparatus recur, and they are not the same kind of thing: causal sufficiency is an assumption (no relevant common causes go unobserved among the modeled variables), latent confounding is the failure mode when it does not hold, and do-calculus is the rule system for deriving intervention effects from a supplied graph. None of them justifies the graph and variables they range over.
The proof route
Proof is a second route. If a candidate commitment can be expressed as a theorem, invariant, type property, model-checking obligation (exhaustively checking a property over the states or transitions of a formal model), or utility comparison over a specified domain, proof search can establish explanatory-reach across that domain. The result is genuine reach-assessment inside the model: the evaluator checks the claim's quantified consequence, not just sampled cases.
[Jürgen Schmidhuber's Gödel-machine proposal] is the useful placement example — a proof-gated host architecture in which a candidate self-rewrite is accepted only when the machine proves that switching now yields higher axiomatized utility than continuing proof search, under the current axioms and utility function.
So the [Gödel machine] fits here conditionally. Were its axioms to include the relevant causal assumptions and its utility function to reward correct intervention or counterfactual generalization, the proof gate could license adopting a causal-theory learner, graph, or inference rule. Without them it supplies the acceptance rule and not the assessment.
The formalization boundary
The formal routes move judgment upstream rather than abolishing it. A proof shows a theorem follows from axioms, not that the variables, domain, or utility function represent the original claim; causal inference gives assumption-relative warrant, not validation of causal truth from observations alone. So a theorem over the wrong variables can pass every obligation while missing the intended commitment, and an invariant relation selected from narrow environments can look stable while tracking an artifact of sampling. These are failures in the translation from the natural-language claim to the formal obligation rather than failures of proof or do-calculus, [which is why warranted autonomy is bounded by oracle domain].
The invariance case has been worked out formally. [Rosenfeld, Ravikumar, and Risteski] analyse the invariant risk minimization objective inside a Gaussian structural equation model and construct a predictor that is near-optimal under the penalized objective and near-identical to the invariant predictor on training data, yet reverts to plain empirical risk minimization once the test environment drifts far enough: the obligation is discharged and the wrong commitment is recovered. The mechanism generalizes past IRM. The penalty that construction pays scales with the mass of the region where it misbehaves, and that region is rare in training — so an acceptance criterion evaluated on the distribution that produced the candidate can price bad off-distribution behaviour at nearly nothing.
The same analysis says when the route pays. In the linear regime it establishes a threshold in the number of training environments E against the dimension d_e of the environment-varying features: above it, any feasible linear featurizer must discard those features and the invariant predictor is recovered; at or below it, a predictor using only environmental features is feasible and attains lower risk. The causal route is therefore worth taking where genuine environments are plentiful relative to the spurious-feature dimension and the model class is restricted enough for feasibility to bite. Where they are not, it returns an answer carrying no more warrant than fitting would have.
Two limits keep this from proving more than it does. The result bounds the IRM objective and close relatives, not invariance-based causal inference generally, so it leaves [invariant prediction] as used above intact: Peters and colleagues analyse a hypothesis-testing procedure with confidence bounds, while the evasion constructed here is what optimizing over a rich hypothesis class admits. And that construction is an existence proof about what the objective permits, not evidence that gradient training finds such a solution — enough to show the obligation underdetermines the commitment, not that practitioners land there.
The natural-language case remains different. A natural-language claim whose reach has not been reduced to causal or proof obligations still needs semantic judgment about what it means and where it breaks. Current LLM-mediated review appears to supply some of that judgment, and this note does not explain why. The narrower point is what stands: once explanatory-reach is represented as formal obligations, symbolic systems can assess it inside their modeled domain — and the edge of that domain is fixed by a translation they do not check.
Relevant Notes:
Artifact B
Warranted autonomy is bounded by oracle domain
Autonomy — how much of an improvement pathway runs without a person — is a separate gradient over a [self-improving system]. This note concerns the pathway shape that has a gate: the [proposal-selection improvement loop], where candidates are evaluated and can fail to be adopted. Bare autonomy is free: hand the gate to a model with a rubric and no human runs it. More autonomy strengthens that attribution, but it is not automatically a better design. What is bounded is warranted autonomy — a loop that runs unattended and can still be trusted with what it accepts.
Warranted evaluation autonomy extends only to the candidates the available oracle can assess with the required confidence, [since the boundary of automation is the boundary of verification]. Outside that domain, unattended evaluation remains possible but unwarranted.
Strength, strictness, and domain
Oracle strength concerns how reliably a check discriminates relative to the objective and what its result establishes. Strictness concerns how much evidence the gate demands before accepting. Domain is the range of candidates the oracle's strength, at whatever strictness is set, suffices to warrant — distinct from a claim's own [explanatory-reach] and from a generator's [search range], the cluster's two other limit vocabularies. Increasing strictness under a fixed oracle usually narrows acceptance: uncertain candidates are rejected or deferred so the remaining acceptances carry more assurance.
Strengthening discrimination can instead expand the warranted domain. A better verifier may reject bad candidates the old one passed while also accepting good candidates the old one could not distinguish from bad ones. Test suites, proofs, model judges, and human judgment therefore do not form nested acceptance sets; they establish different things over overlapping domains.
The [Gödel machine] is the limiting case of assurance obtained through strict acceptance: a rewrite runs only when the machine proves that switching helps under its formalization. It gains warranted total autonomy within that proof surface and excludes improvements it cannot prove. The cost follows from its proof requirement, not from a general law that stronger oracles always accept less.
[Commonplace] composes several oracles: tests and validators for structural constraints, human judgment for criteria that are not adequately automated. It could hand the latter gates to a model tomorrow and become more autonomous without becoming more warranted. Expanding warranted autonomy requires improving the relevant oracle's discrimination or narrowing the gate to cases it can establish.
The useful questions are therefore both how autonomous is the loop? and which of that autonomy is warranted by its oracles?
Oracle hardening moves the boundary
Oracle hardening can move a gate from unwarranted to warranted autonomy: a rubric becomes a validator, a heuristic becomes a test, or an unmeasured property becomes observable. The [oracle-strength spectrum] describes different verification surfaces, not a total order over their acceptance rates.
Hardening may expand the warranted domain by resolving cases the old oracle could not discriminate. Where criteria still outrun the oracle, the system must retain a human evaluator, narrow the unattended gate, or accept unwarranted autonomy.
Scope
- The claim concerns evaluation autonomy, so it is scoped to proposal-selection pathways — a direct evidence-driven update has no gate to hand over, and its trustworthiness is a question about the objective and the update rule instead. Search has a different failure surface, [since false-positive generation faces evaluation before retention].
- Bare autonomy means nobody is required at the gate. Warranted autonomy additionally claims that the unattended gate is reliable enough for its use.
- Warrant is objective-, risk-, and threshold-relative. No oracle is warranted for every decision merely because it is mechanical.
- Several oracles may govern different parts of one acceptance decision; their combined domain need not equal the union of what each accepts independently.
Relevant Notes:
Under-review context phrase
formal guarantees remain bounded by the oracle or axiomatization that produces them