On Representations of Problems of Reasoning about Actions

TL;DR: In a 1968 Machine Intelligence 3 chapter, Saul Amarel walked the missionaries-and-cannibals puzzle through a ladder of half a dozen successive re-encodings and showed that each one shrank the search until the solution could essentially be read off a diagram — then argued that the real problem of AI is not searching within a representation but automatically finding better ones. Nobody in 1968 had any mechanism for a machine to invent an abstraction, so the idea sat as a manifesto for fifty years. Today, LLMs are plausible generators of candidate reformulations and model checkers / program synthesizers are plausible verifiers of them, which makes Amarel's program — for the first time — an engineering project rather than a philosophical one. (Bibliographic details of the chapter were not verified here; the standard citation is Amarel, "On Representations of Problems of Reasoning about Actions," Machine Intelligence 3, ed. Michie, 1968.)

The idea as Amarel had it

The state of the art Amarel wrote against was GPS-era heuristic search: Newell and Simon's General Problem Solver, chess and theorem-proving programs, all of which took a fixed encoding of states and operators handed to them by a human and then searched. The tacit assumption of the field was that intelligence ≈ good search within a given problem space.

Amarel's move was to show, in slow motion, that the human who chose the problem space had already done most of the intelligent work. His vehicle was missionaries and cannibals: three missionaries, three cannibals, a two-person boat, missionaries must never be outnumbered on either bank.

His ladder of formulations goes roughly like this (I am reconstructing from memory of the paper; the exact numbering may differ):

1. Individuals as objects. The state records which bank each of the six named people and the boat is on. Operators move named individuals. This is what a naive natural-language reading gives you.
2. Abstract away identity. Missionaries are interchangeable; so are cannibals. The state collapses to a vector (m, c, b): missionaries on the left bank, cannibals on the left bank, boat position. Roughly 128 configurations collapse to 32, of which only about 20 are legal.
3. Operators as vectors. A boat trip is just a vector added to or subtracted from (m, c) — one of five loads: MM, CC, MC, M, C. The problem becomes navigation on a tiny integer lattice.
4. Draw the lattice. Plot the legal region in the (m, c) plane. The constraint carves out a narrow corridor; the solution is an 11-move zigzag through it that is nearly forced — at the critical middle steps there is essentially one legal continuation. Search has evaporated. Amarel also noted that in the good representation, generalizations (to n missionaries, boat capacity k) become easy, which is a hallmark of a right encoding.

The punchline: each rung of the ladder was a representation shift — dropping irrelevant distinctions, exposing an invariant, changing coordinates — and the total effect was to turn an exponential search into a lookup. Therefore, he argued, the central open problem is a system that performs these shifts itself.

To put crude numbers on the collapse: naive tree search over 11-step move sequences with branching factor ~5 visits on the order of 5^{11} \approx 5 \times 10^7 nodes; graph search in the (m,c,b) space touches at most a few dozen; the diagram requires roughly zero search.

Why it could not work then

The barrier was not compute, and it's worth being precise about that, because it makes this paper unusual among 1960s AI ideas. A late-60s machine like an IBM 360/65 ran at very roughly 10^5–10^6 instructions per second with well under a megabyte of core — but the reduced missionaries-and-cannibals space fits in a page of memory. The problem was there was no generator. A search program's hypothesis space is fixed by its encoding; nothing in GPS or its successors could produce a new encoding as an output.

What would it take? You need three capabilities, and 1968 had none:

• Proposing abstractions. Candidate re-encodings ("individuals are interchangeable," "only the counts matter," "this quantity is conserved") live in an open-ended space of programs/mappings. There was no way to enumerate this space except syntactically, and syntactic enumeration of programs was (and is) hopeless — even today, blind synthesis stalls at a few dozen tokens of program.
• Verifying soundness. A representation shift is only useful if it's sound: an abstract solution must lift back to a concrete one. Checking this is a bisimulation/homomorphism property. Model checking didn't exist (Clarke–Emerson and Queille–Sifakis are early-1980s work); automated theorem proving in 1968 was resolution on toy problems.
• Knowing where to look. Human reformulation is guided by semantic priors — "people are interchangeable," "conservation laws matter," "plot it." No 1960s system had any world knowledge to draw on. This is the deepest gap, and it's exactly the one that stayed open longest.

So the field kept the search half of Amarel's paper and shelved the reformulation half. Fifty years of planning research largely optimized search within human-written encodings (STRIPS, then PDDL), which is a monument to how right Amarel was about where the leverage is and how hard the automation is.

What changed

Each missing ingredient now exists in usable form:

Generators. LLMs are, empirically, decent proposers of reformulations. They carry exactly the semantic priors the 1960s lacked: asked about missionaries and cannibals, a modern model will volunteer that individuals are interchangeable and suggest counting representations, because it has absorbed human mathematical culture. FunSearch (2023) and AlphaGeometry-style systems demonstrated the general pattern: an LLM as a smart, biased sampler over a space of programs/constructions, with a symbolic evaluator keeping it honest.

Verifiers. Model checkers, SMT solvers, and planning validators can check the soundness properties a proposed abstraction must satisfy — that a mapping \phi from concrete to abstract states is a homomorphism (every concrete transition maps to an abstract one), or the stronger condition that abstract plans refine to concrete plans. For finite domains this is fully mechanical.

Precedent that abstraction can be automated at all. CEGAR (counterexample-guided abstraction refinement, ~2000) automated a narrow version of Amarel's loop for hardware verification: over-abstract, find a spurious counterexample, refine, repeat. Planning research automated symmetry reduction and abstraction heuristics (pattern databases, merge-and-shrink). DreamCoder (2021) automated library learning — inventing reusable concepts that compress future search. Each of these is a special case of "change the representation to make search cheap"; none is the general engine Amarel wanted.

A serious 2026 revival

The clean experiment is an automated re-representation loop, scored by search-cost reduction:

1. Input: a problem in a formal language (PDDL, or a transition-system program), plus its natural-language statement.
2. Propose: an LLM generates candidate representation shifts as programs: a state-mapping \phi, invariants ("m \ge c on each bank or m=0"), symmetries (permutations of objects that commute with the dynamics), conserved quantities, and merged/quotiented operators. Crucially it sees both the formal encoding and the natural-language framing — the semantic priors live in the latter.
3. Verify: a model checker / SMT solver certifies each candidate — the invariant really is inductive, the permutation really is a dynamics symmetry, \phi really is a sound homomorphism with a plan-refinement guarantee. Rejects are returned as counterexamples for the LLM to repair (CEGAR with an LLM as the refinement oracle).
4. Score: run an off-the-shelf planner in the old and new encodings; the reward is the log reduction in nodes expanded. Iterate — Amarel's point was that shifts compose into a ladder.
5. Benchmarks: Amarel's own ladder as the unit test (does the system rediscover the (m,c,b) quotient unaided?), then International Planning Competition domains, where hand-designed abstractions are known to yield orders of magnitude — giving a measurable gap between "planner alone" and "planner + human reformulation" that the agent should close. ARC-style puzzles are the stretch goal: problems that are nothing but representation-finding.

Reuse from the paper: the framing (representation shift as the object of study), the ladder methodology, and the evaluation metric (search collapse). Replace: the human in the loop, with an LLM+verifier pair; and the informal notion of "better representation," with the certified-homomorphism-plus-cost-reduction criterion.

Has it been tried? What's open

Partially, in fragments. Korf's 1980 work "Toward a model of representation changes" attacked it directly with 1970s machinery and, tellingly, stalled — the generator problem again. CEGAR, symmetry breaking in planning, merge-and-shrink abstractions, and DreamCoder each vindicate one rung. On the neural side, there is active work on LLMs writing PDDL from natural language ("LLM+P" and successors) and on LLM-guided invariant synthesis for verification. To my knowledge, no published system yet runs the full closed loop — LLM proposes a quotient representation, verifier certifies it, planner's cost drop is the training/selection signal, and shifts compose into a ladder — though I would not be surprised if several groups are building exactly this now.

What's genuinely open: (a) the refinement guarantee in rich domains — sound abstraction is easy to state and hard to get non-trivially, since safe abstractions tend to be either lossless-and-useless or lossy-and-unsound; (b) transfer — Amarel wanted representations that make families of problems easy, not one instance, which suggests amortizing the loop into the model DreamCoder-style; (c) whether the LLM's priors extend to problems humans haven't already reformulated in its training data — the honest worry is that the missionaries demo would be memorization, which is why unseen synthetic transition systems must be in the benchmark.

Where to read it

The chapter appears in Machine Intelligence 3 (ed. Donald Michie, Edinburgh University Press, 1968); scans circulate online and it's reprinted in Readings in Artificial Intelligence. No canonical link was provided here, and I haven't verified page numbers. Read alongside: Korf's "Toward a Model of Representation Changes" (Artificial Intelligence, 1980) for the first serious attempt; Kaplan & Simon's mutilated-checkerboard study (1990) for the cognitive-science view of why representation shifts are the hard human step too; Clarke et al. on CEGAR (2000) for the one place the loop was fully automated in a narrow domain; and Ellis et al., DreamCoder (2021) plus Romera-Paredes et al., FunSearch (2023) for the modern generator-verifier pattern a revival would be built from.