이러한 현실에 직면하여 실리콘 밸리의 일부 스타트업은 AI가 생성한 코드의 정확성을 검증하기 위해 기술을 개발하는 방법을 찾고 있습니다.
ChatGPT와 같은 AI 챗봇이나 현재 프로그래밍 지원 시스템은 몇 초 만에 컴퓨터 코드를 생성할 수 있습니다. 그럼에도 불구하고 전문가들은 이러한 시스템이 때때로 오류가 발생하거나 심지어 부정확한 정보를 생성한다고 말합니다.
카네기 멜론 대학교(미국)의 연구원들이 1월에 발표한 연구에 따르면 AI 코드 생성 도구는 소프트웨어 개발 프로세스를 가속화하는 데 도움이 될 수 있습니다. 그러나 코드 품질을 저하시켜 장기적으로 프로젝트에 문제를 일으킬 수도 있습니다.
이러한 과제에 직면하여 실리콘 밸리의 많은 스타트업 기업들이 컴퓨터 코드를 검증하기 위한 기술을 개발하고 있습니다.
Axiom Math 및 Harmonic(캘리포니아 팔로알토) 또는 Logical Intelligence(샌프란시스코)와 같은 인공 지능 분야의 기술 스타트업은 수학자들이 문제를 증명하는 것과 유사한 방식으로 코드를 검증할 수 있는 AI 시스템을 구축하고 있습니다.
Axiom Math의 설립자이자 CEO인 Carina Hong은 코드 인증이 AI 기술 개발 과정에서 다음 단계가 될 수 있다고 말했습니다.
최근 이 회사는 Menlo Ventures, Greycroft 및 Madrona를 포함한 벤처 캐피탈 펀드로부터 2억 달러를 성공적으로 모금했다고 발표했습니다.
설립된 지 약 1년이고 직원이 약 20명에 불과하지만 Axiom Math는 16억 달러의 가치를 평가받았습니다. 투자자들은 회사의 기술이 Codex 또는 Claude Code와 같은 AI 시스템에서 생성된 코드 품질을 개선하는 데 도움이 될 수 있다고 믿습니다.
Matt Kraning(기술 분야의 벤처 투자자이자 Menlo Ventures의 파트너)에 따르면 현재 AI를 사용하여 코드를 작성할 때 가장 큰 문제는 사용자가 코드에 오류가 있는지 확인할 수 없다는 것입니다.
Matt Kraning은 Axiom과 같은 코드 검증 기술이 이 문제를 어느 정도 해결하는 데 도움이 될 수 있다고 말했습니다.
원래 Axiom은 복잡한 수학 문제를 해결하기 위한 기술을 개발했습니다. 회사 시스템인 AxiomProver는 Putnam 수학 시험(미국과 캐나다에서 가장 우수한 대학생 대회 중 하나)에서 만점을 받았습니다.
이 기술은 수학적 명제를 증명하기 위해 10년 이상 전에 개발된 Lean 프로그래밍 언어를 사용하여 작동합니다.
수학에서 옳고 그름을 명확하게 식별하는 능력 덕분에 시스템은 문제 해결 과정에서 논리적 오류를 제거할 수 있습니다.
연구자들은 컴퓨터 코드를 검증하기 위해 동일한 방법을 적용할 수 있기를 희망합니다. 이것은 AI 시스템이 한 분야에서 기술을 배우고 다른 작업에 성공적으로 적용할 때의 "교환 학습"의 예입니다.
그럼에도 불구하고 일부 전문가들은 이 방법에 여전히 한계가 있다고 경고합니다. 카네기 멜론 대학교 컴퓨터 과학 교수인 보그단 바실레스쿠에 따르면 "정확한" 컴퓨터 코드가 무엇인지 항상 명확하게 정의할 수 있는 것은 아닙니다.
실제로 많은 소프트웨어, 특히 수백만 명의 사용자에게 서비스를 제공하는 온라인 서비스는 복잡하고 예측하기 어려운 운영 환경을 갖게 될 것입니다.
따라서 AI가 일부 오류를 검사하는 데 도움이 될 수 있지만 이 기술은 컴퓨터 코드의 모든 문제를 완전히 제거하기는 어렵습니다.
