I am a 20-year-old independent self-taught researcher currently focused on post-training via RL, building RL environments, and Formal Verification. I recently dropped out of college to pursue doing research independently.
An RL environment where the model is rewarded based on the results of running Frama-C on generated C code, against a fixed input ACSL specification. Verification includes runtime-safety obligations. A full reward is awarded only when all the proofs succeed and some other integrity checks related to keeping the contract fixed pass. Partial rewards are awarded for successful parsing and the fraction of proof obligations discharged. This is currently a public alpha, with 64 tasks available to play with. The judge is isolated, and some adversarial negative controls are used to test whether the judge rejects incorrect implementations. It also produces reproducible proof evidence that can be re-run. Read the technical article here.
An RL environment for doing bounded mathematical reasoning, that doesn't rely on answer keys in the primary mode of specification. The model either has to give an integer answer, or a complete finite certificate for the answer. The problem specification is frozen, and a checker in Lean is used to compute reward. Read the technical article here.
The engine used for MathCheck RL. It is a verification engine that can be used to check answers to bounded mathematical problems. It works by translating the bounded specification into a check that is run in Lean. It can check exact answers, and complete finite relations. It gives reasons for failure, and can be run on untrusted model outputs in an isolated manner. Read the technical article here.
Grammars for AI Proof Steps: Two articles and some reproducible experiments related to using grammars to guide generation of Lean tactics.
Taming Incidental Polysemanticity in Toy Models: A research note on different training choices and proxies for measuring feature entanglement in toy networks.
These preprints are from earlier in my research journey. My current focus is on RL environments and formal verification.
Targeted Lexical Injection: Experiments on doing lexical alignment between Swahili and English via early layer LoRAs.
Surgical Knowledge Rewrite in Compact LLMs: An early exploration into doing knowledge editing via localizing circuits and using a two stage IA³ approach.
I write some research notes and technical essays on my website.
If you have any questions, criticism, or proposals for research, feel free to contact me via the links on my website.