CV - Stanley Ngugi

Research Interests

AI for formal methods: LLM theorem proving, grammar-constrained decoding, verifier-in-the-loop reinforcement learning environments, and agentic proof search. Foundational work in mechanistic interpretability of large language models: knowledge editing, polysemanticity and feature entanglement, circuit analysis, cross-lingual representations in low-resource languages.

Education

Self-directed study — machine learning & mechanistic interpretability 2023 – present

Advanced mathematics for ML (linear algebra, calculus, probability, variational inference), transformer architectures, and PEFT methods, built from first principles through hands-on experimentation.
[Add formal education details here]

Publications & Preprints

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

Technical blog post with artifacts. First application of grammar-constrained decoding (vLLM + llguidance) to Lean tactic generation: 100% syntactic validity at zero latency cost, ~50% more effective RL rollouts, and a documented silent-fallback failure mode in serving stacks.

Lean's Tactic Language Is Smaller Than It Looks 2026

Technical blog post with artifacts. 53-production context-free grammar covering 99.86% of all 144,154 tactic lines in Mathlib; methodology cross-validated on Rocq (98.81%) and Isabelle (95.47%).

Surgical Knowledge Rewrite in Compact LLMs: An 'Unlearn-then-Learn' Strategy with ((IA)³) for Localized Factual Modulation and Catastrophic Forgetting Mitigation 2025

Solo author. arXiv:2508.07075. Circuit-localized two-stage knowledge editing with (IA)³ on Phi-3-mini; 98.50% new-fact accuracy, 96% suppression of conflicting fact, 72% localization accuracy vs ~20% for direct fine-tuning.

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

Solo author. arXiv:2506.15415. Discovered latent near-perfect Swahili–English alignment at Layer 2 of Lugha-Llama-8B-wura; contrastive LoRA fine-tuning improved output-level alignment +28% and generalized to unseen word pairs (p < 7.17 × 10⁻²⁷).

Taming Incidental Polysemanticity in Toy Models: How Network Training Choices Affect Feature Entanglement 2025

Technical blog post with full code. SAE-based measurement of feature entanglement across training configurations; L2 regularization reduced polysemanticity 17.9% vs L1 (p<0.01).

Research Experience

Independent Researcher — AI for formal methods & LLM internals 2024 – present

Built a context-free grammar and corpus extractor for the Lean 4 tactic sublanguage (99.86% coverage of Mathlib; cross-validated on Rocq and Isabelle), then benchmarked grammar-constrained decoding of Qwen2.5-Coder-7B and Goedel-Prover-V2 via vLLM + llguidance.
Designed and ran circuit-localization pipelines to identify components encoding specific facts before targeted PEFT interventions (code).
Built contrastive-learning LoRA training setups targeting empirically identified optimal layers for cross-lingual alignment (code).
Trained toy overcomplete networks and sparse autoencoders to quantify polysemanticity under different regularization schemes (code).

Technical Skills

Languages: Python, Git, SQL (basic)
ML frameworks: PyTorch, Hugging Face Transformers, PEFT (LoRA, (IA)³)
Interpretability: Sparse autoencoders, circuit analysis, activation patching, probing, logit lens
Formal methods & decoding: Lean 4 tactic language tooling, context-free grammar engineering, vLLM structured outputs (llguidance), constrained decoding; Rocq/Isabelle corpus extraction
Data & analysis: NumPy, pandas, matplotlib, statistical testing (scipy)
Infra & tooling: Linux, Jupyter, Weights & Biases, Google Colab / cloud GPUs
Writing: LaTeX, technical blogging, research communication

Languages

English (fluent) · Swahili (native) · [adjust as accurate]

References

Available on request.