Zayden-Jung/logic-skeleton-bench
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Replace explicit rules with behavioral hidden systems

Browse Source
This commit is contained in:
Codex Bot
2026-09-23 00:10:37 +08:00
parent 3cf3db7b12
commit 9f54f8f5a3
12 changed files with 598 additions and 380 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/skeleton-language.md
+181 -222
View File
@@ -1,248 +1,207 @@
# Skeleton Generator and Intermediate Language
# Hidden System and Behavioral Skeleton 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.
This document specifies version 0.2 of the benchmark. The central change is that natural-language rendering no longer receives a system's rules. It receives only behavior produced by executing those rules.
## 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:
## Three-layer contract
```text
Skeleton ::= {
id, family, complexity, entities,
facts, rules, query, answer_options,
gold_answer, proof
HiddenSystem --execute/sample--> BehaviorSkeleton --LLM render--> Natural-language problem
| | |
never public observations only solver input
|
exact enumeration --> gold probability --> majority label --> evaluator only
```
Generation follows this order:
1. A seeded local generator builds an executable `HiddenSystem`.
2. The simulator runs controlled support cases repeatedly and records aggregate outcomes.
3. A held-out query combines known events in a combination not present in the histories.
4. An exact local enumerator computes the query's true outcome distribution and gold label.
5. The full answer-bearing record is written before either LLM is called.
6. `renderer_payload()` removes the program, exact probability, gold label, and latent trace.
7. The renderer expresses only the public behavioral evidence in a surface domain.
8. The solver infers a mechanism from those observations and selects the more likely outcome.
This is system identification followed by transfer, not direct deduction from stated laws.
## Hidden system grammar
```text
HiddenSystem ::= {
initial_record,
conflict_policy,
rules: HiddenRule+
}
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+
HiddenRule ::= {
id,
on_event,
conditions: Condition*,
probability,
action,
target
}
Condition ::= {
source: "attribute" | "state",
key,
operator: "EQ" | "LE" | "GT" | "IS_SET",
value
}
action ::= "ADD_RECORD" | "INVALIDATE_RECORD" | "SET_FLAG"
probability ::= real number in [0, 1]
```
`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 grammar is finite, while different rule selections, parameters, event sequences, attributes, and stochastic outcomes generate an unbounded set of behavioral structures.
The implementation currently serializes Python tuples as JSON arrays. Each JSONL line is one complete skeleton.
### State and execution
## 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:
Each independent trial starts with:
```text
complexity = number of proof-bearing facts or ordered transformations
= len(proof)
record = ABSENT
invalidated = false
flags = {}
```
Named presets are:
Events execute from left to right. For each event, matching rules execute in stored order:
| Preset | Complexity |
1. evaluate all conditions against immutable attributes and current state;
2. if they hold, sample that rule's Bernoulli trigger;
3. if triggered, apply its action immediately.
Actions mean:
- `SET_FLAG(x)`: add internal flag `x`; later rules can test it;
- `ADD_RECORD`: make the record present unless it was previously invalidated;
- `INVALIDATE_RECORD`: remove the record and permanently set `invalidated=true`.
The current `PERSISTENT_INVALIDATION_VETO` policy therefore implements a one-vote veto. A later add cannot restore an invalidated record. Event order matters because a flag can enable a later rule and an early veto persists.
Probabilities belong to hidden rule activation. They are not printed in the rendered problem. The task asks whether `PRESENT` or `ABSENT` has probability greater than one half, not for a numerical probability.
## Exact gold computation versus sampled evidence
These are deliberately separate:
- Support histories are finite empirical data. The seeded simulator samples each case 48 times for short tasks and 64 times for longer tasks.
- The gold query probability is not estimated by Monte Carlo. The evaluator propagates a probability distribution over every reachable internal state, branching at every applicable stochastic rule.
For each state with mass `m` and applicable rule probability `p`, exact enumeration creates:
```text
inactive branch: same state, mass m(1-p)
active branch: action(state), mass mp
```
Equal resulting states are merged after each rule. At the end, the masses of all states whose record is present are summed. The answer is `PRESENT` when that sum exceeds `0.5`, otherwise `ABSENT`. Current generation rejects cases within `0.08` of the boundary to avoid fragile labels.
## Behavioral skeleton grammar
```text
BehaviorSkeleton ::= {
id,
family,
complexity,
event_vocabulary,
attribute_vocabulary,
observation_protocol,
hidden_system,
support_cases: BehaviorCase+,
query_case: BehaviorCase,
answer_options: ["PRESENT", "ABSENT"],
gold_answer,
gold_present_probability,
latent_trace
}
BehaviorCase ::= {
id,
attributes,
events,
trials,
observed_present,
observed_absent
}
```
Support cases have integer observation counts that sum to `trials`. The query has `null` observation counts because its result is what the solver must predict.
The public payload contains:
```text
family, complexity,
event_vocabulary, attribute_vocabulary,
observation_protocol, support_cases,
query_case, answer_options
```
It never contains:
```text
id, hidden_system, gold_answer,
gold_present_probability, latent_trace
```
## Current generated structure
Every system has at least four interacting rules:
- an unconditional probabilistic add event;
- an attribute-gated probabilistic veto event;
- an event that probabilistically sets an invisible flag;
- a later event whose effect requires that flag.
Longer configurations add attribute-gated add or veto rules. Support evidence includes:
- every event in isolation;
- pairwise event combinations;
- both orders of the state-gated pair;
- low/high attribute counterfactual controls;
- repeated outcomes rather than rule annotations.
The query applies all events in order. Its complete combination is held out from support evidence, so the model must compose effects learned from smaller interventions.
Generated indices alternate between present-favored and absent-favored systems to prevent a one-label benchmark. The index is redacted from the renderer payload so this balancing mechanism cannot become a shortcut. It affects hidden parameter ranges, never the answer after generation; the exact enumerator remains authoritative.
## Complexity and determinism
`complexity` is the number of distinct events in the held-out sequence and the minimum number of corresponding hidden rules. It is independent of rendered token count.
| Preset | Ordered query events |
| --- | ---: |
| `short` | 2 |
| `medium` | 4 |
| `long` | 6 |
| `short` | 4 |
| `medium` | 6 |
| `long` | 8 |
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.
Explicit values from 4 through 10 are accepted. `generate_skeletons(count, length, seed)` uses a local pseudorandom generator; the same code version and arguments produce equivalent hidden systems, samples, queries, and gold answers.
### `entities`
## Renderer obligations
The symbol table. Every non-literal argument appearing in facts or the query must be declared here.
The renderer may rename event codes, attributes, states, and outcomes into a coherent scenario. It must preserve every numeric count, attribute value, event order, trial boundary, query input, and answer label.
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.
It must not:
### `facts`
- receive or state hidden rules;
- turn empirical correlations into declared laws;
- expose trigger probabilities, internal flags, latent traces, or the answer;
- collapse a repeated experiment into a deterministic statement;
- add causal or real-world assumptions;
- show the exact query combination as an already observed history.
Atomic premises or state instructions. Their meaning is family-specific.
Retaining the complete pre-render record makes rendering fidelity independently auditable.
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.
## Extension points
### `rules`
The next DSL extensions can remain compatible with the three-layer boundary:
The inference laws needed to solve the generated instance. They are included explicitly so that solving does not require real-world assumptions.
- multiple entities and relations between them;
- delayed actions, expiry, and multiple clock phases;
- priority, last-write, merge, and fallback conflict policies;
- partial observation and noisy sensors distinct from stochastic behavior;
- candidate-program enumeration to report identifiability;
- counterfactual and intervention queries in addition to outcome prediction.
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
```text
LEFT_OF(E, E)
RELATION(E, E) -> {LEFT_OF, RIGHT_OF, UNKNOWN}
```
Rules:
```text
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:
```json
{
"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
```text
MEMBER_OF(E, S)
SUBSET_OF(S, S)
MEMBER_OF(E, S) -> {YES, NO, UNKNOWN}
```
Rule:
```text
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
```text
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:
```text
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:
```text
id, family, complexity, entities, facts,
rules, query, answer_options
```
It does not receive:
```text
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:
```python
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.
Any extension must keep gold computation local, expose behavior rather than source rules, preserve seeded reproducibility, and add tests for execution order, conflict semantics, and renderer redaction.