I'm a Computer Science PhD student at Case Western Reserve University. I make LLM reasoning formally verifiable by pairing language models with SMT solvers and theorem provers, so their outputs can be mathematically checked before anyone has to trust them.
Short version: I teach language models to show their work—then ask a solver to check it.
| Inside the research lab | |
|---|---|
MAIN QUEST |
Turn plausible LLM reasoning into machine-checkable proof |
CO-PILOTS |
SMT solvers, theorem provers, and reliable evaluation |
SIDE QUEST |
Build thoughtful open-source tools like OpenLeaf |
OFFLINE MODE |
Look up at the observable universe and ask smaller questions 🌌 |
prompt ──▶ LLM ──▶ formalize ──▶ solver ──▶ ✓ verified answer
▲ │
└──── repair ◀───────┘ counterexample
| Project | |
|---|---|
| 🌿 OPEN SOURCE | OpenLeaf — a private, local-first LaTeX editor with live PDF preview, SyncTeX, document graphs, and offline storage |
| 🧠 NEURIPS 2025 | Grammars of Formal Uncertainty — when to trust LLMs in automated reasoning tasks |
| ⚡ HIPC 2025 | K⁴ — online log anomaly detection through unsupervised typicality learning |
Generated inside this repository—no sleeping stats server.
while (curious) { question(); formalize(); verify(); share(); }
🐶 Supervised by the very serious research assistant above.