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

본문

&Truth는 AI와 자체 자동화 기술로 증명 생성 시간을 줄이겠다고 밝혔다. &Truth는 정형 검증 자동화를 내세워 7000만달러(약 935억원)의 시드 자금을 조달했다고 밝혔다. &Truth는 29일(현지시간) 출범 발표문에서 비공개 운영을 마치고 사업을 공개한다고 밝혔다. 자금은 AI 안전과 벤처캐피털 분야 인사들로 구성된 그룹에서 조달했으며, 개별 투자자와 기업가치는 공개하지 않았다. 미국 국립표준기술연구소(NIST)는 정형 검증을 요구사항을 공식적으로 명세하고 구현을 수학적으로 모델링한 뒤, 논리 규칙으로 구현이 명세를 충족하는지 증명하는 절차로 설명한다. 앤트로픽(Anthropic)은 10월 22일 Theorem과 함께 진행한 정형 검증 연구 결과를 공개했다. 연구진은 오픈소스 라이브러리 123개의 진입점 239개에 대해, 입력 크기가 64MB 이하일 때 프로그램이 충돌하지 않는다는 증명을 만들었다.

검증 대상은 단일 스레드 정적 RISC-V 바이너리와 연구진이 모델링한 리눅스 환경 등 정해진 조건에 한정됐다. 25일 Reddit RISC-V 게시판의 한 글에는 AI가 작성한 증명을 신뢰하기 어렵다는 의견과, 증명 검증기를 결과의 신뢰 기준으로 삼아야 한다는 답글이 함께 달렸다. 지캐시 아이언우드의 잔액 무결성 검증에는 2700개가 넘는 정형 검증 정리가 포함됐다. &Truth는 여러 프로그래밍 언어의 코드 검증을 목표로 내세웠지만, 출범 발표에서 스마트컨트랙트나 블록체인 코드에 특화된 제품·고객 사례를 제시하지 않았다. 본 기사는 시장 데이터 및 차트 분석을 바탕으로 작성되었으며, 특정 종목에 대한 투자 권유가 아닙니다.