Pramaana Labs, 형식 검증(Formal Verification)을 통한 AI 신뢰성 문제 해결을 위해 2,700만 달러 투자 유치

기업들이 AI를 실험적인 파일럿 프로그램에서 미션 크리티컬(mission-critical)한 비즈니스 운영으로 전환하는 데 어려움을 겪으면서, 업계는 '신뢰성'이라는 거대한 장벽에 직면해 있습니다. Pramaana Labs는 대규모 언어 모델(LLM)의 예측 불가능한 특성에 형식 검증(formal verification)의 수학적 엄밀함을 적용하여 이 간극을 메우고자 합니다.

확률론적 AI와 결정론적 AI 사이의 간극 해소

현대 AI의 근본적인 갈등은 확률론적 추론(probabilistic reasoning)과 결정론적 진실(deterministic truth) 사이의 차이에 있습니다. LLM은 자연어를 처리하고 복잡한 비정형 데이터를 다루는 데 탁월하지만, 환각(hallucination) 현상과 논리적 오류가 발생하기 쉽습니다. 단 한 번의 실수가 법적 또는 재정적 재앙으로 이어질 수 있는 산업 분야에서 이러한 오류는 용납될 수 없습니다.

Pramaana Labs는 하이브리드 아키텍처를 구축하여 이 문제를 해결하고 있습니다. 이들의 시스템은 자연어 상호작용에 필요한 유연성을 유지하기 위해 기존의 LLM 엔진을 활용하되, 그 위에 결정론적 검증 레이어(deterministic verification layer)를 덧씌웁니다. 이 레이어는 LLM이 생성한 출력이 엄격하게 코드화된 규칙을 준수하도록 보장하며, 오류를 방지하는 수학적 가드레일 역할을 효과적으로 수행합니다.

고위험 산업 분야 적용을 위한 LEAN 활용

일반적인 소프트웨어 테스트와 달리, Pramaana Labs는 형식 검증 도구를 활용하며 특히 오픈 소스 프로그래밍 언어인 LEAN에서 영감을 얻고 있습니다. LEAN은 전통적으로 복잡한 수학적 증명을 검증하는 데 사용되며, Pramaana는 이 기술을 응용하여 특정 전문 분야의 '규칙'을 코드화할 계획입니다.

이 회사는 정확성이 타협 불가능한 고감도(high-sensitivity) 수직 시장을 목표로 하고 있습니다:

이러한 시스템이 현실에 기반하도록 하기 위해, Pramaana는 엘리트 도메인 전문가들과 협력하고 있습니다. 여기에는 세무 관련 애플리케이션을 위한 전 국세청(IRS) 청장 대니 워펠(Danny Werfel)을 비롯하여, 사이버 보안 및 신약 개발 프로토콜을 감독하기 위한 IIT Delhi, IIT Madras, UC Berkeley의 교수진이 포함됩니다.

이것이 AI 생태계에 중요한 이유

Khosla Ventures가 주도하고 Accel, Boldcap, Nexus Venture Partners, Premji Invest, Unbound가 참여한 2,700만 달러 규모의 시드 라운드는 AI 투자 분야의 거대한 변화를 시사합니다. 생성형 AI의 '빠르게 움직이고 파괴하라(move fast and break things)' 시대가 기업 환경의 '검증 및 확인(verify and validate)' 요구사항과 마주하고 있습니다.

Pramaana Labs는 비정형화된 지식을 실행 가능하고 검증 가능한 코드(프랑스의 CATALA 프로젝트와 유사)로 변환함으로써, 규제 산업에서 AI가 어떻게 배포될 수 있는지에 대한 청사진을 제시하고 있습니다. 이 접근 방식이 성공한다면, AI가 인류의 건강, 법적 권리, 그리고 거대한 금융 시스템을 안전하게 관리할 수 있게 함으로써 수조 달러의 가치를 창출할 수 있습니다.

핵심 요약