Spaces:
Running
Running
File size: 3,691 Bytes
d86c259 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 | """Small auditable kernel for quantified mathematical certificates.
The kernel deliberately knows nothing about graphops or neural networks. It
checks Horn-style derivations from an explicit trusted foundation. Each
foundation lemma records its full quantified statement and source; each proof
step can only apply a named lemma after every premise has already been derived.
This makes the mathematical trust boundary visible and lets negative controls
prove that deleting a substantive lemma makes the target unreachable.
"""
from __future__ import annotations
from dataclasses import dataclass
from typing import Any
@dataclass(frozen=True)
class Lemma:
identifier: str
premises: tuple[str, ...]
conclusion: str
statement: str
source: str
def verify_horn_certificate(certificate: dict[str, Any]) -> dict[str, Any]:
"""Check a quantified Horn derivation without executing asserted booleans."""
hypotheses = tuple(certificate["hypotheses"])
assert len(hypotheses) == len(set(hypotheses))
lemmas = {
item["id"]: Lemma(
identifier=item["id"],
premises=tuple(item["premises"]),
conclusion=item["conclusion"],
statement=item["statement"],
source=item["source"],
)
for item in certificate["trusted_foundation"]
}
assert len(lemmas) == len(certificate["trusted_foundation"])
assert all(lemma.statement and lemma.source for lemma in lemmas.values())
derived = set(hypotheses)
trace: list[dict[str, Any]] = []
for index, step in enumerate(certificate["steps"], start=1):
lemma = lemmas[step["lemma"]]
assert tuple(step["premises"]) == lemma.premises
assert step["conclusion"] == lemma.conclusion
missing = [premise for premise in lemma.premises if premise not in derived]
assert not missing, f"step {index} ({lemma.identifier}) missing {missing}"
derived.add(lemma.conclusion)
trace.append(
{
"step": index,
"lemma": lemma.identifier,
"premises": list(lemma.premises),
"conclusion": lemma.conclusion,
}
)
target = certificate["target"]
assert target in derived, f"target was not derived: {target}"
return {
"theorem": certificate["theorem"],
"quantifiers": certificate["quantifiers"],
"hypothesis_count": len(hypotheses),
"trusted_foundation_count": len(lemmas),
"derived_step_count": len(trace),
"target": target,
"target_derived": True,
"trace": trace,
"trusted_sources": sorted({lemma.source for lemma in lemmas.values()}),
}
def deletion_controls(certificate: dict[str, Any]) -> list[dict[str, Any]]:
"""Remove each predeclared essential lemma and require proof rejection."""
controls = []
for removed in certificate["essential_lemmas"]:
mutated = {
**certificate,
"trusted_foundation": [
item
for item in certificate["trusted_foundation"]
if item["id"] != removed
],
}
rejected = False
reason = ""
try:
verify_horn_certificate(mutated)
except (AssertionError, KeyError) as error:
rejected = True
reason = type(error).__name__
assert rejected, f"deleting essential lemma {removed} did not fail"
controls.append(
{
"removed_lemma": removed,
"certificate_rejected": rejected,
"failure_type": reason,
}
)
return controls
|