수학으로 AI 코딩 버그 잡는다

소프트웨어 결함을 수학적으로 증명하는 형식 검증 분야에 AI 스타트업들이 잇달아 뛰어들고 있다. 형식 검증은 수십 년간 NASA·Apple 등 일부 핵심 조직에서만 활용됐다. 소프트웨어 목표를 정밀하게 서술하고 코드를 수학 공식으로 변환해야 하는 번거로움 때문에 비용과 시간이 막대하게 들었다.

&Truth의 CSO Ilya Sergey는 "다리와 건물이 무너지지 않는 이유는 건설 전 수학 계산을 했기 때문"이라며 "코드에도 같은 원리를 적용할 수 있는 기술은 이미 있었지만, 규모 확장이 어려웠을 뿐"이라고 설명했다. Sun의 연구팀은 AI 도구를 활용해 메시징 앱 Signal의 암호화 코드 일부를 검증했으며, 숙련 전문가 3명이 5개월 걸린 작업을 500달러 이하 비용으로 반나절 만에 완료했다.

경쟁사 Harmonic은 Robinhood CEO Vlad Tenev가 공동 창업했으며 2억 9,500만 달러를 확보했다. 이번 주 수학 특화 AI 에이전트 Aristotle이 C 언어 및 하드웨어 설계 언어 Verilog 검증을 지원한다고 발표했고, Nvidia 등 칩 제조사와 협력을 검토 중이다. Anthropic과 스타트업 Theorem도 지난주 AI를 활용해 수조 번의 테스트도 잡지 못한 오픈소스 버그를 발견했다고 공동 발표하며 Claude용 검증 플러그인도 공개했다.

다만 기술은 아직 프로토타입 단계다. 고객 지불 의사, 도입 방식, 사용자 실수나 하드웨어 오류에서 비롯된 버그 탐지 한계 등은 여전히 미해결 과제로 남아 있다.