reasonable-reflection

A Rational Defense of Reasonable Reflection (LICS'26 Keynote)

Artifacts

• 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 verify across three instantiations), placing the LLM behind a kernel-style gate
• lean-grey: abstract reflective tower in Lean 4 with execute-at-metalevel and 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: each base-apply modification carries its own CE proof, and chains of admissions compose, CE-preserving (guardedExt_stack_soundForCE, disjoint-guard second install). On top of the single worked modification there is now an open family of admissible modifications proved conservative once (guardedExt_soundForCE_first_install_tower), with a two-lemma per-proposal cost and provable refusals for guards that would hijack defined behavior (no_guardSpec_closureq) — proposed by an LLM and gated by the Lean kernel end-to-end from inside Lean (lake exe booth)
• 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, Approval whose constructor is the gate, transitive composition, with Wand 1998 as the worked counter-example (gated_preserves_beta for any admission; malicious_not_CE for the β-breaking modification)
• lean-refl-beta: β is a refinement, not an equivalence, under reflection, in ~140 self-contained lines — application is meta-level-mediated and stalls at the top of the tower where the β-contractum doesn't, so the redex (λx.x) 0 gets stuck where let x = 0 in x still runs (beta_refinement_not_equivalence); a minimal model of lean-sage's beta_not_unconditional_CtxEquiv
• lean-keep: the reflective-depth axis in isolation — who gates the gate? A tower in which each level's gate is itself replaceable through the gate one level up, with safety of the whole stack as one theorem (tower_safe)
• lean-loeb: a system that internally trusts a successor checker — "whatever it proves is true," plus "it proves whatever I prove" — is already inconsistent (checker_swap_collapse, via Löb over a real arithmetized provability predicate; the successor bears no assumptions, so the collapse lives entirely in the predecessor's beliefs), hence a consistent system that delegates provably loses proof strength (trust_forces_descent); the blocked half of lean-keep's tower_safe
• 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 extended with an LLM that proposes rewrites, each gated by a Lean kernel check (accepted only if Lean discharges the equivalence)
• analyzer-climber: the gate governs static-analysis knowledge — an analyzer treats clampIndex as unknown (⊤) so an array-bounds proof fails, until it admits a certified abstract transfer for it (off-by-one rejected by offByOneClamp_unsound, ⊤ sound-but-useless, precise [lo,hi] sound-and-useful); one certified summary then verifies every later client with no new proof
• lean-eureka: EURISKO's reflection behind a fixed LCF-style gate — heuristics are arbitrary untrusted metaprograms (LLM-written, birthing heuristics in turn, worth-scored by an agenda economy), and corpus soundness under unrestricted heuristic birth is one axiom-free theorem in the small model the runtime instantiates (discovery_sound; ungated, one firing collapses; gating births buys policy, not soundness). In the running system, invented vocabulary is grounded with kernel-checked alias certificates — the matroid synonym tower closed in-process (is_loop_def ↔ Matroid.IsLoop via Matroid.singleton_dep) — and library lemmas compose into certified facts the grounding pass leaves unmatched
• formal-disco: a framework for scalable, distributed discovery systems, generating hundreds of thousands of verified programs in Dafny, Verus, and Frama-C that can be used for training boosting one-shot performance
• formal-disco/lean-eurisko: an experimental branch on top of formal-disco for a EURISKO-inspired discovery system in Lean
• Henri --self: a self-editing agent with a memory of past guarantees