Research and Investment

본 포스트는 Programming Z3를 읽고 정리한 내용입니다.

링크 : http://theory.stanford.edu/~nikolaj/programmingz3.html

1. Introduction

Z3는 background theories를 해결하기 위한 specialized 알고리즘들을 갖춘 SMT solver

  * SMT(Satisfiability Modulo Theories) : SMT problem은 고전적인 1차 논리로 표현되는 background theories(arithmetic, bit-vectors, arrays 등)의 조합과 관련된 logical formulas에 대한 decision problem

    SMT는 constraint satisfaction problem의 한 형태로 생각할 수 있으므로, constraint programming에 대한 공식화된 접근 방식

  출처 : https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

Tutorial의 목적

  1) Z3의 available한 feature는? 어떤 용도로 설계됐는가?

  2) Z3에서 사용되는 underlying 알고리즘은 무엇인가?

  3) Top of Z3에서 어떻게 어플리케이션을 프로그래밍할 수 있는가?

Z3 System Architecture

Z3는 2가지 interface를 제공

  SMT-LIB2 : 텍스트 파일 또는 pipe로 제공되는 스크립트

  C : C-based API를 통한 호출

Architecture 내 기능

  Formulas : draw from symbols whose meaning are defined by a set of Theories

  Solvers : provide services for deciding satisfiability of formula

  Tactics : provide means for pre-processing simplification and creating sub-goals

  Optimization : services allow users to solve satisfiability modulo objective functions to maximize or minimize values

Sort : Z3에서의 type

In

지난 2019년 겨울, 서울에서는 AI Summit 2019라는 세미나(행사)가 있었다.

해당 세미나는 일반적인 학회 대비 가격이 상당하여 가는데 주저하게 됐었다. 약 80만원 정도였던가..

하지만, 프로그램 자체가 현업에서의 AI 적용 사례를 알 수 있을 것으로 판단하고 세미나를 신청하였다.

(AI Summit 홈페이지를 가면 첫 화면에 내가 질문하는 사진이 나온다 하하)

'솔트룩스'라는 회사는 바로 이 때 알았다.

솔트룩스의 이경일 대표이사님께서 

유레카! 증강지능에서 AI 성공 해답을 찾다

라는 주제로 강연을 하셨는데, 내용이 참 인상깊었었다.

특히, 설명 가능한 인공지능(Explainable AI) 관련 기술 소개도 해주셨는데 나는 그 때 처음으로 해당 기술을 알았다.

지금은 과기부, 산자부에서 펀딩된 상당 수의 과제 뿐 아니라 심지어 한화시스템과 같은 방산업체들도 설명 가능한 인공지능 기술들을 다루고 있으나 그 때는 그 정도로 알려지지 않았을 때였다.

지금은 한글로 된 도서도 나왔더라.

아무튼 너무 재미있게 설명해주셔서, 끝나고 관련하여 질문도 했었던 기억이 난다.

(질문을 잘 받아주셨어서 감사했다.)

이 때부터 솔트룩스라는 회사(사실 회사보다는 대표님)에 관심을 갖고 있었고,

얼마지나지 않아서 IPO 후 코스닥에 상장을 했다.

IPO 당시 다른 일들이 있었어서 청약은 하진 못했었다.

2020년 9월 즈음이던가 연구실 내에서도 설명 가능한 인공지능 관련 과제 얘기가 나와서 다시 회사를 찾아 분석해봤고, 꽤 많은 정부 과제/사업들을 수행한다는 뉴스들을 접할 수 있어서 바로 투자를 하였다.

(투자 후 얼마 안지나서 40% 정도 올랐었는데 글을 쓰고 있는 지금 시점에는 3만원 정도에서 횡보중이다.)

국내에 몇 안되는 기술로 승부를 볼 수 있는 인공지능 기업으로 판단되기 때문에 길게보고 투자하는 중이다.

* ICRA 2021 Workshop on Digital Twins for IMR Robots

아래 youtube 영상을 보며 정리한 자료입니다.

https://www.youtube.com/watch?v=DL3NwhLQveo 

IMR Robot을 위한 챗봇 서비스(?)

채팅 창에 드론의 상태, 위치 등을 물으면, 그에 대답하는... Explainable AI 기술도 활용했다고 함

관련 기술 링크는

https://orcahub.org/innovation/technology-spotlights/miriam

Cyber Physical Fabric

: Federating Digital Twins

WiFi CSI Survey

https://dl.acm.org/doi/abs/10.1145/3310194?casa_token=y1CEIPyF7O8AAAAA:uD8D4J1MrmCrpbocjHaZvUTO9hY6trVPM31G4gHMIgbHqMMX6hQ1YlFQ5UdnejC1KGhfEJCWPw 

5G CSI Estimation

https://ieeexplore.ieee.org/abstract/document/8395053?casa_token=hwTZVTZz9tgAAAAA:zYDuyPkTMgVfezRGo992x1jyYOWVUXtF4CczQfqN6lNxLsOm52or-THRcWzmviyV18XQVkc 

https://ieeexplore.ieee.org/abstract/document/9206084

* Positioning Method 정리

https://www.bitcraze.io/category/lighthouse/

Swarm positioning using lighthouse

https://www.youtube.com/watch?v=K1qmc8K3RUA 

https://www.dynsyslab.org/vision-news/

https://github.com/utiasDSL

실시간 음향 처리를 위한 python module 사용법

참조한 youtube link

https://www.youtube.com/watch?v=AShHJdSIxkY 

PyAudio는 cross-platform 오디오 I/O 라이브러리인 PortAudio에 대한 Python 바인딩을 제공한다.

PyAudio는 Python을 통해 Linux, Windows, Mac OS와 같은 다양한 플랫폼에서 오디오를 쉽게 재생/녹음할 수 있는 기능을 제공한다.

http://people.csail.mit.edu/hubert/pyaudio/

CHUNK : the (arbitrarily chosen) number of frames the (potentially very long) signals are split into in this example

rate : Sampling rate

Channels : number of channels

format : Sampling size and format

input : Specifies whether this is an input stream

output : Specifies whether this is an output stream 

PyAudio와 librosa 같이 설치하기

Anaconda install

conda env 생성 후,

pip install librosa

conda install pyaudio

https://stackoverflow.com/questions/33513522/when-installing-pyaudio-pip-cannot-find-portaudio-h-in-usr-local-include

본 과제에서 요구하는 기능은 풍물/사물놀이 음향 데이터(form 마이크)를 받았을 때 harmonic과 percussive를 나누어 이를 활용하여 드론을 제어하는 것

컴퓨터에 연결된 blue yeti 마이크를 input channel로 audio stream을 받아서 이를 실시간으로 처리함

관련 코드

class AudioHandler(object):


    def __init__(self):
        self.FORMAT = pyaudio.paFloat32
        self.CHANNELS = 1
        self.RATE = 44100
        self.CHUNK = 1024 * 2
        self.p = None
        self.stream = None
        self.WAVE_OUTPUT_FILENAME = "output.wave"
        self.RECORD_SECONDS = 5
        self.frames = []
        self.data = []
        self.arr = np.array([])
        self.recording = True


    def start(self):
        self.p = pyaudio.PyAudio()
        self.stream = self.p.open(format=self.FORMAT,
                                  channels=self.CHANNELS,
                                  rate=self.RATE,
                                  input=True,
                                  output=False,
                                  stream_callback=self.callback,
                                  frames_per_buffer=self.CHUNK)

audio stream을 실시간으로 처리하기 위하여 stream_callback 활용, callback 함수를 call함

    def callback(self, in_data, frame_count, time_info, flag):
        numpy_array = np.frombuffer(in_data, dtype=np.float32)
        y_harmonic, y_percussive = librosa.effects.hpss(numpy_array)
        self.arr = np.append(self.arr,y_percussive)
        print(sys.getsizeof(self.arr))

해당 callback 함수 내 librosa 라이브러리를 활용하여 percussive audio data 구분

librosa.effects.hpss의 input은 numpy array를 받으며, output 또한 numpy array(harmonic / percussive)

np.append는 numpy array의 append

현재는 mainloop에서 특정 key 입력을 받으면 append된 numpy array를 wav 파일로서 출력하는 형태로 개발함

이 때 사용한 라이브러리는 soundfile

sf.write('output_percussive.wav',self.arr,self.RATE)

--> 마이크로부터 실시간으로 들어오는 audio stream을 time window로 구분, 구분된 stream의 평균 audio 세기에 따라 드론이 움직이는 함수 추가 개발 예정

2021.06.30. 추가

Real-time audio segmentation 관련 참조

https://github.com/tyiannak/pyAudioAnalysis

참조 블로그

https://hyongdoc.tistory.com/400?category=884319 

https://dacon.io/competitions/official/235616/codeshare/1305?page=1&dtype=recent 

https://sanghyu.tistory.com/45

사물놀이 주파수 관련 논문

https://www.kci.go.kr/kciportal/ci/sereArticleSearch/ciSereArtiView.kci?sereArticleSearchBean.artiId=ART001315664 

https://www.dbpia.co.kr/Journal/articleDetail?nodeId=NODE00536716 

Matplot for display spectrum

https://stackoverflow.com/questions/19181165/matplotlib-figure-as-a-new-class-attribute-how-to-show-it-later-on-command

https://gist.github.com/sshh12/62c740b329229c7292f2a7b520b0b6f3

MFCC 관련 설명 블로그

* https://brightwon.tistory.com/11

http://keunwoochoi.blogspot.com/2016/03/2.html

https://hyunlee103.tistory.com/45

작년 형이 2019 인공지능 그랜드챌린지에 참가하여 관련 행사에 대해 관심을 갖게 됐다.

인공지능 그랜드챌린지는 과학기술정보통신부가 주최하는 연구개발 과제(이자 대회)로 정부가 도전과제를 제시하고 참가자들이 이를 해결하는 대회 형태의 과제이다. 

우수팀은 후속연구비를 지원받으며 그 금액도 상당하다.

2021년 현재도 해당 과제가 계속 이어지고 있는데, 교수님 말씀으론 과기정통부 내부에서 본 과제에 대한 결과물에 대해 상당히 만족한다고 한달까..

여튼, 2019년은 드론을 application으로 아래의 총 4개의 트랙이 개최됐다.

1. 상황인지 : 드론으로 촬영된 동영상의 내용을 이해하고 분석하기

2. 문자인지 : 드론으로 촬영된 대규모 이미지에서 문자 제시하기

3. 청각인지 : 드론으로 취득된 음성정보에서 구조요청 소리를 듣고 구분하기

4. 제어인지 : 주어진 장애물 세트환경을 자율비행으로 통과하기

4개의 트랙 모두 상당히 난이도가 높았으며 주어지는 데이터셋 또한 적어 직접 데이터를 만들던지 등의 방법이 요구됐다.(물론 제어인지 부분은 약간 다르지만)

여기서 2트랙의 1위를 차지한 기업이 이스트소프트였다.

트랙별 비교가 의미가 있나 싶다만, 4개 트랙에서 가장 높은 성취가 나온 영역 또한 '문자인지'라고 한다.

고등학교에 재학 시절, 이스트소프트에 투자한 적이 있었는데 그 때는 알약과 카발온라인이라는 게임을 보고 투자를 했었다.

그런데 최근에 보니 이스트소프트가 기업의 Vision 자체를 인공지능 기업으로 바꾸고 있었으며 다양한 분야에서 실력을 발휘하고 있었다. (예. GLASS FINDER)

https://blog.est.ai/2019/11/%ec%95%88%ea%b2%bd-%ea%b2%80%ec%83%89-%ec%84%9c%eb%b9%84%ec%8a%a4-glasses-finder/

가장 맘에 들었던 점은 위의 링크처럼 기술 블로그를 제대로 운영하며 자사의 솔루션, 개발기 등을 틈틈이 포스팅하는점이였다.

상당 수 기업들이 자사의 홈페이지조차 제대로 운영하지 않는다는 점에서 매우 맘에 들었다.

그래서 작년 말부터 이스트소프트를 매수하였고, 아직 가지고 있으며 진정한 인공지능 기업으로 거듭날 때까지 함께할 생각이다.

혹시 아는가, 이스트소프트에 취직할 수 있을지도(?)

나의 Main 연구분야가 통신인 점이 참 아쉽다.

2021.09.05 추가 작성

이스트게임즈가 개발, 서비스하는 '카발 모바일'이 필리핀 매출 순위 1위를 했다는 기사를 접했다.

내가 고등학생 때인가? 이스트소프트(이스트게임즈)에서 출시한 카발온라인을 했었던 기억이 있는데,

그게 모바일로 출시되다니.. 게임업계의 IP(Intellectual Property)는 참 재밌다.

https://www.fnnews.com/news/202109020959591211