프라마나랩스, 규제 산업 겨냥 ‘검증형 AI’로 시드 2,700만달러 유치

고위험 인공지능을 위한 ‘컴파일러’를 내세운 프라마나랩스가 시드 투자 2,700만달러를 유치했다. 원화 기준으로는 약 412억원 규모다. 생성형 AI의 가장 큰 약점으로 꼽히는 ‘그럴듯하지만 틀린 답변’을 줄이기 위해, 답변을 내놓기 전에 수학적으로 검증하는 구조를 앞세웠다는 점이 눈에 띈다.

프라마나랩스는 17일(현지시간) 세금, 의료 진단, 사이버보안, 금융 컴플라이언스 등 실수가 큰 비용으로 이어지는 분야를 겨냥한 검증 시스템을 개발 중이라고 밝혔다. 이번 투자 라운드는 코슬라벤처스가 주도했고, 액셀, 볼드캡, 넥서스벤처파트너스, 프렘지인베스트, 언바운드캐피털이 참여했다.

결정론적 검증 계층

이 회사의 핵심은 대형언어모델(LLM) 위에 ‘결정론적 검증 계층’을 올리는 방식이다. 일반적인 AI 모델이 자연어 질문에 대한 초안을 만들면, 프라마나랩스의 시스템이 해당 답변을 특정 산업의 규칙 체계와 대조해 검증한다. 답이 규칙에 맞는 것으로 ‘증명’되지 않으면 결과를 반환하지 않는 구조다.

회사는 세법과 임상 프로토콜처럼 규칙이 엄격한 영역의 기준을 기계가 추론할 수 있는 형식 언어로 다시 작성한다고 설명했다. 이후 사용자의 질문을 형식화된 주장으로 바꾸고, 이를 증명 엔진에 넘겨 기계가 확인 가능한 증명을 생성한다. 만약 답변이 성립하지 않으면 어떤 규칙에서 문제가 발생했는지 짚어준다. 프라마나랩스는 현재까지 ‘확신에 찬 오답’을 검증 완료 답변으로 내놓은 적은 없다고 밝혔다.

기술 기반으로는 오픈소스 형식 검증 언어 ‘린(Lean)’이 사용된다. 이는 수학 정리를 기계적으로 검증하는 데 쓰이는 언어로, 프라마나랩스는 이 접근이 실제 AI 시스템에도 적용 가능하다고 보고 있다. 회사는 구글 딥마인드의 ‘알파프루프(AlphaProof)’와 프랑스의 ‘카탈라(Catala)’ 프로젝트를 사례로 들며, 수학적 증명과 규제 규칙의 형식화를 자동화할 수 있는 가능성이 커지고 있다고 강조했다.

란잔 라자고팔란 최고경영자(CEO)는 테크크런치와의 인터뷰에서 세법을 두고 “따라야 할 규칙이 매우 많은 점에서 수학과 비슷하다”며 “이를 일단 코드화하면 그 위에서 이뤄지는 추론은 결정론적으로 바뀌기 시작한다”고 말했다. 결국 AI가 단순히 ‘말이 되는 답’을 만드는 수준을 넘어, 왜 그 답이 맞는지까지 입증해야 하는 산업이 늘고 있다는 뜻이다.

창업 배경과 인력 구성

프라마나랩스는 인도공과대학 마드라스 동문 3명이 창업했다. 라자고팔란은 과거 구글맵스의 콘텐츠 중재 부문을 이끌었고, 공동창업자 크리슈난은 글린테크놀로지스의 글린 어시스턴트 개발에 참여했다. 또 다른 공동창업자 산제이는 구글 딥마인드의 연구 엔지니어로 근무하며 제미나이 모델 개발에도 관여했다. 현재 팀에는 구글 딥마인드, 메타플랫폼스($META), 마이크로소프트($MSFT), 우버테크놀로지스($UBER), UC버클리 출신 연구진이 포함돼 있다.

각 산업별로 별도의 검증 시스템을 구축한다는 점도 특징이다. 세금 분야는 전 미국 국세청 청장 대니 워펠이 자문하고 있으며, 사이버보안과 신약 개발 분야는 인도공과대학 델리, 인도공과대학 마드라스, UC버클리 교수진이 감독한다. 구글 딥마인드의 푸시밋 콜리와 마이크로소프트 리서치의 스리람 라자마니도 지원 인사로 이름을 올렸다.

투자금 활용과 의미

이번 자금은 규칙 형식화 모델과 증명 모델 학습, 연구 엔지니어 채용, 그리고 규제 산업별 전문 인력 확충에 투입될 예정이다. 생성형 AI가 기업 현장으로 빠르게 들어오고 있지만, 의료·세무·금융처럼 오류 허용 범위가 극히 낮은 분야에서는 ‘정확성의 증명’이 새로운 경쟁력이 될 수 있다는 평가가 나온다. 프라마나랩스의 시도는 AI 산업이 단순한 응답 생성에서 ‘검증 가능한 자동화’로 이동하는 흐름을 보여주는 사례로 읽힌다.