feat(schema): persist and instantiate scoped multi-role relation schemas
This commit is contained in:
@@ -0,0 +1,163 @@
|
||||
# Simplex schema: a semantic relation joining roles
|
||||
|
||||
Here **simplex** means the owner's multi-role relation pattern: one statement relates
|
||||
objects, assumptions and a conclusion. The implementation does not construct geometric
|
||||
simplices, faces, boundaries or a mathematical simplicial complex.
|
||||
|
||||
## The model
|
||||
|
||||
| Concept | Representation | Meaning |
|
||||
|---|---|---|
|
||||
| Reusable role definition | `Role` | A semantic slot type with optional textual type/context and finite `choices` |
|
||||
| Statement/relation pattern | `Simplex` | A named mapping from at least two local aliases to roles |
|
||||
| Object or assumption supplied by a caller | `Fact` | A role plus a non-None value |
|
||||
| Requested result | `Goal` | A role whose value is not supplied yet |
|
||||
| Application to particular objects | `SimplexInstance` | Facts and goals bound by local slot alias |
|
||||
| Explicit composition | A `Simplex` used as a role | A supplied nested pattern; no proof dependency is discovered automatically |
|
||||
| Persistent catalog | `SchemaRegistry` | JSON/SQLite nodes and alias-to-definition references |
|
||||
|
||||
`kind` separates `object`, `fact`, `goal`, `own` and nested `simplex` roles.
|
||||
A role's `attrs.references` may name other aliases in the same simplex; unknown aliases
|
||||
are rejected. These references can describe the objects mentioned in an assumption or
|
||||
conclusion. They are not geometric edges. Their provenance must distinguish manually
|
||||
supplied relationships from incomplete syntactic candidates.
|
||||
|
||||
`type_text` is descriptive Lean/mathematical text, not an executable type checker.
|
||||
`choices` is a finite set of admissible values, not a replacement for arbitrary Lean typeclass
|
||||
constraints. Supplied fact and resolved goal values are checked against explicit choices.
|
||||
No registry method establishes that a string is a proof or that a mathematical premise is true.
|
||||
|
||||
## Concrete example: two groups and a homomorphism
|
||||
|
||||
One schema joins these slots:
|
||||
|
||||
| Local alias | Role | Type/claim | References |
|
||||
|---|---|---|---|
|
||||
| `left` | object | group carrier | none |
|
||||
| `right` | object | group carrier | none |
|
||||
| `map` | object | `left →* right` | left, right |
|
||||
| `bijective` | fact | `Bijective map` | map |
|
||||
| `goal` | goal | `Nonempty (left ≃* right)` | left, right |
|
||||
|
||||
The simplex is this complete relation pattern, not an individual role or an asserted
|
||||
geometric object. `left` and `right` may explicitly reuse the same `role:group` definition
|
||||
while binding to different group objects. Reusing a role definition does not equate their values.
|
||||
|
||||
Run the synthetic, offline example:
|
||||
|
||||
```sh
|
||||
PYTHONPATH=. python3 examples/simplex_registry.py
|
||||
```
|
||||
|
||||
It binds symbolic caller values for the input slots, leaves the goal unresolved, and returns
|
||||
a structurally ready candidate. It does not run a Lean proof.
|
||||
|
||||
## Scope, persistence and reuse
|
||||
|
||||
`SchemaRegistry.set_simplex` assigns every child a scoped key by default:
|
||||
`<schema-key>/slot/<escaped-alias>`. Thus `G` in one theorem is not the same object as `G`
|
||||
in another. Corpus keys also include the frozen annotation hash and item identity.
|
||||
|
||||
To reuse a definition, register it with `set_role` and explicitly pass a `role_keys` mapping
|
||||
to `set_simplex`. The referenced definition must match the supplied role exactly. A shared
|
||||
definition still has distinct occurrence keys for every alias. No role is semantically merged
|
||||
merely because its spelling, type text or keywords resemble another role.
|
||||
|
||||
Keys are immutable within a registry. Identical registration is idempotent; changed content
|
||||
or changed definition references require a new version key. `get_role` and `get_simplex`
|
||||
resolve exact keys, not ambiguous bare names. `search_roles` returns literal-substring candidates
|
||||
for a caller to review; it does not approve semantic reuse.
|
||||
|
||||
Serialization includes names, kinds, context, types, choices, attributes and nested aliases.
|
||||
`role_from_dict` restores JSON snapshots. SQLite uses one connection and one transaction per
|
||||
nested registration, foreign keys and JSON payloads; it does not load archived pickle blobs.
|
||||
Cyclic nesting and failed reuse checks roll back the complete write. Returned objects are
|
||||
restored snapshots; changing one does not silently update a registered definition.
|
||||
|
||||
## Query and binding APIs
|
||||
|
||||
```python
|
||||
from leanbench.schema_registry import SchemaRegistry, slot_key
|
||||
|
||||
with SchemaRegistry("private-registry.sqlite") as registry:
|
||||
schema = registry.get_simplex("schema:example")
|
||||
matches = registry.search_roles("group")
|
||||
containers = registry.find_by_roles(["role:group"], match_all=True)
|
||||
candidates = registry.find_solvable([
|
||||
slot_key("schema:example", "left"),
|
||||
slot_key("schema:example", "right"),
|
||||
slot_key("schema:example", "map"),
|
||||
slot_key("schema:example", "bijective"),
|
||||
])
|
||||
```
|
||||
|
||||
`find_by_roles` searches definition references, including descendants of nested schemas.
|
||||
`find_solvable` retains the archived API name but implements **structural readiness only**:
|
||||
all input occurrences must be supplied and at least one marked goal/own occurrence must
|
||||
remain unresolved. It returns `structural_candidate_only: true`, not a proof or a computed value.
|
||||
Having one `role:group` definition cannot satisfy two distinct group slots. A nested input
|
||||
must itself be explicitly supplied; the registry does not apply its internal theorem automatically.
|
||||
|
||||
`SimplexInstance(schema, facts=..., goals=...)` binds local aliases. Facts and goals must be
|
||||
distinct declared slots. Omitting `goals` uses roles marked `goal` or `own`; `resolve` checks
|
||||
a supplied goal value against choices. Completion means that declared goals have values,
|
||||
not that Lean verified them. Value unification, dependent type checking and proof search
|
||||
remain outside this implementation.
|
||||
|
||||
## Materialization of the 65 P0 items
|
||||
|
||||
The builder consumes the frozen current-chat GPT diagnostic's source descriptions and
|
||||
unchanged Lean strings. It makes no model request, revises no assessment and performs no
|
||||
Lean compilation. Results:
|
||||
|
||||
| Artifact | Count |
|
||||
|---|---:|
|
||||
| Source annotation seed schemas | 65 |
|
||||
| Lean signature schema seeds | 50 |
|
||||
| Items with fewer than two projected Lean roles | 15 |
|
||||
| Stored schemas | 115 |
|
||||
| Scoped role records / slot occurrences | 483 / 483 |
|
||||
|
||||
These 115 seeds deliberately do not auto-reuse definitions across statements. Explicit reuse
|
||||
is supported and tested by the synthetic example; a reviewed shared ontology is future work.
|
||||
The 15 incomplete Lean sides remain in the index with status `insufficient_projected_roles`.
|
||||
A closed declaration may mention concrete objects inside its conclusion that the binder-based
|
||||
projector misses. No object roles were invented to hide this limitation.
|
||||
|
||||
Source schemas are marked `unreviewed_annotation_seed`. Existing `given` tags are preserved
|
||||
with `quantifier_status: unreviewed`; they are not silently converted to universal/existential
|
||||
quantifiers. References on the source side use explicit symbol candidates; Lean references
|
||||
are syntactic identifier candidates. Neither is a complete dependency analysis.
|
||||
For example, P11's source seed lists a named size while Lean uses `Fintype.card G` inline.
|
||||
The materializer preserves both representations; it does not invent a validated cardinality
|
||||
binding or repair the old alignment result. Annotation quality and semantic normalization
|
||||
still require a separate review.
|
||||
|
||||
Private outputs under `experiments/P0-pilot/data/simplex-schemas-v1/`:
|
||||
|
||||
- `registry.sqlite`: queryable catalog with the 115 schemas and scoped slots.
|
||||
- `schemas.json`: all 65 source/Lean pairs, retaining incomplete Lean projections.
|
||||
- `schemas.html`: a local review of all 65 pairs.
|
||||
- `schema-inputs.json`: input hashes; an existing directory rejects changed inputs.
|
||||
|
||||
Tracked, text-free outputs:
|
||||
|
||||
- `experiments/P0-pilot/results/simplex-schema-index.json`: 65 item IDs, schema keys,
|
||||
role counts, coverage status and reference-candidate counts.
|
||||
- `experiments/P0-pilot/results/simplex-schema-summary.json`: coverage, limitations and hashes.
|
||||
|
||||
Replay from the repository root with private inputs present:
|
||||
|
||||
```sh
|
||||
PYTHONPATH=. python3 experiments/P0-pilot/build_schemas.py \
|
||||
--items experiments/P0-pilot/data/simplex-schemas-v1/items.jsonl \
|
||||
--assessments experiments/P0-pilot/data/simplex-schemas-v1/assistant-assessments.json \
|
||||
--key experiments/P0-pilot/labels/key.json \
|
||||
--private-out experiments/P0-pilot/data/simplex-schemas-v1 \
|
||||
--index experiments/P0-pilot/results/simplex-schema-index.json \
|
||||
--summary experiments/P0-pilot/results/simplex-schema-summary.json
|
||||
```
|
||||
|
||||
The original annotations, judgments, Qwen results and matcher thresholds remain unchanged.
|
||||
The registry is a usable schema foundation, not evidence of a validated theorem, a working
|
||||
prover, independently measured faithfulness, or a completed Phase 1 experiment.
|
||||
Reference in New Issue
Block a user