SOUPER 간단 리뷰

SOUPER는 Super Optimization를 약자로 한 프로젝트 입니다. 이런 이름 때문에 오해할 수 있는데, Super Optimization이라고 해서 코드를 "슈퍼향상 시키는 최적화"가 아니고, "자동화 된 최적화" 가 목적입니다. 6^^

 

 

Souper 에 대해 다루기 전에 먼저 자동화 된 최적화를 구현하기 위해서는 최적화를 자동으로 만들 수 있어야 겠죠. 그러자면 자동으로 생성된 "최적화에 대한 검증" 방식이 필요합니다. SOUPER는 CEGIS 방식을 취하는데, 이를 우리나라 말로 옮기면 "반증 기반 유도 합성" 이 됩니다.

 

발견된 최적화 방식에 대해서, "반증 했을 때 만족하는(SAT) 경우가 있는가?" 를 확인하는 방식입니다.

 

 

예를 들어 봅시다.

 

위처럼, 아주 형편없는 예제 코드가 있습니다.

이 코드들은 중간에 나온 블록들처럼, 연산이 합쳐집니다.

 

이 코드에서 SOUPER에서는 어떻게 "최적화를 자동으로 찾아낼 수 있을까?" 요.

 

 

먼저 SOUPER는 각연산에 대한 Cadidates를 만듭니다.

 

\

그리고 Cadidates 들에 대한 다양한 조합을 만들고 이를 SMT 문장으로 만든 뒤 SOLVER에 질의를 합니다. SOLVER가 해당 SMT에 대해 SAT/UNSAT 응답을 주면 이를 통해 최적화가 될 수 있는지 없는지 여부를 판단하게 됩니다.

 

위의 예제에 대해 SOUPER가 생성하는 SMT 문은 아래와 같습니다.

그리고 해당 SMT문을 ChatGPT갓이 해석해준 문장을 덧붙입니다.

 

 

 

SMT/SOLVER는 이 글의 범주를 벗어나니 생략하겠습니다.

 

 

정리요약

 

우리는 이미 코드 예문을 통해 다음과 같은 코드가

e = (a^b) ^ (b^(a^b))

다음과 같이 최적화 된다는 사실을 알고 있습니다.

e = b

 

SOUPER는 위 구문들을 Candiates로 쪼개 하나씩 합성을 하면서 CEGIS 검증을 SMT/SOLVER 로 수행합니다.

위의 코드 구문에서 e = (a^b) ^ (b^(a^b)) 이 e = b 이 되기 때문에 (a^b) ^ (b^(a^b)) == b 이어야 합니다.

 

그러면 반증인 (a^b) ^ (b^(a^b)) != b 이 만족(SAT) 하는 경우가 있는지 검증해서 만족하지 않는다면 위 최적화에 대한 검증이 되는 것이고 이를 통해 자동화 된 최적화를 찾았다고 할 수 있는 것 입니다.