Generate proof-bearing dynamic world histories
This commit is contained in:
+193
-154
@@ -1,207 +1,246 @@
|
||||
# Hidden System and Behavioral Skeleton Language
|
||||
# Dynamic World Generator and Intermediate Language
|
||||
|
||||
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.
|
||||
This specification defines the answer-bearing world representation generated before natural-language rendering.
|
||||
|
||||
## Three-layer contract
|
||||
## Pipeline boundary
|
||||
|
||||
```text
|
||||
HiddenSystem --execute/sample--> BehaviorSkeleton --LLM render--> Natural-language problem
|
||||
| | |
|
||||
never public observations only solver input
|
||||
|
|
||||
exact enumeration --> gold probability --> majority label --> evaluator only
|
||||
HiddenProgram + seed
|
||||
↓
|
||||
Initial WorldState
|
||||
↓ stochastic transition sampling
|
||||
Realized Event Trace
|
||||
↓ deterministic closure and query selection
|
||||
Query + Gold Proof
|
||||
↓ redact program, hidden state, proof, and answer
|
||||
Renderer Payload
|
||||
↓
|
||||
Natural-language history → Solver
|
||||
```
|
||||
|
||||
Generation follows this order:
|
||||
Randomness affects which events occur. It never makes the final question probabilistic: after the trace is realized, the evaluator asks whether a proposition follows in that particular world.
|
||||
|
||||
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
|
||||
## Hidden program
|
||||
|
||||
```text
|
||||
HiddenSystem ::= {
|
||||
initial_record,
|
||||
conflict_policy,
|
||||
rules: HiddenRule+
|
||||
HiddenProgram ::= {
|
||||
types: TypeName+,
|
||||
relations: PredicateName+,
|
||||
operators: OperatorName+,
|
||||
quantifiers: QuantifierName+,
|
||||
structures: StructureName+,
|
||||
inference_rules: RuleExpression+,
|
||||
transition_rules: TransitionRule+
|
||||
}
|
||||
|
||||
HiddenRule ::= {
|
||||
TransitionRule ::= {
|
||||
id,
|
||||
on_event,
|
||||
conditions: Condition*,
|
||||
probability,
|
||||
action,
|
||||
target
|
||||
trigger,
|
||||
preconditions: Expression*,
|
||||
probability: Number[0,1],
|
||||
effects: Expression+
|
||||
}
|
||||
```
|
||||
|
||||
Condition ::= {
|
||||
source: "attribute" | "state",
|
||||
key,
|
||||
operator: "EQ" | "LE" | "GT" | "IS_SET",
|
||||
value
|
||||
The current finite vocabulary includes:
|
||||
|
||||
```text
|
||||
types:
|
||||
Entity, Set, Region, Number, Boolean, State
|
||||
|
||||
relations:
|
||||
EQUAL, NOT_EQUAL, ABOVE, BELOW,
|
||||
MEMBER, SUBSET, DISJOINT,
|
||||
ADJACENT, CONNECTED, CAUSES, LOCATED_IN
|
||||
|
||||
operators:
|
||||
NOT, AND, OR, IMPLIES,
|
||||
ADD, SUBTRACT, COMPARE,
|
||||
UNION, INTERSECTION,
|
||||
MOVE, SWAP, SET, COMPOSE
|
||||
|
||||
quantifiers:
|
||||
ALL, EXISTS
|
||||
|
||||
structures:
|
||||
CHAIN, BRANCH, MERGE, CYCLE, NEST, CONDITION, SEQUENCE
|
||||
```
|
||||
|
||||
Not every primitive must affect every query. The point of the shared world is that many logic domains evolve concurrently and become realistic distractors for one proof-bearing target.
|
||||
|
||||
## Entities and initial state
|
||||
|
||||
```text
|
||||
Entity ::= { id, type }
|
||||
|
||||
WorldState ::= {
|
||||
locations,
|
||||
directed_order_relations,
|
||||
memberships,
|
||||
subset_relations,
|
||||
disjoint_relations,
|
||||
connections,
|
||||
numeric_values,
|
||||
boolean_flags,
|
||||
hidden_generation_attributes
|
||||
}
|
||||
|
||||
action ::= "ADD_RECORD" | "INVALIDATE_RECORD" | "SET_FLAG"
|
||||
probability ::= real number in [0, 1]
|
||||
```
|
||||
|
||||
The grammar is finite, while different rule selections, parameters, event sequences, attributes, and stochastic outcomes generate an unbounded set of behavioral structures.
|
||||
The default 128-entity allocation includes ordinary entities, sets, regions, and numeric counters. Entity IDs are abstract symbols; the renderer must assign stable names within its chosen scenario.
|
||||
|
||||
### State and execution
|
||||
Some initial facts are public, such as locations and counter values. Each has an `I####` audit ID. Latent generation attributes, such as levels used to keep randomly generated order and subset graphs consistent, are stored for audit but removed from the renderer payload.
|
||||
|
||||
Each independent trial starts with:
|
||||
## Event language
|
||||
|
||||
```text
|
||||
record = ABSENT
|
||||
invalidated = false
|
||||
flags = {}
|
||||
WorldEvent ::= {
|
||||
id,
|
||||
time,
|
||||
kind,
|
||||
participants,
|
||||
arguments
|
||||
}
|
||||
```
|
||||
|
||||
Events execute from left to right. For each event, matching rules execute in stored order:
|
||||
|
||||
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:
|
||||
Current realized event forms are:
|
||||
|
||||
```text
|
||||
inactive branch: same state, mass m(1-p)
|
||||
active branch: action(state), mass mp
|
||||
MOVE(entity, origin, destination)
|
||||
RELATE(ABOVE, higher, lower, region)
|
||||
RELATE(MEMBER, entity, set)
|
||||
RELATE(SUBSET, child_set, parent_set)
|
||||
RELATE(DISJOINT, left_set, right_set)
|
||||
RELATE(CONNECTED, left_entity, right_entity)
|
||||
UPDATE_NUMBER(counter, ADD|SUBTRACT, amount, before, after)
|
||||
SET_STATE(entity, flag, before, after)
|
||||
```
|
||||
|
||||
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.
|
||||
Every simulator step selects a candidate transition type. Preconditions are evaluated, then the transition's probability determines whether an event actually happens. Only realized events enter the trace. A fixed seed makes the complete trace reproducible.
|
||||
|
||||
## Behavioral skeleton grammar
|
||||
The default short configuration runs 1000 candidate steps and currently realizes about 400 events. Thus probability controls world evolution, while the resulting event history is an ordinary deterministic collection of facts and changes.
|
||||
|
||||
## Current inference semantics
|
||||
|
||||
```text
|
||||
BehaviorSkeleton ::= {
|
||||
ABOVE(x,y) ∧ ABOVE(y,z) → ABOVE(x,z)
|
||||
ABOVE(x,y) → BELOW(y,x)
|
||||
|
||||
MEMBER(x,A) ∧ SUBSET(A,B) → MEMBER(x,B)
|
||||
MEMBER(x,A) ∧ DISJOINT(A,B) → ¬MEMBER(x,B)
|
||||
|
||||
CONNECTED(x,y) ↔ CONNECTED(y,x)
|
||||
|
||||
numeric updates execute in timestamp order
|
||||
later SET_STATE operations replace the prior value of the same flag
|
||||
MOVE replaces the current region of its participant
|
||||
```
|
||||
|
||||
`ABOVE` and `SUBSET` events are generated from adjacent hidden levels. This allows long chains while preventing contradictory cycles. The levels are generator machinery, not observable premises.
|
||||
|
||||
## Query generation
|
||||
|
||||
```text
|
||||
Query ::= {
|
||||
predicate,
|
||||
arguments,
|
||||
time
|
||||
}
|
||||
```
|
||||
|
||||
After simulation, the query builder searches the realized graphs rather than inserting a prefabricated puzzle. Current query families are:
|
||||
|
||||
- `spatial_order`: transitive `ABOVE` proof;
|
||||
- reverse `spatial_order`: a `NO` answer proved by an opposite-direction chain;
|
||||
- `membership_inheritance`: membership propagated through nested subsets;
|
||||
- `membership_disjointness`: inherited membership in one set plus disjointness from the queried set.
|
||||
|
||||
For a requested complexity `k`, the selected proof contains at least `k` realized event IDs. The queried proposition itself must not appear as a direct event. The full record stores both the event IDs and normalized proof facts.
|
||||
|
||||
Current generation checks record that:
|
||||
|
||||
- no event directly states the query;
|
||||
- proof length meets the requested minimum;
|
||||
- proof events are a small fraction of the full history;
|
||||
- simple direct-fact and too-short-proof baselines fail.
|
||||
|
||||
These checks are structural. They should be expanded with executable solver baselines as the benchmark grows.
|
||||
|
||||
## Full skeleton
|
||||
|
||||
```text
|
||||
WorldSkeleton ::= {
|
||||
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,
|
||||
entity_count,
|
||||
simulation_steps,
|
||||
hidden_program,
|
||||
entities,
|
||||
initial_state,
|
||||
events,
|
||||
trials,
|
||||
observed_present,
|
||||
observed_absent
|
||||
final_state,
|
||||
query,
|
||||
answer_options,
|
||||
gold_answer,
|
||||
proof_event_ids,
|
||||
proof_facts,
|
||||
generator_checks
|
||||
}
|
||||
```
|
||||
|
||||
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.
|
||||
`skeletons.jsonl` contains this complete record for reproducibility and auditing.
|
||||
|
||||
The public payload contains:
|
||||
## Renderer boundary
|
||||
|
||||
The renderer receives only:
|
||||
|
||||
```text
|
||||
family, complexity,
|
||||
event_vocabulary, attribute_vocabulary,
|
||||
observation_protocol, support_cases,
|
||||
query_case, answer_options
|
||||
family
|
||||
complexity
|
||||
entity_types
|
||||
initial_observations
|
||||
events
|
||||
query
|
||||
answer_options
|
||||
```
|
||||
|
||||
It never contains:
|
||||
It does not receive:
|
||||
|
||||
```text
|
||||
id, hidden_system, gold_answer,
|
||||
gold_present_probability, latent_trace
|
||||
world id
|
||||
hidden program or transition probabilities
|
||||
latent initial-state attributes
|
||||
complete final state
|
||||
gold answer
|
||||
proof event IDs or proof facts
|
||||
generator checks
|
||||
```
|
||||
|
||||
## Current generated structure
|
||||
The renderer must map every symbol to one stable surface name, preserve all events and their direction and ordering, and produce one chronological fictional history. Every rendered initial fact and event line retains its `I####` or `V#####` audit ID. The evaluator rejects a rendering when any expected ID is absent. The renderer may compress formatting, but it may not summarize away distractors, state hidden rules, expose the proof, or directly assert the queried proposition.
|
||||
|
||||
Every system has at least four interacting rules:
|
||||
## Complexity dimensions
|
||||
|
||||
- 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.
|
||||
The axes are deliberately independent:
|
||||
|
||||
Longer configurations add attribute-gated add or veto rules. Support evidence includes:
|
||||
```text
|
||||
length minimum gold-proof events
|
||||
entity_count total typed entities
|
||||
simulation_steps candidate evolution steps
|
||||
event_count realized events; measured after simulation
|
||||
```
|
||||
|
||||
- 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.
|
||||
Named proof presets are `short=4`, `medium=6`, and `long=8`. The task file separately controls world size and simulation duration.
|
||||
|
||||
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.
|
||||
## Planned extensions
|
||||
|
||||
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.
|
||||
The IR is intended to grow without changing the visibility boundary. Useful next additions include:
|
||||
|
||||
## 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` | 4 |
|
||||
| `medium` | 6 |
|
||||
| `long` | 8 |
|
||||
|
||||
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.
|
||||
|
||||
## Renderer obligations
|
||||
|
||||
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.
|
||||
|
||||
It must not:
|
||||
|
||||
- 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.
|
||||
|
||||
Retaining the complete pre-render record makes rendering fidelity independently auditable.
|
||||
|
||||
## Extension points
|
||||
|
||||
The next DSL extensions can remain compatible with the three-layer boundary:
|
||||
|
||||
- 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.
|
||||
|
||||
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.
|
||||
- relation deletion and expiry;
|
||||
- explicit event causation chains;
|
||||
- multi-effect transactions and conflict policies;
|
||||
- union and intersection queries;
|
||||
- quantified `ALL` and `EXISTS` questions;
|
||||
- temporal queries about intermediate rather than final state;
|
||||
- counterfactual interventions;
|
||||
- executable nearest-neighbor, keyword, local-window, and shallow-proof baselines;
|
||||
- renderer fidelity verification against every source event.
|
||||
|
||||
Reference in New Issue
Block a user