혁신적 AI 시스템, 버그 없는 소프트웨어 검증에서 가능성 입증

전통적으로 소프트웨어 코드 검증 은 수동 코드 검토나 코드를 실행하여 이상을 찾는 등 노동 집약적인 과정이었습니다. 이러한 방법은 가치가 있지만 인간의 실수에 취약하며 복잡한 시스템에는 비현실적입니다.

Baldur 에 오신 것을 환영합니다. Baldur 는 대규모 언어 모델 (LLM) 의 힘을 활용하여 수학 증명을 자동으로 생성하는 정밀하게 설계된 솔루션입니다. 방대한 수학 콘텐츠와 증명에 사용되는 Isabelle/HOL 언어로 LLM 을 미세 조정함으로써, Baldur 는 한때 고된 작업이었던 것을 자동화하기 위한 거대한 도약을 이루었습니다. 그 결과? 코드 정확성을 검증하는 정리 증명기와 협력하여 오류율을 현저히 줄이는 시스템을 탄생시켰습니다.

Baldur 의 성공 핵심에는 증명을 자동으로 생성하는 도구인 Thor 와의 파트너십이 있습니다. Thor 는 57% 의 성공률을 자랑하지만, Baldur 와 결합하면 두 도구는 증명 생성에서 놀라운 65.7% 의 정확도를 달성합니다. 북유럽 신화에 영감을 받은 이 역동적인 듀오는 AI 기반 소프트웨어 검증의 잠재력을 보여줍니다.

LLM 의 과제

ChatGPT 와 같은 LLM 을 다룰 때 직면하는 주요 과제 중 하나는 때때로 정확성이 부족하다는 점입니다. 경고 신호를 보내는 대신 '침묵 속 실패'를 일으켜 유효해 보이는 오류 결과를 제공할 수 있습니다. AI 가 생성한 증명의 신뢰성을 보장하려면 이러한 문제를 해결하는 것이 필수적입니다.

발두르 개발은 결코 쉬운 일이 아니었으며, 수개월에 걸친 노력과 구글과의 긴밀한 협력이 필요했습니다. 프로젝트의 주저자인 에밀리 퍼스트는 Minerva를 활용했는데, 이는 방대한 자연어 텍스트 코퍼스로 훈련된 대형 언어 모델(LLM)입니다. 이후 Minerva는 수학 및 과학 논문과 수학 표현이 포함된 웹 콘텐츠를 포함한 118GB 규모의 상당한 데이터셋으로 파인튜닝되었습니다. 그러나 가장 중요한 차별점은 Isabelle/HOL 언어를 추가로 파인튜닝하여 포괄적인 수학 증명 생성의 기반을 마련했다는 점입니다.

Baldur 의 오류 수정 접근 방식은 독창적입니다. 정리 증명기가 생성된 증명 내 오류를 식별하면, 해당 정보를 Baldur 로 피드백하여 시스템이 실수로부터 학습할 수 있도록 합니다. 이러한 반복적 프로세스는 증명의 정확성과 신뢰성을 높여 코드를 검증하는 매우 효과적인 도구가 됩니다.

버그 없는 소프트웨어를 위한 유망한 미래

개선이 필요한 부분도 있지만, 발더는 형식적 소프트웨어 검증의 유망한 길을 제시합니다. 엔지니어가 여전히 소프트웨어를 개발해야 하지만, 이제 그들은 수학적 증명을 자동으로 생성할 수 있는 강력한 파트너인 발더를 보유하고 있습니다.

UMass Amherst의 Manning College of Information and Computer Sciences 교수인 Yuriy Brun은 "우리의 작업은 이러한 증명들을 작성하는 것을 자동화하려는 데 중점을 둡니다. Baldur은 대규모 언어 모델을 사용하여 수학적 정리를 제공하면 정리 증명기가 검증할 수 있는 해당 정리의 증명을 자동으로 생성합니다."라고 언급했습니다.

Baldur의 성공은 이 프로젝트에 헌신적으로 노력한 팀에게 기인합니다. Emily First, 당시 Google에서 근무하던 Markus Rabe, 그리고 일리노이 대학교 어바나 샴페인分校의 조교수인 Talia Ringer가 크게 기여했습니다. Defense Advanced Research Projects Agency(DARPA)와 National Science Foundation(NSF)가 프로젝트를 지원했습니다.

Baldur와 같은 혁신적인 솔루션은 기술 산업이 소프트웨어 시스템의 끊임없이 증가하는 복잡성과 씨름함에 따라 희망을 제공합니다. AI의 능력이 계속 진화하고 성숙해짐에 따라, Baldur가 소프트웨어 정확성을 새로운 수준으로 끌어올릴 잠재력은 유망합니다.