Research Statement
B.S. Computer Science & B.S. Computational Mathematics (expected Dec 2026), Pennsylvania State University · Schreyer Honors College
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.
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 models the protocol in a bounded relational encoding under a Dolev–Yao adversary and compiles a typed relational rule-AST to the Tamarin prover (rather than a fixed template), reasoning about the properties studied in the formal 5G literature — the serving-network confusion of Basin et al. (NDSS 2019) and the failure-message linkability of the CCS 2018 analysis. The work is designed to span four standards (5G-AKA, NIST SP 800-63/63B, OWASP ASVS) with an external evaluation on LogicEval. This is in-progress thesis work under submission: I state precisely what is and is not proven, and I am holding quantitative results and the formal-evaluation findings until the paper is peer-reviewed rather than publishing them ahead of review.
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.
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 Signetry, 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.
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.
The thesis artifact is Zenodo/CITATION-ready with a paper under submission; I am glad to share the private repository and working paper with faculty on request. Last updated 2026 · binaydalai.me/research-statement.html