A Rational Defense of Reasonable Reflection (LICS'26 Keynote)
- llm-meta-level: the meta-level is an LLM proposing modifications to level 0; the 0↔1 boundary is checked by a verifier (sandbox /
tsc/dafny verifyacross three instantiations), placing the LLM behind a kernel-style gate - lean-grey: abstract reflective tower in Lean 4 with
execute-at-metaleveland reflectively-modifiable governance policies; modifications restricted to guard+handler (no closures/heap) - lean-green: meta level realized as a mutable heap cell with closures and causal
set!, plus the CakeML-style value-bisimulation infrastructure for conservative extension (CE) soundness theorem and an LLM proposer/gate cascade - lean-sage: the synthesis — lean-grey's multi-level reflective tower over lean-green's heap/closure/
set!substrate, with a kernel-checked proof-bearing admission gate on top: eachbase-applymodification carries its own CE proof, and admissions compose across the tower - lean-emerald: pedagogical rebuild of lean-sage's proof-bearing CE substrate, 5x smaller
- lean-gate: the kernel-typed-evidence pattern that every artifact in this portfolio instantiates, in ~80 lines — CE predicate,
Approvalwhose constructor is the gate, transitive composition, with Wand 1998 as the worked counter-example (gated_preserves_betafor any admission;malicious_not_CEfor the β-breaking modification) - climbing-calc: type-level proof-bearing admission for a total-functions calculator — Lean's type checker is the schema/operator gate
- climber: gate governs the right to extend the proof system itself (sound axiom-schema extensions, Beklemishev-shaped)
- defeater: non-monotonic dual of climber — gate admits sound exception schemas, governing what gets withdrawn rather than added
- reviser: gate checks rationality of belief-revision operators, not the beliefs themselves
- sc-mini/llm: minimal positive supercompiler, forked with sound LLM-proposed rewrites
- verified discovery system: gate over discovery of theorems and heuristics