당신이 로봇에게 아주 복잡한 케이크를 굽는 법을 가르치려 한다고 상상해 보세요. 아주 새롭고 신비로운 레시피 북을 사용해서 말이죠. 이 책(딥러닝 라이브러리)은 엄청나게 방대하지만, 설명은 모호합니다. 예를 들어 "밀가루를 넣으시오"라고만 되어 있을 뿐, 설탕의 양에 따라 밀가루를 정확히 얼마나 넣어야 하는지, 혹은 아주 작은 숟가락으로 거대한 그릇의 반죽을 섞으려고 하면 어떻게 되는지에 대해서는 알려주지 않습니다. 만약 당신이 잘못 추측한다면, 로봇은 주방을 엉망으로 만들거나, 더 심하게는 겉보기에는 멀쩡해 보이지만 맛은 끔찍한 케이크를 구워낼 수도 있습니다.

이것이 바로 연구자들이 딥러닝 라이브러리(PyTorch나 TensorFlow 같은)를 다룰 때 직면했던 문제입니다. 이들은 현대 AI를 움직이는 "레시피 북"입니다. 매우 강력하지만 숨겨진 함정(버그)들로 가득 차 있습니다. 문제는 이 라이브러리들의 매뉴얼이 종종 불완전하거나, 여기저기 흩어져 있거나, 혹은 혼란스러운 언어로 작성되어 있다는 점입니다.

여기에 Centaur가 등장합니다. 연구자들이 이 라이브러리들을 테스트하기 위해 개발한 새로운 도구입니다. Centaur를 인간의 창의적인 직관과 컴퓨터의 엄격한 논리를 결합한 초스마트 탐정이라고 생각해보세요.

Centaur의 두 가지 두뇌

Centaur는 "뉴로심볼릭(neurosymbolic)" 방식, 즉 두 가지 서로 다른 사고방식이 함께 작동하는 구조를 가지고 있습니다.

1. "뉴럴(Neural)" 두뇌 (창의적인 탐정): 이 부분은 **대규모 언어 모델(LLM)**을 사용합니다. 이것을 수백만 개의 요리 블로그와 레시피 북을 읽은 아주 박식한 셰프라고 생각해 보세요. Centaur가 특정 함수(예: "두 숫자 더하기")를 살펴볼 때, LLM은 그 규칙을 추측합니다. "이봐요,"라고 LLM이 말할 수 있습니다. "보통 리스트 두 개를 더할 때는 크기가 같아야 하거나, 하나는 복사해서 붙여넣을 수 있는 단일 숫자여야 해요."

   • 함정: LLM은 창의적이지만 실수를 할 수 있습니다. 그럴듯하게 들리지만 실제로는 사실이 아닌 규칙을 추측할 수도 있습니다.

2. "심볼릭(Symbolic)" 두뇌 (엄격한 수학 교수님): 이 부분은 SMT 솔버(논리 엔진의 일종)를 사용합니다. 이것은 셰프가 하는 모든 추측을 검증하는 엄격한 수학 선생님과 같습니다. 만약 셰프가 "밀가루 5컵과 설탕 2컵을 섞을 수 있다"라고 말한다면, 수학 교수님은 그것이 물리 법칙(또는 이 경우에는 소프트웨어의 법칙)을 어기지 않고 실제로 작동하는지 계산을 통해 확인합니다.

   • 능력: 수학 교수님은 단순히 "예" 또는 "아니오"라고만 답하지 않습니다. 그들은 규칙이 작동한다는 것을 증명할 수 있는 수천 개의 구체적이고 유효한 예시(예: "밀가루 3컵, 설탕 1컵")를 생성할 수 있습니다.

Centaur의 작동 방식 (레시피)

Centaur가 사용하는 단계별 과정을 쉽게 설명하면 다음과 같습니다.

1단계: 추측 게임 (규칙 생성)
Centaur는 "셰프"(LLM)에게 특정 함수가 어떻게 작동해야 하는지에 대한 규칙을 작성하도록 요청합니다. 셰프가 제멋대로 행동하는 것을 막기 위해, Centaur는 규칙이 특정한 논리적 형식으로 작성되도록 강제하는 특별한 템플릿(문법)을 제공합니다. 그러면 셰프는 "두 텐서의 모양(shape)은 같아야 한다"와 같은 규칙을 추측할 수 있습니다.

2단계: 사실 확인 (제약 조건 학습)
그다음 Centaur는 이러한 추측들을 소량의 알려진 "좋은" 입력값(유효한 데이터)과 대조하여 테스트합니다.

• 만약 규칙이 모든 좋은 입력값에 대해 성립한다면, Centaur는 그 규칙을 유지합니다.
• 만약 규칙이 실패한다면, 그 규칙을 버립니다.
• 정교화: 때때로 셰프가 의미가 똑같은 두 개의 규칙을 추측할 수도 있습니다. Centaur는 이러한 중복을 찾아내어 제거하는 특별한 기술을 가지고 있어 혼란을 방지합니다.

3단계: 대량 생산 (퍼징, Fuzzing)
이제 검증된 규칙 목록을 갖게 된 Centaur는 "수학 교수님"(SMT 솔버)을 사용하여 수백만 개의 새로운 테스트 케이스를 생성합니다. 규칙이 수학적으로 증명되었기 때문에, Centaur는 자신이 만드는 거의 모든 입력값이 유효할 것임을 알고 있습니다. 이는 마치 완벽한 케이크 반죽만을 만들어내는 기계를 가진 것과 같아서, 절대 타거나 익지 않은 반죽을 만들지 않습니다.

4단계: 충돌 테스트
Centaur는 이 수백만 개의 완벽한 입력값들을 딥러닝 라이브러리에 집어넣습니다. 만약 라이브러리가 충돌하거나, 멈추거나, 이상한 결과를 내놓는다면, Centaur는 이를 버그로 표시합니다.

이것이 왜 중요한가요?

이전의 도구들은 두 가지 방식으로 버그를 찾으려 했습니다.

• "무작위 투척자": 라이브러리에 무작위 데이터를 던졌습니다. 이것은 눈을 가리고 다트를 던지는 것과 같습니다. 대부분의 다트는 과녁을 빗나가며(유효하지 않은 입력), 이로 인해 많은 시간을 낭비하게 됩니다.
• "코드 판독기": 라이브러리의 소스 코드를 읽어 규칙을 파악하려 했습니다. 이것은 집이 지어지고 있는 동안 설계도를 읽으려는 것과 같습니다. 느릴 뿐만 아니라, 설계도가 엉망이라면 길을 잃게 됩니다.

Centaur는 다릅니다. Centaur는 라이브러리가 어떻게 작동하는지 관찰하여(LLM 사용) 규칙을 학습하고, 그 후 수학을 사용하여 완벽한 테스트 케이스를 생성합니다.

결과 (논문의 주장)

연구진은 가장 인기 있는 두 AI 라이브러리인 PyTorch와 TensorFlow를 대상으로 Centaur를 테스트했습니다. 결과는 다음과 같습니다.

• 정확도: Centaur의 규칙은 94%의 정확도를 보였습니다. 규칙을 틀리거나 실제로 존재하는 규칙을 놓치는 경우가 드물었습니다.
• 효율성: 다른 도구들이 주로 유효하지 않은 입력(테스트에 쓸모없는 것)을 생성했던 반면, Centaur는 98% 유효한 입력을 생성했습니다. 이는 Centa가 불가능한 시나리오에 시간을 허비하지 않고, 거의 모든 시간을 실제 시나리오를 테스트하는 데 썼음을 의미합니다.
• 커버리지: Centaur는 이전의 최고 도구들보다 더 많은 코드 영역을 탐색했습니다. 특히 표면적인 오류가 아닌, 소프트웨어의 핵심 로직에 있는 "깊은" 버그들을 찾아냈습니다.
• 버그 사냥: Centaur를 사용하여 팀은 이 라이브러리들에서 26개의 새로운 버그를 발견했습니다. 이 중 18개가 개발자들에 의해 확인되었습니다. 그중 하나는 논문이 발표되기 전에 이미 수정되었습니다!

"깊은 버그(Deep Bugs)"에 대한 간단한 비유

다리를 상상해 보세요.

• **얕은 버그(Shallow bugs)**는 도로 옆의 구멍(포트홀)과 같습니다. 보기 쉽고 고치기도 쉽습니다.
• **깊은 버그(Deep bugs)**는 주요 지지 빔에 생긴 균열과 같습니다. 겉으로는 보이지 않지만, 무거운 트럭이 지나가면 다리 전체가 무너질 수 있습니다.

이전의 도구들은 주로 포트홀을 찾는 데 그쳤습니다. 하지만 다리가 어떻게 지어졌는지에 대한 복잡한 규칙을 이해하는 Centaur는 지지 빔의 균열을 찾아낼 수 있었습니다.

요약

Centaur는 창의적인 AI를 사용하여 딥러닝 라이브러리의 규칙을 추측하고, 논리적인 수학 엔진을 사용하여 그 규칙을 검증한 뒤 수백만 개의 완벽한 테스트 케이스를 생성하는 새로운 테스트 도구입니다. 이러한 결합을 통해 Centaur는 다른 도구들이 놓칠 수 있는 숨겨진 위험한 버그들을 찾아내어, 우리가 의존하는 AI 시스템을 더 안전하고 신뢰할 수 있게 만듭니다.