Research
My research sits at the intersection of machine learning and formal methods. I am interested in what we can formally prove about deployed neural networks — not just measure on a test set. My current focus spans two threads: building the first formal robustness verification benchmark for surgical skill-assessment networks, and extending behavior-tree verification tools to natively support multi-agent modeling.
Publications
First Formal Robustness Verification Benchmark for Surgical Skill Assessment
2026In preparationTargeting VNN-COMP 2026 · QEST+FORMATS 2026Jamie Fong, Taylor T. Johnson
We present the first formal robustness verification benchmark for surgical skill-assessment neural networks. Using Star-set reachability and bound propagation on a grouped 1D fully-convolutional network trained on da Vinci robotic kinematics (JIGSAWS), we certify four property families across three tasks and five LOSO folds, characterize a two-regime certifiable horizon across n2v and α,β-CROWN, and expose a formal monotonicity failure in which the model provably inverts expert-above-novice skill ordering on held-out data.
Read paper (PDF)Composing Multi-Agent Behavior Trees: A DSL Extension for BehaVerify
2025PreprintVanderbilt UniversityJamie Fong, Taylor T. Johnson
Behavior trees (BTs) are widely used in robotics, but multi-agent verification requires tedious hand-coding because existing BT verification tools do not support native multi-agent modeling. We present a DSL extension for BehaVerify that models multi-agent scenarios through agent-type templates and an expansion-based architecture that does not modify the existing code-generation or verification pipeline. The expander instantiates templates prior to code generation, substitutes parameters, and unrolls quantified specifications. Case studies show that verification results are semantically equivalent while reducing lines of code by up to 58% for a five-agent scenario.
Read paper (PDF)