(6) 프로그램 디버깅을 돕는 인공지능 - IEEE Spectrum

 

AI-기반 증명 생성기인 Baldur는 자동으로 코드를 확인하기 위해

자체 증명을 통해 소프트웨어 디버깅을 돕습니다. 

모든 소프트웨어가 완벽하지는 않습니다. 

많은 앱, 프로그램 및 웹사이트는 버그가 존재하는 상태로 출시됩니다. 

 

그러나 암호 프로토콜, 의료 기기 및 우주 셔틀과 같은 

중요한 시스템의 소프트웨어는 오류가 없어야 하며, 

버그의 부재를 보장하기 위해서는 코드 리뷰와 테스트를 넘어 

형식적인 검증이 필요합니다.

형식적인 검증은 코드에 대한 수학적인 증명을 작성하는 것을 포함하며, 

"코드가 정확한지 확인하는 데 가장 어렵지만 동시에 가장 강력한 방법 중 하나"입니다. 

이것은 매사추세츠 암허스트 대학의 교수인 Yuriy Brun이 말합니다.

형식적인 검증을 더 쉽게 만들기 위해 Brun과 그의 동료들은 

새로운 AI-기반인 Baldur을 고안했습니다. 

이 방법은 자동으로 증명을 생성하는 데 도움이 됩니다. 

 

관련된 논문은 2023년 12월에 샌프란시스코에서 개최된

ACM Joint European Software Engineering Conference 및

Foundations of Software Engineering에서

발표되어 우수 논문상을 수상했습니다.

 

팀 멤버로

UMass Amherst에서 박사 학위 연구 중인 Emily First,

Google에서 연구를 진행한 전 연구원인 Markus Rabe,

일리노이 대학교 어바나 캠퍼스의 조교수인 Talia Ringer가 함께했습니다.

 

Baldur는 Google의 Minerva 대형 언어 모델 (LLM)에 기반하고 있으며, 

이 모델은 수학 표현을 포함하는 과학 논문 및 웹 페이지에서 훈련되었으며, 

이후에는 증명 및 정리에 관한 데이터로 세밀하게 조정되었습니다. 

 

Baldur는 자체 증명을 생성하기 위해 Isabelle이라는 

증명 보조 또는 자동 정리기와 함께 작동합니다. 

 

Baldur에게 정리 문장이 주어지면 

거의 41%의 확률로 전체 증명을 생성할 수 있습니다.

Baldur의 성공률을 높이기 위해 팀은 모델에 이론 파일에서 

정리 문장 앞의 다른 정의나 라인과 같은 추가적인 맥락 정보를 공급했습니다. 

이를 통해 증명률이 47.5%로 증가했습니다. 

 

이는 Baldur가 맥락을 이용하여 

새로운 정확한 증명을 예측할 수 있다는 것을 의미합니다. 

 

프로그래머가 특정 메서드가 주변 코드 및 

동일한 클래스의 다른 메서드와 어떻게 관련되어 있는지를 알 때 

해당 메서드의 버그를 수정하는 데 더 잘 갖춰져 있는 것과 유사하게, 

Baldur은 추가적인 맥락으로 더 나은 성능을 발휘할 수 있습니다.

현재 자동 증명 생성의 최첨단 도구인 Thor는

57%의 높은 증명률을 가지고 있습니다. 

 

Baldur의 강점은 전체 증명을 생성할 수 있는 능력에 있습니다. 

 

Thor는 가능한 증명 공간을 탐색하는 

작은 언어 모델과 결합된 메서드를 사용하여 

증명의 다음 단계를 예측합니다. 

 

그러나 Thor와 Baldur(북유럽 신화에서 Thor의 형제)가 함께 작동할 때, 

이 두 모델은 거의 66%의 시간 동안 정확한 증명을 생성할 수 있습니다.

팀은 또한 Baldur가 자체 증명을 "수리"할 수 있다는 것을 발견했습니다. 

이전에 실패한 시도와 Isabelle이 반환한 오류 메시지를 제공하면

 Baldur은 잘못된 증명을 올바른 것으로 바꿀 수 있습니다.

"Baldur이 오류 메시지가 이렇게 큰 도움이 되는 것은 놀랍습니다,"

라고 Brun은 말합니다.

 

 "이것은 더 나은 답을 제공하기 위해 대형 언어 모델에 제공할 수 있는 

더 유용한 정보가 더 많다는 것을 나타냅니다. 

우리는 겉만 긁어본 것에 불과합니다."

팀은 모델에게 유용하다고 생각되는 정보의 정확한 양을 아직 찾지 못했습니다.

 "한 가지 제한 사항은 생성하려는 증명 주변의 일부 정보를 제공하고 있지만 

어디서 유용하지 않게 되는지를 알지 못합니다" 라고 Brun은 말합니다. 

 

그리고 여전히 상당한 정도의 오류가 있으며 보다 설명이 더 잘 되어 있는 

데이터셋을 사용하여 모델을 세밀하게 조정함으로써

개선될 수 있을 것이라고 기대합니다.

 

다음 단계로 Baldur를 다른 증명 보조에 적용하고

모델의 정확도를 향상시킬 수 있는

맥락 정보를 더 스마트하게 수집하는 방법을 찾고 있습니다.

 

팀은 Baldur가 증명 엔지니어들의 작업을

단순화하는 데 도움이 되도록 기대하며,

이들 엔지니어들은 미국 국방부 및

국방 고등 연구 계획국 (DARPA)과 같은 기관에서

국가 안보 시스템의 형식적인 검증과 같은 작업을 수행합니다.

전반적으로 팀은 소프트웨어 개발자들로부터 Baldur와 같은 도구가 

코드에서 오류를 디버깅하거나 명세를 정제하거나 

더 높은 품질의 시스템을 만드는 데 

어떻게 도움이 될 수 있는지에 대한 피드백을 받기 위해 노력할 계획입니다.

Brun은 "개발자가 코드의 특성 중 일부를 증명하려고 노력하는 상황에서

상호 작용하는 도구를 구축하는 데는 많은 힘이 있습니다.

이러한 도구와 상호 작용하는 방법을 이해하고 자동 접근 방식을 통해

개발자를 지원하는 것은 더 나은 결과를 이룰 수 있습니다" 라고 말합니다.

 

*댓글과 공감, 광고 클릭은 계속해서 기록들을 이어나가는데 큰 힘이 됩니다:)

감사합니다