171 lines
9.2 KiB
Markdown
171 lines
9.2 KiB
Markdown
# 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 generated copy of the schema-only review tracked below.
|
|
- `schema-inputs.json`: input hashes; an existing directory rejects changed inputs.
|
|
|
|
Tracked 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.
|
|
- [65-item schema review](reviews/simplex-schemas.html): an owner-approved, self-contained
|
|
HTML view of all 65 source/Lean pairs. It includes schema role descriptions and Lean
|
|
signature expressions, but no textbook paragraphs or full assistant judgment explanations.
|
|
Open the file in a browser after cloning, or download it from the repository; the Git web
|
|
interface may display HTML source instead of rendering it. The JSON indexes above remain
|
|
text-free counts/keys. Full source-inclusive inputs and assessment files remain gitignored.
|
|
|
|
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 \
|
|
--review-page docs/reviews/simplex-schemas.html
|
|
```
|
|
|
|
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.
|