CIDA 연구실은 형식 언어와 오토마타 이론 분야에서 세계적으로 인정받는 연구를 수행하고 있습니다. 형식 언어는 컴퓨터 과학의 이론적 기초를 이루는 분야로, 언어의 구조와 규칙을 수학적으로 정의하고 분석하는 데 중점을 둡니다. 오토마타 이론은 이러한 언어를 인식하고 처리할 수 있는 수학적 모델(오토마타)의 특성과 한계를 연구합니다. 본 연구실은 정규 언어, 문맥 자유 언어, 트리 언어 등 다양한 언어 계층에 대한 복잡도, 편집 거리, 결정 가능성, 상태 복잡도 등 핵심 이론 문제를 다룹니다. 특히, 본 연구실은 오토마타의 기술적 특성(예: 상태 복잡도, 결정성, 비결정성 등)과 언어 간의 관계, 그리고 다양한 연산(삽입, 삭제, 별, 연결 등)에 대한 이론적 한계를 분석합니다. 최근에는 두 언어 간의 편집 거리 계산, 정규 표현식의 자동 평가 및 채점, 예제 기반 정규 표현식 합성, 그리고 오토마타 기반 프로그램 분석 등 실용적 문제에도 이론적 접근을 시도하고 있습니다. 이러한 연구는 국제 저명 학회 및 저널에 다수 게재되었으며, Salomaa Prize 등 권위 있는 상을 수상하는 등 학계에서 높은 평가를 받고 있습니다. 이와 더불어, 본 연구실은 오토마타 이론을 기반으로 한 다양한 응용 연구도 활발히 진행하고 있습니다. 예를 들어, 자연어 처리, 코드 생성 및 분석, 테스트 케이스 자동 생성, 그리고 신경망 모델의 형식적 검증 등 다양한 분야에 오토마타 이론을 접목하여 새로운 연구 패러다임을 제시하고 있습니다. 이러한 연구는 이론과 실용의 경계를 허물며, 차세대 컴퓨터 과학 발전에 기여하고 있습니다.

CIDA 연구실은 스포츠 데이터, 특히 축구 데이터를 활용한 인공지능 및 머신러닝 기반 분석 연구를 선도하고 있습니다. 최근 GPS, 카메라, 컴퓨터 비전 기술의 발전으로 선수 및 공의 실시간 위치 데이터를 대규모로 수집할 수 있게 되었으며, 본 연구실은 이러한 시공간적 데이터를 효과적으로 분석하는 다양한 알고리즘을 개발하고 있습니다. 예를 들어, 선수 트래킹 데이터와 이벤트 데이터를 활용한 포메이션 분석, 선수별 퍼포먼스 평가, 전술 변화 탐지, 그리고 경기 내 다양한 상황(스프린트, 패스, 압박 등)에 대한 맥락적 해석이 주요 연구 주제입니다. 특히, 본 연구실은 딥러닝, 강화학습, 세트 트랜스포머 등 최신 AI 기술을 접목하여 결측 데이터 보간, 궤적 예측, 이벤트 예측, 전략 최적화 등 다양한 문제를 해결하고 있습니다. 예를 들어, 다중 객체의 이동 궤적에서 결측 구간을 보완하는 트랜스포머 기반 모델, 선수별 기대 위협(xT) 및 기대 득점(xG) 지표 산출, PPDA(수비 액션 당 허용 패스 수) 등 첨단 축구 분석 지표의 자동화 및 시각화 기술을 개발하였습니다. 또한, 실제 경기 데이터를 활용한 실증적 연구와 함께, 다양한 국제 스포츠 분석 대회 및 학술대회에서 우수한 성과를 거두고 있습니다. 이러한 연구는 단순한 통계 분석을 넘어, 복잡한 팀 스포츠의 전술적·전략적 의사결정 지원, 선수 영입 및 트레이드 가치 평가, 경기력 향상 등 실질적 현장 적용 가능성을 높이고 있습니다. 나아가, 스포츠 데이터 분석 기술을 타 분야(예: 모빌리티, 군집 행동 분석 등)로 확장하는 연구도 병행하고 있어, 데이터 기반 의사결정의 새로운 패러다임을 제시하고 있습니다.

CIDA 연구실은 인공지능 시스템, 특히 딥러닝 및 스파이킹 신경망(Spiking Neural Network, SNN)의 신뢰성과 안전성을 확보하기 위한 형식적 검증(Formal Verification) 연구를 활발히 수행하고 있습니다. 최근 인공지능의 활용이 확대됨에 따라, 모델의 예측 결과에 대한 신뢰성, 적대적 공격에 대한 강건성, 그리고 시스템의 안전성 보장이 중요한 사회적 이슈로 대두되고 있습니다. 본 연구실은 오토마타 이론, 모델 체크, 논리적 사양 등 형식적 방법론을 접목하여 신경망 모델의 다양한 속성(안정성, 안전성, 적대적 강건성 등)을 체계적으로 검증하는 기술을 개발하고 있습니다. 특히, 스파이킹 신경망은 생물학적 뇌의 작동 원리를 모방하여 에너지 효율이 뛰어난 차세대 인공지능 모델로 주목받고 있으나, 기존의 인공신경망과 달리 시간적 정보 처리와 이벤트 기반 동작 특성으로 인해 검증이 매우 어렵습니다. 본 연구실은 시간 인코딩, 효율적 모델 체크, 대규모 신경망 검증을 위한 이론적 프레임워크 등 새로운 방법론을 제시하여, 기존 한계를 극복하고 실질적인 검증 성능을 달성하였습니다. 또한, 신경망의 구조 최적화, 프루닝, 적대적 공격 탐지 등 다양한 응용 연구도 병행하고 있습니다. 이러한 연구는 인공지능 시스템의 신뢰성 확보와 더불어, 자율주행, 의료, 금융 등 안전이 중요한 분야에서 인공지능의 실질적 도입을 촉진하는 데 기여하고 있습니다. 나아가, 형식적 검증과 인공지능의 융합을 통해 차세대 AI 시스템의 투명성, 해석 가능성, 안전성 보장 등 미래 지향적 연구를 선도하고 있습니다.