I build AI for formal methods.

Researcher in Nairobi, Kenya working at the intersection of LLMs and theorem proving: grammar-constrained decoding, kernel-in-the-loop training, and RL environments where every generated proof step reaches the judge. Background in mechanistic interpretability — I like knowing what the model is doing on the inside.

CV sngugi.research@gmail.com github rss

Writing

2026

A Quarter of Your Prover's Tokens Never Reach the Judge Aug 22

Grammar-constrained decoding makes 100% of generated Lean tactics parseable at zero latency cost — while hallucination stays at ~50%. That asymmetry is the point.

Lean's Tactic Language Is Smaller Than It Looks Aug 22

We built a 53-production context-free grammar for Lean 4 tactics and measured it against every tactic line in Mathlib: 99.86% coverage. The methodology transfers to Rocq and Isabelle.

2025

Taming Incidental Polysemanticity in Toy Models Oct 19

Do training choices shape feature entanglement? SAE-based measurements across regularization, init, activations and noise — L2 beat L1 by 17.9%.

Research

Surgical Knowledge Rewrite in Compact LLMs: An 'Unlearn-then-Learn' Strategy with ((IA)³) arXiv · Aug 2025

Locate a fact's circuit first, then unlearn-then-learn with (IA)³: 98.5% edit accuracy on Phi-3-mini while control-fact retention more than triples versus direct fine-tuning (72% vs ~20%) — and suppressed knowledge stays latent, not gone.

Targeted Lexical Injection: Unlocking Latent Cross-Lingual Alignment in Lugha-Llama via Early-Layer LoRA Fine-Tuning arXiv · Jun 2025

Swahili–English alignment was already near-perfect inside Lugha-Llama at Layer 2 (cosine 0.99998) — just lost by the output layer (0.32). Early-layer contrastive LoRA brings it back: +28%, generalizing to unseen words.

Now

Building RL environments for formal methods — closed training loops where a grammar-constrained generator talks to a real Lean kernel and every contact becomes step-level learning signal.