Research Statement

Binay Dalai

B.S. Computer Science & B.S. Computational Mathematics (expected Dec 2026), Pennsylvania State University · Schreyer Honors College

binaydalai.me · binaydalai.me/research · ORCID 0009-0009-6285-8305 · binaydalai2024@gmail.com

My research sits at the intersection of machine learning, optimization, and formal methods. The through-line is a single conviction: the systems we increasingly delegate decisions to should be systems we can reason about — where behavior traces back to a proof, a constraint, or a measurable landscape rather than to trust in a black box. I am most excited by problems where a learned component and a formal guarantee have to be made to coexist.

Formal verification meets language models

My honors thesis is a corpus-agnostic “Ingest → Catch → Secure” platform that turns cybersecurity standards into machine-checkable logic. A language model extracts normative IF–THEN rules from a raw standard; a formal validity gate (symbol-checking, Z3 satisfiability, and a calibrated fidelity backend) admits only sound, non-trivial rules; and a closed-loop SMT verifier discovers violations under a Dolev–Yao adversary and synthesizes formally-gated mitigations. The design principle is that the model is never trusted — every rule it proposes must clear a solver before it counts.

On the 3GPP 5G-AKA authentication protocol, the platform reproduces two published attacks — the serving-network confusion of Basin et al. (NDSS 2019) and the failure-message linkability of the CCS 2018 5G analysis — as SAT witnesses, and certifies their fixes as non-vacuous UNSAT. A typed relational rule-AST compiles to Tamarin (not a template), proving an SN-binding fix for unboundedly many user equipments, serving networks, and sessions; a faithful SQN desync/re-sync model over a real ordered counter proves replay-rejection and re-sync recovery. Empirically, the fidelity gate improves rule-acceptance F1 from 0.07 (a prior lexical gate) to 0.61 on a 200-pair gold set with blinded dual-LLM annotation and human adjudication; relational extraction reaches macro-F1 0.94. The work spans four standards (5G-AKA, NIST SP 800-63/63B, OWASP ASVS) and includes an external head-to-head on LogicEval (61 real CVEs). Throughout, I state precisely what is and is not proven — the remaining bounds (bounded SQN epochs, an auto-incomplete equivalence, an abstracted key schedule) are named, not hidden.

Optimization and learning dynamics

Earlier, I studied quantum-assisted optimization for transformer architectures (published, IEEE NMITCON 2025). Using the Quantum Approximate Optimization Algorithm to optimize attention-block parameters in a from-scratch transformer, the hybrid quantum-classical pipeline improved efficiency by 43% on representative NLP tasks in simulation, and I analyzed output-weight heat maps and convergence trajectories to characterize where the quantum-assisted step helps. This is where my interest in loss-landscape geometry and optimization dynamics began — the question of why a training process converges the way it does, not just that it does.

Applied ML systems

Alongside the research, I build ML systems that ship. At IBM I develop generative-AI prototypes and watsonx applications, and previously delivered Watson-based services on OpenShift for Fortune 500 engagements. At Lockheed Martin I designed reinforcement-learning policies for dynamic threat-assessment scenarios, reaching an 85% success rate under high uncertainty. Independently I have shipped agent-governance and DevSecOps systems — including umbra-core, an agent-agnostic change-control layer that proves what an AI coding agent was allowed to change with an Ed25519-signed, SLSA/in-toto receipt and an on-disk prompt-injection defense. This applied work keeps my research honest: it is a constant reminder that a guarantee only matters if it survives contact with a real system.

Direction

For doctoral study I want to deepen the seam between learned components and formal guarantees: LLM-assisted verification that remains sound by construction, the geometry of optimization in high-dimensional models, and trustworthy autonomy for agentic systems. I am drawn to groups working on symbolic protocol analysis, neuro-symbolic methods, and the theory of learning dynamics, and I would bring both the formal-methods rigor and the systems-building instinct my recent work reflects.