logic-skeleton-bench/docs/skeleton-language.md

Skeleton Generator and Intermediate Language

This document specifies the answer-bearing logical skeleton generated before any natural-language rendering. The skeleton is the experimental ground truth; natural language is only one view of it.

Pipeline contract

The benchmark follows this order:

1. A deterministic local generator selects a logic family and constructs a typed skeleton.
2. The generator computes gold_answer and a proof trace from the structure itself.
3. The complete skeleton is written to skeletons.jsonl before any model call.
4. A redacted renderer payload removes gold_answer and proof.
5. The renderer converts the remaining structure into a self-contained natural-language problem.
6. The solver sees only that rendered problem and returns one permitted answer label.
7. The evaluator compares the label with the original gold_answer.

This ordering prevents the renderer from deciding or leaking the label. It also makes a failed or semantically inaccurate rendering auditable against its source skeleton.

Abstract grammar

The current intermediate language can be summarized as:

Skeleton       ::= {
  id, family, complexity, entities,
  facts, rules, query, answer_options,
  gold_answer, proof
}

entities       ::= Map<Symbol, TypeName>
facts          ::= Fact+
Fact           ::= { predicate: PredicateName, arguments: SymbolOrLiteral+ }
rules          ::= RuleText*
query          ::= { predicate: PredicateName, arguments: SymbolOrLiteral* }
answer_options ::= AnswerLabel+
gold_answer    ::= one member of answer_options
proof          ::= ProofStep+

Symbol, TypeName, PredicateName, and AnswerLabel are case-sensitive strings. Facts and queries use positional arguments. A predicate's arity and accepted argument types are defined by its logic family.

The implementation currently serializes Python tuples as JSON arrays. Each JSONL line is one complete skeleton.

Field semantics and invariants

id

A stable run-local identifier such as order-0000. It consists of a family prefix and generation index. It is not a semantic input to either model.

family

The name of the generator and inference system that owns the skeleton. Different families may reuse a predicate spelling only when its semantics and argument types are identical.

complexity

The intended structural length of the required proof, not a token count and not a target natural-language length.

For every current family:

complexity = number of proof-bearing facts or ordered transformations
           = len(proof)

Named presets are:

Preset	Complexity
short	2
medium	4
long	6

Explicit integer values from 1 through 20 are accepted. Future families must document any deviation from the proof-length interpretation; ideally they should not deviate.

entities

The symbol table. Every non-literal argument appearing in facts or the query must be declared here.

Examples of current types are Entity, Set, and Counter. Types exist to distinguish superficially similar but structurally different expressions, such as membership of an entity in a set versus a subset relation between two sets.

facts

Atomic premises or state instructions. Their meaning is family-specific.

Fact order is semantically irrelevant for declarative families such as transitive order and set membership. Fact order is semantically significant for procedural families such as sequential state updates. The renderer must preserve ordering whenever the family's rules say that order matters.

rules

The inference laws needed to solve the generated instance. They are included explicitly so that solving does not require real-world assumptions.

Rules are human-readable in version 0.1. A future version can replace or supplement them with machine-executable rule expressions. Until then, the local generator remains the authoritative implementation of the rule.

query

The proposition or value to determine. Its predicate declares the requested operation; its arguments bind the relevant entities.

answer_options

The complete set of legal output labels. The renderer must reproduce these labels exactly, although it may explain them in the surface story. The solver's structured-output schema restricts its response to this set.

gold_answer

The standard answer computed locally during generation. It must be a member of answer_options. Neither the renderer nor the solver may receive it.

proof

A minimal intended sequence of premises or transformations sufficient to derive the gold answer. It is primarily an audit trail and a complexity witness. It is not currently checked by the solver and is never sent to the renderer.

Current predicate signatures

The notation below uses E:Entity, S:Set, C:Counter, and N:Integer.

Transitive order

LEFT_OF(E, E)
RELATION(E, E) -> {LEFT_OF, RIGHT_OF, UNKNOWN}

Rules:

LEFT_OF(x, y) and LEFT_OF(y, z) imply LEFT_OF(x, z)
RIGHT_OF(x, y) iff LEFT_OF(y, x)

The current generator creates a directed chain of exactly complexity edges and asks for the relation between its endpoints. The edge list may be shuffled because the relation is declarative. The standard answer is computed as LEFT_OF before rendering.

Example:

{
  "id": "order-0000",
  "family": "transitive_order",
  "complexity": 2,
  "entities": {"E0": "Entity", "E1": "Entity", "E2": "Entity"},
  "facts": [
    {"predicate": "LEFT_OF", "arguments": ["E0", "E1"]},
    {"predicate": "LEFT_OF", "arguments": ["E1", "E2"]}
  ],
  "rules": [
    "LEFT_OF is transitive",
    "RIGHT_OF(x,y) iff LEFT_OF(y,x)"
  ],
  "query": {"predicate": "RELATION", "arguments": ["E0", "E2"]},
  "answer_options": ["LEFT_OF", "RIGHT_OF", "UNKNOWN"],
  "gold_answer": "LEFT_OF",
  "proof": ["LEFT_OF(E0,E1)", "LEFT_OF(E1,E2)"]
}

Membership inheritance

MEMBER_OF(E, S)
SUBSET_OF(S, S)
MEMBER_OF(E, S) -> {YES, NO, UNKNOWN}

Rule:

MEMBER_OF(x, A) and SUBSET_OF(A, B) imply MEMBER_OF(x, B)

The generator emits one membership fact followed logically by complexity - 1 subset links. It asks whether the entity belongs to the final set. Premises may be shuffled. The standard answer is YES.

Sequential state update

INITIAL_VALUE(C, N)
INCREMENT(C, N)
DECREMENT(C, N)
FINAL_VALUE(C) -> IntegerLabel

The generator chooses an initial non-negative integer and then emits exactly complexity ordered updates. An update that would make the state negative is replaced with an increment. The standard answer is produced by executing the updates locally. Two distinct adjacent integer distractors are added to answer_options.

Generator determinism

generate_skeletons(count, length, seed) uses a local pseudorandom generator initialized from seed. Given the same code version, count, length, and seed, it produces byte-equivalent semantic records.

Families are selected round-robin in the initial implementation:

0 -> transitive_order
1 -> membership_inheritance
2 -> sequential_state_update
3 -> transitive_order
...

Randomness currently affects premise order and arithmetic values or operations. It never delegates answer generation to an LLM.

Renderer boundary

The renderer receives:

id, family, complexity, entities, facts,
rules, query, answer_options

It does not receive:

gold_answer, proof

The renderer may:

• invent concrete or fictional names;
• replace abstract entities with objects in a coherent scene;
• express formal predicates in natural language;
• reorder declarative premises without changing their meaning.

The renderer must not:

• add or remove facts;
• reverse relation direction;
• reorder procedural state updates;
• introduce real-world assumptions needed for the answer;
• expose or hint at the standard answer;
• rename the permitted answer labels.

Renderer errors are a separate experimental failure mode from solver errors. Retaining both the skeleton and rendered problem makes those failures distinguishable during review.

Adding a logic family

A new family generator should satisfy all of these conditions:

1. Declare every symbol and type used by its facts and query.
2. Generate a satisfiable instance unless inconsistency is the property being tested.
3. Compute the gold answer locally without an LLM.
4. Emit a proof trace whose length agrees with complexity.
5. Provide finite, unambiguous answer labels suitable for exact-match scoring.
6. State whether fact order is semantically significant.
7. Avoid relying on culturally specific or real-world knowledge.
8. Add tests for determinism, type/arity invariants, gold-answer membership, and at least one boundary complexity.

The family function signature is:

def generator(index: int, complexity: int, rng: random.Random) -> Skeleton:
    ...

Register it in GENERATORS to include it in round-robin generation. A later heatmap runner can reuse the same stored skeleton set across every renderer/solver model pair, ensuring that model comparisons operate on identical logical inputs.