Reliable software and Neural Network Lab.

컴퓨터공학과 김지응

신뢰성 소프트웨어 및 신경망 연구실은 컴퓨터공학과에 속해 있으며, 신경망 검증 및 형식 검증 분야에서 활발한 연구를 진행하고 있습니다. 최근 3년간 구글 코리아와 협력하여 양자화 신경망의 정확성을 달성하기 위한 형식적 접근법을 연구하였으며, 삼성미래기술육성재단과 함께 신경망 분해/통합 검증을 위한 원천 기술을 개발하였습니다. 또한, pKVM에 대한 형식 검증과 분산 시스템 검증을 위한 ADO 프로젝트를 수행하였으며, 스마트 계약 자동 합성 도구를 개발하는 등 다양한 연구 프로젝트를 성공적으로 완료하였습니다. 이러한 성과는 국제 학술지 및 컨퍼런스에 다수 발표되었으며, 연구실의 높은 연구력을 입증하고 있습니다.

Smart Contract Synthesis

Quantized Neural Networks

Formal Verification

대표 연구 분야

연구 영역 전체보기

양자화 신경망의 정확성 향상을 위한 형식적 접근

양자화 신경망의 정확성을 높이는 것은 딥러닝 모델의 실용성을 극대화하는 중요한 연구 영역입니다. 이를 위해 정확한 수학적 모델과 형식적 검증 방법을 통해 신경망의 성능을 분석하며, 최적화 기술을 적용하여 실제 환경에서의 활용 가능성을 극대화합니다. 본 연구는 Google Korea와의 협력 하에 진행되며, 양자화된 신경망의 성능과 효율성을 보장하는 데 중점을 둡니다.

모듈형 신경망 검증을 위한 원천 기술 개발

삼성미래기술육성재단과 협력하여 모듈형 신경망의 검증 기술을 개발하는 연구를 진행하고 있습니다. 이 연구는 신경망의 분해와 통합 과정을 형식적으로 검증하여 신뢰성을 높이는 데 목적을 두고 있습니다. 이를 통해 복잡한 신경망 시스템에서도 높은 신뢰도를 유지하며, 다양한 응용 분야에서 안정적으로 활용될 수 있는 기반 기술을 제공하고자 합니다.

주요 논문

발행물 전체보기

ThreadAbs: A Template for Building Verified Thread-local Interfaces with Software Scheduler Abstractions

Jieung Kim, Jeremie Koenig, Hao Chen, Ronghui Gu, Zhong Shao

Journal of Systems Architecture, 2024

SimplMM: A Simplified and Abstract Multicore Hardware Model for Large Scale System Software Formal Verification

Jieung Kim, Ronghui Gu, Zhong Shao

Journal of Systems Architecture, 2024

Building Certified Concurrent OS Kernels

Ronghui Gu, Zhong Shao, Hao Chen, Jieung Kim, Jeremie Koenig, Xiongnan (Newman) Wu, Vilhelm Sjoberg, David Costanzo

Communications of the ACM, 2019

완료된 프로젝트

프로젝트 전체보기

Formal approaches to achieve accuracy of quantized neural network, Korea Model Optimization Program, Google Korea

2023.09.22~2024.09.21

1970년 ~ 1970년

A Fundamental Technology for Modular Neural Network Verification (신경망 분해/통합 검증을 위한 원천 기술 연구), 삼성미래기술육성재단

2023.12.01~2026.11.30

1970년 ~ 1970년

Formal verification on pKVM

1970년 ~ 1970년