[박찬 기자]

<이미지를 클릭하시면 크게 보실 수 있습니다>

AI가 작성한 코드를 AI로 검증하는 새로운 기술이 실리콘 밸리에서 주목받고 있다. 이번에는 수학 AI로 유명한 액시엄 매스(Axiom Math)가 이 분야에 도전장을 내밀었다.

뉴욕 타임스는 12일(현지시간) AI 코딩의 품질 저하와 버그 증가 문제가 제기되면서 이를 해결하기 위한 스타트업들이 잇달아 등장하고 있다고 보도했다.

그 예로 지난 1월 카네기멜론대학교가 AI 코드 생성 기술 분석 연구를 소개했다. AI는 소프트웨어 개발 속도를 크게 높일 수 있지만, 코드 품질을 저하해 프로젝트 속도를 늦출 수 있다는 결과다.

이러한 문제는 코드 생성 도구가 확산하면서 중요한 문제로 떠오르고 있다. 이를 해결하기 위해 실리콘 밸리에서는 코드를 자동으로 검증하는 AI 시스템 개발이 새로운 경쟁 분야로 떠오르고 있다.

대표적인 기업이 액시엄과 하모닉, 로지컬 인텔리전스 등이다.

그중 액시엄은 최근 멘로 벤처스, 그레이크로프트, 마드로나 벤처 그룹 등으로부터 2억달러(약 3000억원) 투자를 유치하며 기업가치 16억달러(약 2조4000억원)를 기록했다.

직원 20여명 규모의 설립 1년 차 스타트업이지만, 투자자들은 AI 코드 품질 문제를 해결할 핵심 기술로 보고 대규모 자금을 투입하고 있다는 것이다.

액시엄은 그동안 수학적 증명(formal proof) 시스템을 통해 에르되시 문제 등 수학 난제를 해결하는 데 집중했다. 이를 적용한 기술 액시엄프루버(AxiomProver)는 수학 문제의 정답을 형식적 증명 방식으로 검증할 수 있다.

이 시스템은 수학 증명을 위해 개발된 프로그래밍 언어 린(Lean)을 활용한다. 이는 수학자들이 정리와 증명을 컴퓨터로 검증하기 위해 만든 도구였지만, 이제는 AI가 이를 활용해 문제의 정답 여부를 논리적으로 증명하는 데 사용되고 있다.

이제는 수학 문제 증명 능력을 소프트웨어 코드 검증으로 확장했다. 이러한 접근을 전이 학습(transfer learning)이라고 부른다. 즉 AI가 먼저 수학적 증명 능력을 학습한 뒤, 그 과정에서 얻은 논리적 검증 능력을 소프트웨어 코드의 품질과 정확성을 확인하는 데 적용하는 방식이다.

이를 통해 AI 코드 검증 성능을 평가하는 벤치마크 테스트에서도 높은 점수를 기록했다고 밝혔다.

카리나 홍 액시엄 CEO는 "코드 검증은 AI 개발의 다음 프론티어 분야"라고 강조했다. 그는 스탠포드대학교에서 박사 과정을 포기하고 24세의 나이에 스타트업을 설립한 것으로 유명하다.

전문가들은 코드 검증 AI의 한계도 지적한다. 수학에서는 정답과 오답이 명확하게 구분되지만, 소프트웨어 개발에서는 그렇지 않기 때문이다. 특히 수억명의 사용자가 동시에 사용하는 서비스에서는 '정확한 코드'라는 정의 자체가 복잡해질 수 있다.

보그단 바실레스쿠 카네기멜론대 컴퓨터공학 교수는 "AI가 검증할 수 있는 영역은 분명히 있다. 하지만 코드의 모든 문제를 완전히 해결할 수 있다는 의미는 아니다"라고 설명했다.

그러나 업계에서는 AI가 코드를 작성하고 또 AI가 이를 검증하는 구조가 앞으로 소프트웨어 개발의 핵심 모델이 될 가능성이 크다고 보고 있다.

AI 코드 생성 기술이 빠르게 보편화하면서, 이제 업계의 다음 과제는 "AI가 만든 코드를 얼마나 신뢰할 수 있느냐"라는 문제로 이동하고 있기 때문이다.

박찬 기자 cpark@aitimes.com

<저작권자 Copyright ⓒ AI타임스 무단전재 및 재배포 금지>