기업들이 인공지능(AI) 파일럿 프로그램을 실제 비즈니스에 적용하는 데 어려움을 겪는 주요 원인 중 하나는 바로 AI의 신뢰성(reliability) 문제입니다. 이러한 문제를 해결하기 위해 수학적 형식화(mathematical formalization) 도구를 활용, 컴퓨터 과학의 가장 신뢰할 수 있는 시스템과 가장 예측 불가능한 시스템을 결합하려는 새로운 스타트업 프라마나 랩스(Pramaana Labs)가 코슬라 벤처스(Khosla Ventures) 주도로 2,700만 달러(약 370억 원)의 시드 투자를 유치했습니다.
프라마나는 법률, 신약 개발, 세금 준비와 같이 오류가 발생하면 치명적인 결과를 초래할 수 있는 고감도 분야에 집중할 예정입니다. 이들 시스템에 AI를 배포하려면 현재보다 훨씬 강력한 환각(hallucination) 및 오류 방지 기능이 필수적입니다. 프라마나의 공동 창립자이자 CEO인 란잔 라자고팔란(Ranjan Rajagopalan)은 세법과 같이 지켜야 할 많은 규칙이 있는 분야는 형식화에 특히 적합하다고 설명합니다. 일단 규칙이 명확하게 코드화되면, 그 위에 구축되는 추론(reasoning)은 결정론적(deterministic)이 될 수 있다는 것입니다. 프라마나의 시스템은 기존 대규모 언어모델(LLM)을 기반으로 자연어 질문에 답하고 복잡한 문제를 해결하는 유연성을 유지하면서도, 그 위에 LLM의 작업을 검증하는 결정론적 계층을 추가합니다. 특히 수학적 증명 검증에 사용되는 오픈소스 프로그래밍 언어인 LEAN을 활용한 형식 검증 도구를 사용하는 것이 프라마나의 독특한 접근 방식입니다.
이러한 접근 방식은 프랑스의 CATALA 프로젝트와 같은 선례가 있습니다. CATALA 프로젝트는 프랑스의 세금 및 복지 시스템의 상당 부분을 실행 가능한 코드로 형식화했습니다. 프라마나는 각 사용 사례에 맞춰 도메인 전문가의 감독하에 자체적인 LEAN 스타일의 형식 검증 시스템을 구축할 계획입니다. 예를 들어, 세법 분야에서는 전 국세청(IRS) 국장인 대니 워펠(Danny Werfel)과 협력하고 있으며, 사이버 보안 및 신약 개발 시스템에는 IIT 델리, IIT 마드라스, UC 버클리 교수들이 참여하고 있습니다. 라자고팔란은 “세상에서 가장 어려운 문제들은 해결 불가능한 것이 아니라, 형식화되지 않은 것”이라며, “건강, 돈, 자유를 잃을 수 있는 모든 분야에는 규칙이 있으며, 이제 그 규칙들을 코드화해야 한다”고 강조했습니다. 이는 AI의 신뢰성을 확보하고, 그 활용 범위를 더욱 넓히는 데 중요한 전환점이 될 수 있습니다.