cv

I build reinforcement-learning environments and tools for formal reasoning.

I'm a 20-year-old self-taught independent AI researcher working on post-training with reinforcement learning, theorem-proving systems, formal methods, and executable verification. I left college to focus on independent research.

CV sngugi.research@gmail.com github rss

Selected writing

An RL Environment Where C Code Has to Be Proved, Not Just Tested RL, formal methods · 17 min
An RL environment where models write C functions and reward comes from proving that the code satisfies a fixed specification, rather than from passing a test suite. The public release includes 64 tasks and an isolated Frama-C judge.
How MathCheck RL Replaces Hidden Answer Keys with Lean-Checked Rewards RL · 19 min
A math RL environment for bounded integer problems that does not store expected answers. Models return an integer or a complete finite certificate, and reward comes from checking that submission against the full encoded problem.
Building a Lean-Backed Verifier for Bounded Mathematical Answers formal methods · 17 min
A verification engine for bounded integer problems. It turns a problem specification and candidate answer into executable Lean code, checks the entire finite domain, and gives a definitive result without requiring a proof from the model.
How a Grammar Changes AI-Generated Mathematical Proof Steps formal methods · 21 min
What changes when a language model is constrained to generate only text shaped like Lean tactics? The study examines how grammar masking prevents malformed proof steps without mistaking valid syntax for a correct proof.
Building a Grammar for AI-Generated Mathematical Proof Steps formal methods · 17 min
A practical study of Lean's tactic language: extracting tactic forms from real proofs, designing a grammar around them, and stress-testing what the grammar accepts and rejects.
Taming Incidental Polysemanticity in Toy Models interpretability · 25 min
How training choices shape feature entanglement in overcomplete toy networks, using sparse autoencoders to compare the representations learned across different configurations and random seeds.

Earlier research

Unlearn, Then Learn: A Circuit-Informed Knowledge-Editing Experiment preprint
An early experiment in changing one factual association in Phi-3-mini: first locate and suppress the original association, then train a replacement. The complete experimental pipeline is public.
Targeted Lexical Injection: Early-Layer LoRA for Swahili–English Alignment preprint
An early experiment using small adapters to strengthen Swahili–English word alignment already present inside Lugha-Llama, evaluated on training pairs and a separate set of unseen words.