Publications

Proposes FlowReg, a neural ODE-based regularization method for reinforcement learning that aligns an agent's latent representation with the underlying environment dynamics by modeling MDP trajectories as ODE flows. Integrated into Actor-Critic algorithms, it improves performance across Atari environments.

Presents a reinforcement learning framework for proof search in the Tamarin security protocol verifier, inspired by AlphaZero and AlphaProof. A stateless Tamarin API exposes proof search as a classical RL environment, in which Monte Carlo Tree Search is guided by a neural heuristic that learns from completed subproofs. Across 16 case studies, it finds more proofs automatically than Tamarin's standard search and produces shorter proofs than both the standard and human-engineered heuristics.

Tackles both sides of reactive synthesis. Algorithmically, it couples large reasoning models with model checkers to iteratively repair a synthesized Verilog implementation through sound symbolic feedback, solving more benchmarks than the best dedicated tools in the annual synthesis competition and extending to parameterized systems. On the specification side, an autoformalization step shifts the task from temporal logic to natural language, evaluated on a hand-authored dataset of natural-language specifications.

Introduces NeuRes, a neuro-symbolic approach to propositional satisfiability that combines certificate-driven training with expert iteration. By deriving resolution proofs and satisfying assignments in parallel, NeuRes learns more data-efficient representations than classification-only models like NeuroSAT, requiring orders of magnitude less training data.

Presents FLoBC, a generic decentralized federated learning system built on blockchain, supporting any gradient-descent-compatible model. Benchmarks a trainer/validator design and reward-penalty policy, showing the decentralized system matches (and marginally outperforms) centralized training.

Bridges the two standard ways of applying deep learning to reactive synthesis — reinforcement learning, which converges slowly, and supervised learning, which explores little. The model is initialized by supervised learning and then trained further by reinforcing formally verified predictions, so it learns to synthesize correct solutions rather than fixate on the supervised data. The same signal optimizes for circuit size without degrading performance, and can iteratively reinforce on open problems that existing synthesis tools cannot solve.

Introduces Contrastive Neural Model Checking (CNML), which uses the model checking task itself as the guiding signal for representation learning. A self-supervised contrastive objective jointly embeds logical specifications and systems into a shared latent space. On industry-inspired retrieval tasks, CNML outperforms algorithmic and neural baselines in both cross-modal and intra-modal settings, and the learned representations transfer to downstream tasks and generalize to more complex formulas.

Uses a 2-stage variant of U-Net to split object skeletonization into two sub-problems, shape minimization and corrective skeleton thinning, producing results visually better than the baseline SkelNetOn model. Proposes M-CCORR, a metric based on normalized correlation coefficients, as an alternative to F1 for this task: it handles the class imbalance and avoids F1's over-sensitivity to pixel shifts.

A survey of theoretical complexity: how computation is abstracted by Turing machines, the problem classes P and NP and the relationship between them, and problem reduction as a tool for comparing hardness. Presents Boolean satisfiability at the center of the NP-complete problems along with tractable and intractable variants such as Horn-SAT and 3-SAT, then establishes polynomial-time reductions from 3-SAT to Clique Finding, Hamiltonian Cycle Finding, and 3-Coloring.