Research

We are working on the following research topics. Please feel free to contact Prof. Sang-Ki Ko if you are interested in collaborating. See our full publication list and team members for more details.

Quick links: Neuro-Symbolic Algorithms · Formal Verification of Neural Networks · Next-Generation Neural Networks · Multi-Agent Reinforcement Learning · ML/AI Applications

Neuro-Symbolic Algorithms

At the core of our group is the design of algorithms that combine the rigor of symbolic, automata-theoretic methods with the flexibility of neural learning. Building on a foundation in formal language theory — the descriptional and computational complexity of finite automata and regular expressions, and combinatorial properties of strings (in particular Simon’s congruence) — we develop neuro-symbolic methods that synthesize and infer formal objects, such as regular expressions, from examples.

Active Topics

Neuro-symbolic regular expression synthesis from examples
Regular language inference from positive/negative examples
Descriptional complexity of finite-state automata and regular expressions
Computing the edit-distance of formal languages
Simon’s congruence: closure, neighborhood, and pattern matching on strings and languages
Closest and consensus substring problems for regular languages

Representative Publications

ReSyn: A Generalized Recursive Regular Expression Synthesis Framework, IJCAI 2026 (BK21 Top Conference, IF: 4)
SplitRegex: Efficient Regex Synthesis by Neural Example Splitting, Journal of Automata, Languages and Combinatorics, 2025
Automated Grading of Regular Expressions, ESOP 2023 (BK21 Top Conference, IF: 2)
Existential and Universal Width of Alternating Finite Automata, DCFS 2023; Information and Computation, 2025
Simon’s Congruence Pattern Matching, ISAAC 2022; Theoretical Computer Science, 2024
On the Simon’s Congruence Neighborhood of Languages, DLT 2023
Closest Substring Problems for Regular Languages, Theoretical Computer Science, 2021
Reachability Problems in Low-dimensional Nondeterministic Polynomial Maps over Integers, Information and Computation, 2021

See the full publication list for more.

Formal Verification of Neural Networks

As neural networks are deployed in safety-critical settings, rigorous correctness guarantees become essential. We develop automata-theoretic and model-checking methods for formally verifying properties of deep neural networks (DNNs) and spiking neural networks (SNNs), with an emphasis on scalability, adversarial robustness, and efficient analysis. This direction extends our neuro-symbolic and formal-methods expertise to modern neural models.

Active Topics

Formal verification of deep neural networks and spiking neural networks
Model checking of neural network properties using automata-theoretic techniques
Efficient and scalable verification of neural networks using formal methods
Adversarial robustness analysis of neural networks

Representative Publications

Timestep-Compressed Attack on Spiking Neural Networks through Timestep-Level Backpropagation, AAAI 2026 (BK21 Top Conference, IF: 4)

Next-Generation Neural Network Architectures and Learning Algorithms

We explore neural architectures and training methods beyond conventional deep networks. Our current focus is on spiking neural networks (SNNs) — energy-efficient, biologically inspired models — and on novel learning algorithms such as spike-timing-dependent plasticity (STDP), with attention to training efficiency and adversarial robustness.

Active Topics

Spiking neural networks: architectures and training
Biologically inspired learning rules such as STDP
Timestep-efficient training and inference for spiking neural networks
Adversarial robustness of next-generation neural networks

Representative Publications

Timestep-Compressed Attack on Spiking Neural Networks through Timestep-Level Backpropagation, AAAI 2026 (BK21 Top Conference, IF: 4)
STDP-based Learning for Adversarial Robustness of Spiking Neural Networks, Korea Computer Congress (KCC) 2025

Multi-Agent Reinforcement Learning

We study reinforcement learning for systems of multiple interacting agents — from game-playing agents to coordinated decision-making in complex, dynamic environments. We are particularly interested in scalable multi-agent learning and its use for strategic decision-making, including team-sport scenarios (see Sports Data Analytics).

Active Topics

Multi-agent reinforcement learning in cooperative and competitive environments
Reinforcement learning for game-playing agents
Strategy optimization and decision-making in dynamic, uncertain environments
Multi-agent reinforcement learning for sports strategy

Representative Publications

Modular Reinforcement Learning for Playing the Game of Tron, IEEE Access, 2022
Comparison of Multi-Agent Reinforcement Learning Algorithms in Cooperative Grid Environments, Korea Computer Congress (KCC) 2024
Playing the Game of Tron with Actor-Critic Algorithm in Uncertain and Dynamic Environment, KSC 2021
AlphaQuoridor: A Quoridor Playing Agent based on the AlphaZero Algorithm, KSC 2020

ML/AI Applications

We put the methods above — neuro-symbolic algorithms, deep and spiking neural networks, and multi-agent reinforcement learning — to work on real-world problems. Our two flagship application domains are sports data analytics and AI-driven program understanding and generation.

Sports Data Analytics Using ML/AI

In close collaboration with industry partners, we develop data-driven methods for performance analysis in professional football (soccer), spanning multi-agent trajectory inference from sparse or heterogeneous data, contextual valuation of players and actions, formation and pressing analysis, generative modeling of matches, and reinforcement learning for strategic decision-making.

Active Topics

Contextual player performance evaluation using event and tracking data
Multi-agent trajectory imputation and prediction from event and snapshot data
Generative (language-model-style) modeling of matches for counterfactual player valuation
Ball-free event detection from player trajectories
Football formation and pressing analysis
Player and team valuation from action sequences using large language models
Multi-agent reinforcement learning for football strategy optimization
Transfer fit assessment and player scouting

Representative Publications

Modeling Matches as Language: A Generative Transformer Approach for Counterfactual Player Valuation in Football, ECML PKDD 2026 (KIISE CS Top Conference)
PathCRF: Ball-Free Soccer Event Detection via Possession Path Inference from Player Trajectories, KDD 2026 (BK21 Top Conference, IF: 4)
Valuing La Pausa: Quantifying Optimal Pass Timing Beyond Speed, MIT Sloan Sports Analytics Conference 2026 (Finalist — Top 7 of 200+ submissions)
Imputing Multi-Agent Trajectories from Event and Snapshot Data in Soccer, CIKM 2025 (BK21 Top Conference, IF: 3)
Trajectory Imputation in Multi-Agent Sports with Derivative-Accumulating Self-Ensemble, ECML PKDD 2025 (KIISE CS Top Conference)
exPress: Contextual Valuation of Individual Players Within Pressing Situations in Soccer, MIT Sloan Sports Analytics Conference 2025
Ball Trajectory Inference from Multi-Agent Sports Contexts Using Set Transformer and Hierarchical Bi-LSTM, KDD 2023 (BK21 Top Conference, IF: 4)
SoccerCPD: Formation and Role Change-Point Detection in Soccer Matches, KDD 2022 (BK21 Top Conference, IF: 4)

Programming Language Understanding and Generation

We investigate AI-driven approaches for understanding, generating, and repairing source code. We study code complexity prediction using both structural program representations and deep learning, grammar-based test case generation, contract-satisfying code generation, and the application of large language models to code analysis tasks.

Active Topics

Large language models for code generation, analysis, and repair
Contract- and specification-satisfying code generation
Source code time complexity prediction using deep learning with automata-theoretic analysis
Automated test case generation from formal grammars and logical descriptions
Automated program synthesis and repair
Fault localization and automated code debugging

Representative Publications

ContractEval: A Benchmark for Evaluating Contract-Satisfying Assertions in Code Generation, Findings of ACL 2026
EnCur: Curriculum-based in-context learning with structural encoding for code time complexity prediction, Expert Systems with Applications, 2026
CodeComplex: Dataset for Worst-Case Time Complexity Prediction, EMNLP 2025 (BK21 Top Conference, IF: 3)
LogiCase: Effective Test Case Generation from Logical Description in Competitive Programming, IJCAI 2025 (BK21 Top Conference, IF: 4)
MultiFix: Learning to Repair Multiple Errors by Optimal Alignment Learning, EMNLP 2021 (BK21 Top Conference, IF: 3)