Projects

The first formal robustness verification benchmark for surgical skill-assessment neural networks, applying Star-set reachability and bound propagation to a grouped 1D FCN trained on da Vinci robotic kinematics (JIGSAWS dataset).

• Derived a flat reformulation of the grouped FCN architecture that enables compatibility with Star-based verifiers (n2v), with equivalence verified numerically to ~1e-7.
• Certified four property families — sensor-noise tolerance, output-range bounding, segmentation invariance, and monotonicity — across all three JIGSAWS tasks and 5 LOSO folds.
• Ran a cross-verifier study (n2v vs. α,β-CROWN) characterizing a two-regime certifiable horizon: full agreement at T≤60, n2v certifying to T=70, and α,β-CROWN extending certification to T≥200; identified approximation looseness (not memory) as the binding constraint.
• Discovered a formal monotonicity failure: the model provably inverts expert-above-novice skill ordering on held-out data in 3/5 Suturing folds and 5/5 Needle Passing folds — a nominal model failure exposed by verification, not an adversarial artifact.

A DSL extension for BehaVerify that lets users model and verify multi-agent behavior-tree scenarios without hand-coding each agent.

• Designed agent-type templates and an expansion-based architecture that instantiates templates before code generation — leaving BehaVerify's existing code-generation and verification pipeline unmodified.
• Built an expander that substitutes parameters and unrolls quantified specifications, avoiding hard-coding while producing a model the current DSL accepts as-is.
• Demonstrated through case studies that verification results are semantically equivalent, reducing lines of code by up to 58% for a five-agent scenario.

An AI chatbot that answers user questions about Chicago's municipal law using retrieval-augmented generation.