문의현 교수의 연구실에서 발표한 논문 "Parallel Training of GRU Networks with a Multi-Grid Solver for Long Sequences"가 "International Conference on Learning Representations 2022 (ICLR22)"에 게재되었다. ICLR은 Google Scholar 머신러닝 분야에서 세계 랭킹 1위에 올라 있는 세계 최고 수준의 인공지능 학술대회이다.
본 연구에서는 Multi-Grid Reduction in Time (MGRIT) Solver 기술을 활용하여 길이가 매우 긴 시계열 데이터가 주어졌을 때 GRU모델의 학습 과정을 효율적으로 분산 처리할 수 있는 알고리즘을 개발하였다. 본 연구에서 제안하는 parallel-in-time 기반의 새로운 병렬 처리 방식은 아래 그림과 같이 긴 시계열 입력 데이터를 여러 개의 짧은 시계열 데이터로 분할하고 다수의 프로세서에서 짧은 시계열 데이터를 처리하도록 설계되었다. 이를 통해 시계열 데이터 내에서의 지역 정보(local information)를 기본 GRU 모델의 학습 방식에 비해서 정밀하게 인식할 수 있다는 장점이 있다. 제안한 모델이 학습하는 동안 사용되고 갱신되어야 할 파라미터 값은 서로 다른 프로세서들 간에 상호 전달 및 공유할 수 있도록 병렬화 모델을 설계하였다. 더 구체적으로는 MGRIT 알고리즘의 inexact propagation 개념을 GRU 모델에 적용함으로써, 아래 그림과 같이 각 프로세서에서 계산되는 지역 에러(local error)는 fine grid에서 완화(relaxation)시켜주는 과정을 통하여 업데이트되며 전역 에러(global error)는 coarse grid에서 보정(correction)해주는 과정을 통하여 갱신될 수 있다.
이러한 과정을 반복적(recursive)으로 수행해가면서 GRU모델을 학습한다. 본 논문의 실험 결과에서는 HMDB51 비디오 데이터를 이용하여 새로운 모델의 학습 결과가 순차적인 GRU 모델의 학습 방식에 비해 질적인 성능을 보장하면서 최대 6.5배 빠르게 학습이 가능한 것을 보였다. 시계열 입력 데이터의 길이가 길어질수록 본 연구에서 제안한 모델은 학습 시간을 더욱 단축시킬 수 있다는 장점을 가지고 있다.
김필은 교수의 IRAM 연구실에서 진행중인 건설 현장을 위한 자율 주행 시스템을 연구를 소개한다. 로봇은 흔히 지도에 대한 정보를 기반으로 실내 환경에서 정확한 위치를 파악하고 탐색할 수 있다. 일반적인 지도는 건물의 구조적 레이아웃을 포함하지만 위치 파악의 정확도는 비구조적 건물 요소, 즉 문이나 가전제품 및 가구와 같은 일반적인 항목에 의해 크게 영향을 받는다. 이 연구는 센서에 의해 감지된 비구조적 요소에 대한 시맨틱맵을 동적으로 업데이트하여 실내 로봇 위치 파악의 견고성과 정확성을 향상시킨다. 우리는 객체 인식과 지도 업데이트를 전통적인 확률적 지역화로 통합하는 수정된 AMCL (Adaptive Monte Carlo Localization)을 제안한다. 제안된 접근 방식을 통해 로봇은 현재 환경 상태를 반영하는 의미론적 건물 지도을 업데이트하여 비구조적 요소로 인해 발생하는 오류를 자동으로 수정할 수 있다. kinnapped robot과 기존의 localization 시나리오에 대한 평가로 시맨틱 지도 업데이트 기능이 보다 정확하고 강력한 자세 추정을 달성할 수 있음을 보였다.
[그림 1] 건설 현장을 위한 자율 주행 시스템 구조
또 다른 연구의
목적은 모의 건설현장에서 장애물을 감지할 수 있는 센서일체형 건설장비를 모의하는 것이다.
다양한 센서를 이용하여 현장을 정확히 포착하여 상황을 파악하고 상황 정보를 관리인에게 전달할 수 있는 건설장비의 완전 자율주행에 초점을 맞추고자 하였다. 3D 레이저
스캐너와 카메라를 사용하여 가상 픽업 트럭 모델을 만들고 장애물을 감지하기 위해 감지 데이터를 수집 및 처리하는 시뮬레이션에 대한 개요를 제공했다. 로봇
운영 체제(ROS)
프레임워크를 기반으로 통합된 센서를 장착한 픽업 트럭을 생성하여 포인트클라우드 클러스터를 감지하기 위해
PCL (포인트
클라우드 라이브러리) 알고리즘을
적용했다. 사각지대에
있는 작업자와 같은 물체를 인식하는 기능을 통해 혼잡한 건설 현장에서 작업자 안전을 향상시킬 수 있는 가능성을 보여준다. 추가
연구에는 실제 작업장에서 장비의 센서 기반 인식 및 평가를 기반으로 하는 자율 제어가 포함될 예정이다.
길현영 교수의 연구실에서 발표한 논문 "Formal Verification of Blockchain Smart Contracts via ATL Model Checking"이 "IEEE Access" 2022년 호에 게재되었다.
논문 사이트로 이동
이더리움과 같은 최신 블록체인 기술은 스마트 컨트랙트 구현에서 Turing-complete한 프로그래밍 언어를 제공함으로써, 특히 신뢰성이 중요한 금융 분야에 적용되게 하였다. 그러나 스마트 컨트랙트의 사소한 에러들은 금전적으로 막대한 손실을 야기하곤 하는데, DAO 오류, Parity multi-signature 오류, integer underflow/ overflow 오류 등이 그 사례이다. DAO 오류의 경우 5000만 달러 상당의 이더를 도난당하게 하여 이더리움이 이더리움과 이더리움 클래식으로 나뉘게 되는 계기를 만들었다. 이러한 스마트 컨트랙트 상의 오류들을 검출하기 위해 정적 프로그램 분석과 정리 증명기법 기반의 연구들이 진행되어왔으나, 정적 프로그램 분석은 사전에 정의된 패턴의 에러만을 검출할 수 있고, 정리 증명기법 기반 연구는 완전 자동화가 불가능하여 전문가의 참여가 필수적이라는 단점을 갖고 있다. 본 연구는 스마트 트랜잭션의 정확성을 검증하기 위해서, ATL (Alternating-time Temporal Logic) 모델체킹 기법을 이용한다. ATL 모델 체킹이란, 검증 대상인 시스템의 모델과 검증하고자 하는 ATL property가 주어지면, 해당 시스템의 모델이 모든 경우에 주어진 ATL property를 만족하는지를 자동적으로 검증하는 기법이다. ATL 모델체커는 주어진 모델이 property를 만족하는 경우에는 true를 리턴하지만 만족하지 않는 경우에는 counter-example을 알려줌으로써, 개발자가 스마트 컨트랙트의 어느 부분에서 오류가 발생하였는지를 알 수 있게 한다.
[그림 1] ATL model checking procedure for solidity contracts
본 연구에서는 주어진 스마트 컨트랙트를 ATL 모델체커로 검증하기 위해서, 이더리움 스마트 컨트랙트에서 주로 사용되는 Solidity 언어를 ATL 모델체커 MCMAS]의 언어로 정확하게 번역할 수 있는 방법론을 제안하고, DAO Attack, TX.ORIGIN Attack, Safe Remote Purchase Contract 등 3가지 사례에 대한 적용을 통해, 본 연구의 방법론이 실제 스마트 컨트랙트 검증에 성공적으로 사용될 수 있음을 보였다. 또한 본 연구실은 블록체인뿐만 아니라 Service composition, Aircraft systems 등 다양한 Software System의 정확성과 안정성에 대한 검증 연구를 해왔고, 최근에는 인공지능 신경망에 대한 검증 연구를 진행 중이다.