1. 소식
  2. arrow_forward_ios

새 소식

태그
검색
과거 미분류

허충길 교수 연구진, 소프트웨어 검증 기술로 세계 선도

허충길 교수 연구진, 소프트웨어 검증 기술로 세계 선도 LLVM 컴파일러 최적화 자동 검증기 Alive2 개발로 컴파일러 검증 기술 선도 최신 동시성 메모리모델 개발로 동시성 P/G 개발 및 검증 위한 기반기술 선도 허충길 교수 연구진이 마이크로소프트 연구소 및 유타 대학교와 공동으로 LLVM 컴파일러 최적화를 자동으로 검증하는 프레임워크인 Alive2를 개발하였다. Alive2는 컴파일러 실행 중 생성된 최적화 전후 프로그램들의 실행의미 및 이들의 동등함을 수식으로 표현한 후, 마이크로소프트의 자동수식검증기(SMT solver)인 Z3를 사용해 최적화의 올바름을 보이거나, 그렇지 않으면 오류를 찾아낸다. 이때 핵심기술은 프로그램의 복잡한 실행의미를 SMT solver가 쉽게 풀 수 있는 형태로 효율적으로 표현하는 것이다. SMT solver는 수학적으로 엄밀하게 수식의 참/거짓을 체크하기 때문에, Alive2는 오탐(False Alarm)이 거의 없고 테스팅으로는 찾을 수 없는 오류들을 찾아낼 수 있다. 실제로 Alive2는 지금까지 테스팅으로서는 발견할 수 없었던 수십개의 컴파일러 버그를 발견하였으며, Alive2의 온라인 서비스(https://alive2.llvm.org) 는 현재 LLVM 커뮤니티의 코드 리뷰 단계에서 개발자들에 의해 활발하게 사용되고 있다. "Alive2: Bounded Translation Validation for LLVM.", Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, John Regehr. 허충길 교수 연구진이 이스라엘 Tel Aviv 대학과 공동으로, 기존의 동시성 메모리 모델들이 만족하지 못했지만 개발자들이 실질적으로 가정하고 있는 성질인 부분적 무경쟁 보장(Modular Data-Race-Freedom Guarantees)을 만족하는 메모리 모델을 최초로 개발하였다. 부분적 무경쟁 보장은 데이터 경쟁(Data Race)이 일어나지 않는 (부분적인) 메모리 영역에서는 동시성으로 인한 느슨한 행동(Relaxed behavior)이 나타나지 않음을 보장하는 것이다. 연구진은 우선 현실에서 그러한 보장을 깨는 특수한 반례를 찾아내어 엄밀하게는 그 보장이 성립하지 않음을 보인 후, 성능에 크게 영향을 미치지 않는 작은 컴파일러 최적화인 RMW-store reordering을 금지하는 것으로 이 문제를 해결할 수 있음을 보였다. 이를 엄밀하게 보이기 위해 허충길 교수 연구진에서 개발해오고 있는 메모리 모델인 Promising Semantics를 개선한 PS2.1을 개발하였고, 이 모델에서 RMW-store reordering은 성립하지 않지만 부분적 무경쟁 보장은 성립함을 Coq 증명보조도구를 사용해 컴퓨터로 증명하였다. "Modular Data-Race-Freedom Guarantees in the Promising Semantics.", Minki Cho, Sung-Hwan Lee, Chung-Kil Hur, Ori Lahav. 위 논문 2편은 오는 6월 PLDI(Programming Language Design and Implementation) 2021에 발표될 예정이다....
포스트 대표 이미지
포스트 대표 이미지

2021년 2월 우수학위논문상 수상자 선정

우리 학부에서는 매 학기 졸업생을 대상으로 우수학위논문상을 수여합니다. 대학원 졸업논문의 경우 논문 심사 위원들이, 학부 졸업논문의 경우 지도교수가 뛰어난 논문을 선별하여 우수학위논문상 후보로 추천하고, 논문상 심사위원회에서 엄격한 심사를 거쳐 수상자를 선정하고 있습니다. 2021년 2월에는 박사 논문상 수상자 3명, 석사 논문상 수상자 3명, 학사 논문상 수상자 1명을 최종 선발하였습니다. o 박사 논문상 수상자: 유영재 (지도교수: 김건희) 제목: Large Scale Video Understanding with Narrative Description 유영재 학생은 이미지/오디오/영상 을 언어로 설명 혹은 질의응답을 하는 인공지능 기술에 기여하였으며, 자기 지도 학습을 적용하여 영상 인지 능력을 향상시켰습니다. 컴퓨터비젼과 인공지능의 최우수학회인 CVPR, ECCV, AAAI, ICLR 등에 다수의 논문을 발표하였습니다 o 박사 논문상 수상자: 정은지 (지도교수: 전병곤) 제목: Unifying Imperative and Symbolic Deep Learning Execution 정은지 학생은 인공지능 딥러닝 모델을 쉽게 프로그래밍하고 빠르게 수행할 수 있는 새로운 딥러닝 소프트웨어 기술을 연구하여, 컴퓨터 시스템 분야 최우수 학술대회인 NSDI와 EuroSys 등에 제1저자로 연구 논문을 발표하였습니다. o 박사 논문상 수상자: 양영석 (지도교수: 전병곤) 제목: A Flexible Architecture for Optimizing Distributed Data Processing 양영석 학생은 분산 데이터 처리 최적화를 위한 유연한 아키텍처를 연구하여 컴퓨터 시스템 분야 최우수 학술대회인 ATC와 EuroSys에 논문을 발표하였습니다. 연구 결과물은 Apache 재단 Incubator 프로젝트로 선정되었으며, Google Cloud 빅데이터 시스템인 Apache Beam의 공식 Runner로 선정되었습니다. o 석사 논문상 수상자: 김동주 (지도교수: 김건희) 제목: Natural Audio Captioning 김동주 학생은 석사 기간 동안 인공지능 분야에 다양한 연구를 수행하였습니다. 최초로 자연의 소리를 인간의 언어로 설명할 수 있는 모델을 개발하였고, 불균형한 데이터가 혼재한 환경에서 지속적으로 학습하는 문제를 극복하는 연구또한 참여하며 인공지능 최우수 학회인 NAACL, ICML, ECCV 등에 1저자로 2편 공저자로 1편 출판하였습니다. o 석사 논문상 수상자: 이준희 (지도교수: 권태경) 제목: A TLS Downgrade Attack using Spatial Differences in Security Configurations 이준희 학생은 분산된 환경에서 대규모 웹서비스가 CDN과 같은 제 3자에게 보안 설정을 위암할 때 발생할 수 있는 보안 설정의 공간적 차이를 이용한 TLS 다운그레이드 공격을 제안하였습니다. 또한 전세계 7백만개 이상의 도메인을 대상으로 실질적인 위협에 대해 분석하였으며, 관련 연구 결과는 보안분야 우수학술대회인 ASIACCS 2021에서 발표할 예정입니다. o 석사 논문상 수상자: 김종석 (지도교수: 김건희) 제목: Dual Composition Network in Interactive Image Retrieval 김종석 학생은 대화형 이미지 검색 알고리즘에 대한 연구를 수행하였습니다. 기존 방법과 상호보완적으로 성능을 높일 수 있는 방법을 제안하였으며, 이를 바탕으로 인공지능 분야 우수 학술대회인 AAAI에 논문을 발표하였습니다. o 학사 논문상 수상자: 정재훈 (지도교수: 강유) 제목: T-GAP: Learning to Walk across Time for Temporal KnowledgeGraph Completion 정재훈 학생은 자연어 데이터로부터 구조화된 정보를 지식 그래프의 형태로 추출해내고, 사용자 쿼리에 따른 지식 그래프 탐색에 대한 연구를 수행하였습니다. 연구를 바탕으로 자연어 처리 분야 최우수 학술 대회인 EMNLP에 논문을 출판하였으며 KDD에 1편 제출하였습니다....
포스트 대표 이미지
포스트 대표 이미지
포스트 대표 이미지

2020년 Naver Fellowship 수상자 선정

2020년 Naver Ph.D. Fellowship Award 수상자가 선정되어 소식을 전합니다. 1인당 500만원의 장학금을 수여하는 본 프로그램에 올해는 훌륭한 인재들이 많이 지원하였으며, 연구성과 및 논문실적을 기준으로 심사를 하여 총 4명의 박사과정 학생이 그 기쁨을 누리게 되었습니다. 오현섭 학생(지도교수 전화숙)은 세계 최대 IoT 표준단체(OCF)의 IoT 표준기술과 이에 기반한 IoTivity 오픈소스 소프트웨어 플랫폼을 활용하여, 삼성리서치와 함께 OCF-to-Zigbee (O2Z) bridging 표준 기술 개발을 진행하였습니다. 김태욱 학생(지도교수 이상구)은 언어학적 개념을 활용하여 우수한 문장 표현 학습 모델을 개발하고 이를 분석하는 연구를 진행하였습니다. 김병창 학생(지도교수 김건희)은 자연어 생성을 위한 딥러닝 모델을 연구하고 있으며, 최근 챗봇이 생성한 대답의 품질을 향상시키는 연구를 수행 중입니다. 오민식 학생(지도교수 김선)은 세포의 상태 변화를 일으키는 다중 오믹스와 유전자 발현량의 조절 관계를 찾기 위한 다중 오믹스 데이터 통합 분석 방법을 연구하고 있습니다. 장학생으로 선정된 학생들에게 진심으로 축하의 메시지를 전하며, 향후에도 우수한 연구자로 성장하여 좋은 결과를 보여주기를 기대합니다....
포스트 대표 이미지

Qualcomm Innovation Fellowship에 학생 6명 선정

2020년 Qualcomm Innovation Fellowship에 대학원생 6명 선정 AI 분야 가장 혁신적인 논문 20편 선정, 대학원생 저자들에게 장학금 수여 20편 중 10편이 서울대 논문, 그 중 7편이 컴퓨터공학부 논문 AI, 머신러닝, 자율주행 분야에서 가장 우수한 대학 논문을 선발해 저자 학생들에게 조건 없는 장학금을 지급하는 Qualcomm Innovation Fellowship(퀄컴 이노베이션 펠로우십)에서 우리 학부 대학원생 6명의 논문이 선정되어 장학금 400~800만원을 받았다. 퀄컴은 혁신적인 연구를 수행하는 학생들을 격려하기 위해 2009년부터 매년 펠로우십을 운영하고 있으며, 미국과 유럽의 대학에서 시작해 인도와 한국에도 확대하고 있다고 밝혔다. 2020년 처음으로 한국을 대상으로 열린 ‘퀄컴 이노베이션 펠로우십’에서는 150편의 논문이 제출되었으며 서울대 10편, 카이스트 8편, 포스텍 1편, 성균관대 1편을 포함해 최종 20편이 선정되었다. 특히 유재민 학생은 딥러닝 학습 데이터를 추출하는 논문과 그래프 샘플링 연구 논문이 모두 선정되어 유일하게 2개의 펠로우십을 수상했다. https://cse.snu.ac.kr/sites/default/files/node--notice/20210102_%ED%80%84%EC%BB%B4%EC%88%98%EC%83%81%EC%9E%906%EB%AA%85.png 김동주 학생(지도교수 김건희)은 불균형한 데이타가 혼재한 환경에서 지속적으로 학습하는 알고리즘의 문제를 극복하는 연구로 펠로우십에 선정되었다. 김병창 학생(지도교수 김건희)은 챗봇이 대화할 때 의미 없는 내용과 유용한 내용을 구분하게 하는 인공지능 대화 모델을 개발하여 관련 논문으로 펠로우십에 선정되었다. 김재겸 학생(지도교수 김건희)은 추론 시점에 소량의 데이터로 적대적 학습을 진행해 학습된 모델의 도메인 차이 문제를 개선하는 논문으로 펠로우십에 선정되었다. 유재민 학생(지도교수 강유)은 딥 러닝 모델이 학습한 지식을 인공 데이터 형태로 추출하는 논문과 효율적인 그래프 추론을 위해 대용량 그래프를 샘플링하는 논문으로 2개의 펠로우십에 선정되었다. 이수찬 학생(지도교수 김건희)은 사람의 개입 없이 자동으로 모델 구조를 확장하며 여러 종류의 태스크를 순차적으로 배워나갈 수 있는 지속학습 모델을 설계한 논문으로 펠로우십에 선정되었다. 정연우 학생(지도교수 송현오)은 복잡하게 꼬인 데이터에서 데이터를 가장 잘 표현하는 이산 정보와 연속 정보를 분리해내는 방법을 연구한 논문으로 펠로우십에 선정되었다. 서울대학교 AI연구원 장병탁 교수는 “퀄컴과 같은 글로벌 기업에서는 당장 기업에서 활용할 수 없더라도 혁신적인 아이디어를 생각해 내고 도전적인 연구를 하는 학생들에게 지원을 아끼지 않는다.”고 강조하고, “국내에서도 젊은 연구자들의 아이디어에 더 투자해 주기 바란다.”고 당부했다. Qualcomm Innovation Fellowship 2020 홈페이지 https://www.qualcomm.com/research/research/university-relations/innovation-fellowship/2020-south-korea...
포스트 대표 이미지

송현오교수 연구진, 최고 성능의 데이터 증대 알고리즘 개발

송현오 교수 연구진,새로운 데이터증대 기법을 제시하여 인공신경망 실제 적용가능성 크게 향상송현오 교수 연구진(김장현.추원호.정호산 석박통합과정)은 인공신경망의 일반화 성능 및 강건성을 향상하는 데이터 증대 기법 Co-Mixup을 개발하였다고 밝혔다. 구체적으로 Co-Mixup은 다량의 데이터가 주어졌을 때, 각 데이터의 중요한 정보의 양을 최대화하는 동시에 다양한 데이터를 생성하는 것을 목표로 한다 [그림 1]. 연구진은 이를 위해 형식적인 문제를 설계하였고 이를 효과적으로 해결하는 알고리즘을 개발하였다 [식 1]. Co-Mixup은 올해 5월에 온라인으로 개최될 인공지능 최고 학회 중 하나인 ICLR의 구두 발표(Oral) 세션에서 발표될 예정이다. 해당 세션은 올해 ICLR에 제출된 논문 중 약 상위 1%(=53/2997)의 논문에만 주어지는 발표 기회이다. https://cse.snu.ac.kr/sites/default/files/node--notice/20210125_hyunoh2.pngReferences Jang-Hyun Kim, Wonho Choo, Hosan Jeong, Hyun Oh Song, Co-Mixup: Saliency Guided Joint Mixup with Supermodular Diversity, ICLR 2021.기존 데이터 증대 기법이 지니는 임의적 요소를 최적화하는 알고리즘 개발 제한된 학습 데이터로 학습에 효과적인 새로운 데이터 생성 인공신경망의 물체 인식, 위치 탐지, 그리고 강건성 등 다양한 성능을 향상  ...
포스트 대표 이미지

[문병로교수 칼럼] '알파폴드'가 몰고 올 제약 혁명

출처: 매일경제 2021년 1월 22일자 [매경의 창] 2012년 세계이미지인식대회(ILSVRC)에서 캐나다 토론토대 제프리 힌튼 교수 팀이 혁명을 일으켰다. 2등과 에러율 10%포인트 이상 차이로 우승을 해 딥러닝 열풍을 불렀다. 구글 계열사인 딥마인드는 2016년 알파고로 두 번째 혁명을 일으켰다. 딥러닝을 탐색 알고리즘 틈에 끼워넣어 세계 최고의 바둑기사를 이겼다. 딥마인드는 다음 문제로 게임과 단백질 폴딩 문제를 지목했다. 단백질 폴딩은 단백질의 염기서열이 접혀서 만드는 3차원 구조를 알아내는 문제다. 유명한 난제이고, 오늘 칼럼의 주제다. 약물은 저마다 특정 단백질을 타깃으로 한다. 작용을 돕거나 방해한다. 자물쇠와 열쇠처럼 약물의 입체 구조가 단백질의 입체 구조와 잘 맞물려야 한다. 과거에는 경험적으로 "어떤 식물을 먹으면 병이 낫더라"는 식의 정보를 기초로 이런저런 성분을 추출해서 시험해 보는 식이었다. 타깃 단백질이 뭔지 모르고 개발되기도 했다. 대개 지난한 시행착오 끝에 유용한 약이 탄생했다. 이제는 과학이 발전해 질병에 영향을 미치는 단백질의 인과관계 체인을 추적할 수 있게 됐다. 이 과정 중 한 단백질과 입체 구조가 잘 맞는 서열을 만들면 약이 될 가능성이 크다. 그런데 이 3차원 구조 예측 문제가 어마어마하게 어려운 문제라 세기의 도전이라는 별명이 붙었다. 컴퓨터로 후보 서열을 도출한다 해도 예측 정확도가 낮아 일단 실물을 만들어 보면 거의 다 실패한다. 드물게 성공하면 대박이 터진다. 이런 기대감으로 매출 50억원에 100억원 적자가 나는 바이오 기업이 5조원의 시가총액을 가지기도 한다. 1972년 노벨 화학상을 받은 크리스티안 안핀센이 단백질의 아미노산 서열이 전적으로 3차원 구조를 결정할 것이라고 추정했다. 1994년 몰트와 피델리스 두 사람이 예측 기술을 촉진하기 위한 경연대회인 CASP를 오픈했다. 격년으로 대회를 연다. 구조가 알려진 단백질을 학습용으로 제공하고 구조가 파악됐지만 공개되지 않은 단백질의 구조를 추정한 품질로 평가한다. 단백질은 수천~수만 개의 아미노산으로 구성된다. 아미노산 서열에서 예측한 입체 구조와 실제 단백질 구조의 모든 아미노산 끄트머리 위치를 비교해서 유사도 점수가 90 이상이면 대략 맞는다고 간주한다. 알파고가 이세돌을 이긴 2016년까지는 1등이 유사도 40 아래에 머물렀다. 대회를 시작하고 22년이나 흐른 후다. 가이드라인 기준 90을 고려하면 터무니없는 수준이었다. 이로부터 2년 후 딥마인드가 60점 근처의 압도적 점수로 우승한다. 프로그램 이름은 알파폴드이고 딥러닝으로 만들어졌다. 2등은 여전히 40점 아래였다. 놀라웠지만 실용적으로 의미 있는 수준은 아니었다. 2년이 더 흐른 2020년 알파폴드는 92.4라는 놀라운 기록으로 다시 우승했다. 가장 어려운 단백질 모음에 대해서도 87 수준으로 맞혀 집행부에서 알파폴드가 속임수를 쓰지 않나 의심했다고 한다. 17만여 개의 단백질이 포함된 대형 데이터베이스를 사용했다. 이건 바둑과는 산업적 차원이 다르다. 글로벌 제약사들 매출은 1000조원이 넘는다. 후보 약물을 만들기 전에 입체 구조를 컴퓨터에서 거의 파악할 수 있게 돼 신약 개발의 혁명이 일어날 것이다. 신약이 쏟아져 나올 것이다. 우리나라도 컴퓨터 장비에 몇십억 원 정도 투자할 여력이 있는 기업에서는 이 흐름에 동참할 시기가 왔다. 컴퓨터 전공자들이 바빠질 일 투성이다. 수도권정비계획법으로 손을 못 대던 서울대 컴퓨터 관련 학부 정원이 20명 늘었다. 턱없이 부족한 숫자지만 교육부에서 그 불합리한 벽을 처음으로 깼다. 행정부에서 보기 힘든 용기를 보였다. 그래도 서울대 컴퓨터공학부는 70명에 불과하다. 500명이라도 부족하다. 지금 증원을 해도 7~8년은 지나야 그 인력들이 기여하기 시작하니 이미 시간을 많이 잃고 있다. 문병로 교수 ...
포스트 대표 이미지
포스트 대표 이미지