7000만달러 시드 조달한 정형 검증 기업, AI 자동화에 나선다

&Truth는 정형 검증 자동화를 내세워 7000만달러(약 935억원)의 시드 자금을 조달했다고 밝혔다. 회사는 AI와 자체 기술을 결합해 소프트웨어가 요구조건을 충족하는지 증명하는 작업을 단축하겠다고 밝혔다.

&Truth는 29일(현지시간) 출범 발표문에서 비공개 운영을 마치고 사업을 공개한다고 밝혔다. 자금은 AI 안전과 벤처캐피털 분야 인사들로 구성된 그룹에서 조달했으며, 개별 투자자와 기업가치는 공개하지 않았다.

미국 국립표준기술연구소(NIST)는 정형 검증을 요구사항을 공식적으로 명세하고 구현을 수학적으로 모델링한 뒤, 논리 규칙으로 구현이 명세를 충족하는지 증명하는 절차로 설명한다.

일반적인 소프트웨어 테스트는 선택한 입력값으로 프로그램을 실행해 결과를 살펴본다. 정형 검증은 명세에 적힌 조건이 충족되는지를 증명한다.

이때 증명은 명세가 정한 범위 안에서만 유효하다. 코드가 요구조건을 만족한다는 결과만으로 그 요구조건이 실제 사용 환경과 의도를 모두 반영한다고 볼 수는 없다.

&Truth는 증명 작성 과정에 AI와 자체 자동화 기술을 적용하겠다고 밝혔다. 회사는 여러 프로그래밍 언어에 걸친 코드 검증을 목표로 제시했다.

회사는 AI가 증명 생성을 100배 이상 빠르게 하고, 자체 기술이 추가로 100배의 속도 향상을 낼 수 있다고 주장했다. 수개월 또는 수년이 걸리던 작업을 수시간이나 수분으로 줄일 수 있다는 설명이다.

이 속도 향상은 회사가 제시한 성능 목표다. 출범 발표문에는 해당 수치를 독립적으로 재현한 평가 결과가 담기지 않았다.

앤트로픽(Anthropic)은 10월 22일 Theorem과 함께 진행한 정형 검증 연구 결과를 공개했다. 이 연구는 &Truth의 제품이나 성능을 평가한 것이 아니라 별도로 진행된 작업이다.

연구진은 오픈소스 라이브러리 123개의 진입점 239개에 대해, 입력 크기가 64MB 이하일 때 프로그램이 충돌하지 않는다는 증명을 만들었다.

연구진은 증명 과정에서 발견한 결함을 수정한 뒤 결과를 검증했다. 검증 대상은 단일 스레드 정적 RISC-V 바이너리와 연구진이 모델링한 리눅스 환경 등 정해진 조건에 한정됐다.

앤트로픽은 이 결과가 라이브러리 전체에 버그가 없다는 뜻은 아니라고 설명했다. 증명 검증기는 제출된 증명이 명세와 일치하는지 확인하지만, 명세가 실제 요구사항과 환경을 온전히 반영하는지까지 판단하지는 못한다.

25일 Reddit RISC-V 게시판의 한 글에는 AI가 작성한 증명을 신뢰하기 어렵다는 의견과, 증명 검증기를 결과의 신뢰 기준으로 삼아야 한다는 답글이 함께 달렸다. 추천 23건을 받은 게시물 하나인 만큼 업계 전반의 반응으로 일반화하기는 어렵다.

정형 검증은 가상자산 분야에서도 별도로 활용된 사례가 있다. 지캐시 아이언우드의 잔액 무결성 검증에는 2700개가 넘는 정형 검증 정리가 포함됐다. 이 사례가 &Truth의 제품이나 고객과 연결된다는 의미는 아니다.

&Truth는 여러 프로그래밍 언어의 코드 검증을 목표로 내세웠지만, 출범 발표에서 스마트컨트랙트나 블록체인 코드에 특화된 제품·고객 사례를 제시하지 않았다.