메뉴
BL
TechCrunch AI 41일 전

프라마나 랩스, 270억 시드 투자 유치

IMP
8/10
핵심 요약

AI 스타트업 프라마나 랩스(Pramaana Labs)가 대형 언어 모델(LLM)의 오류와 환각을 잡기 위해 수학적 '형식 검증(Formal verification)'을 도입합니다. 이를 통해 법률, 세무, 신약 개발 등 오류가 치명적인 분야에서 기업들이 안전하게 AI를 활용할 수 있도록 돕고자 합니다.

번역된 본문

기업들이 AI 시범 프로젝트를 실제 비즈니스의 기능적 부분으로 전환하는 데 어려움을 겪으면서 신뢰성이 가장 중요한 화두로 떠올랐습니다. 새로운 스타트업이 컴퓨터 과학에서 가장 신뢰할 수 있는 시스템 중 하나를 가장 혼란스러운 시스템 중 하나와 결합하여 수학적 형식화 도구를 활용해 이 문제를 해결하려고 합니다.

수요일, 프라마나 랩스(Pramaana Labs)는 코슬라 벤처스(Khosla Ventures)의 주도로 엑셀(Accel), 볼드캡(Boldcap), 넥서스 벤처 파트너스(Nexus Venture Partners), 프렘지 인베스트(Premji Invest), 언바운드(Unbound) 등이 참여한 2,700만 달러(약 270억 원)의 시드 투자 유치를 발표했습니다.

프라마나는 오류 비용이 매우 높고 신뢰성이 필수적인 법률, 신약 개발, 세무 준비와 같은 고도로 민감한 수직 산업 분야에 집중할 예정입니다. 이러한 시스템에 AI를 배포하려면 현재 우리가 가진 것보다 환각과 오류에 대한 더 강력한 보호 장치가 필요할 것입니다.

하지만 프라마나의 공동 창립자이자 CEO인 란잔 라자고팔란(Ranjan Rajagopalan)은 이러한 분야가 형식화에 독특하게 적합하다고 봅니다. 라자고팔란은 세법의 규칙을 설명하며 테크크런치(TechCrunch)에 다음과 같이 말했습니다. "이는 준수해야 할 많은 규칙이 있다는 점에서 수학과 같습니다. 규칙이 일단 코드화되면, 그 위에서 이루어지는 추론은 결정론적으로 변하기 시작합니다."

프라마나의 시스템은 여전히 기존의 대형 언어 모델(LLM)을 기반으로 실행되어 자연어 질문에 답하고 기존 컴퓨터가 처리할 수 없는 복잡한 문제를 해결하는 유연성을 갖추고 있습니다. 하지만 그 LLM 위에 언어 모델의 작업 결과를 교차 검증하는 결정론적(Deterministic) 계층이 추가로 존재합니다.

이러한 LLM 엔진과 결정론적 검증의 결합은 인기 있는 구성입니다. 프라마나만의 독특한 접근 방식은 수학적 증명을 검증하는 데 사용되는 오픈소스 LEAN 프로그래밍 언어를 활용하는 등 '형식 검증(Formal verification)' 도구를 사용한다는 것입니다. 이러한 작업에는 실제 선례가 있습니다. 라자고팔란은 프랑스의 세금 및 복지 시스템의 상당 부분을 실행 가능한 코드로 형식화한 프랑스의 카탈라(CATALA) 프로젝트를 예로 들었습니다.

각 사용 사례에 대해 프라마나는 분야 전문가들이 감독하는 자체적인 LEAN 스타일의 형식 검증 시스템을 구축할 것입니다. 세법의 경우 전 미국 국세청(IRS) 청장인 대니 베르펠(Danny Werfel)과 협력하고 있으며, 인도 공과대학(IIT) 델리 및 마드라스 캠퍼스와 UC 버클리의 교수들이 사이버 보안 및 신약 개발 시스템을 감독할 예정입니다.

라자고팔란은 "세상에서 가장 어려운 문제는 해결 불가능한 것이 아니라 형식화되지 않은 것"이라며, "잘못될 경우 누군가의 건강, 돈, 또는 자유를 잃게 만들 수 있는 모든 영역에는 규칙이 있다"고 말했습니다. 이제 이러한 규칙들을 코드화하기만 하면 됩니다.

원문 보기
원문 보기 (영어)
As enterprises struggle to turn AI pilot programs into functional parts of their business, reliability has taken center stage. A new startup is hoping to solve that problem by drawing on the tools of mathematical formalization, combining one of computer science’s most reliable systems with one of its most chaotic. On Wednesday, Pramaana Labs announced $27 million in seed funding led by Khosla Ventures, with participation from Accel, Boldcap, Nexus Venture Partners, Premji Invest, and Unbound. Pramaana will focus on highly sensitive verticals like law, drug discovery, and tax preparation — where errors can be costly and reliability is at a premium. Deploying AI in those systems will require stronger protections against hallucinations and errors than we currently have. But as Pramaana co-founder and CEO Ranjan Rajagopalan sees it, they’re also uniquely suited to formalization. “It's like math in the sense that you have a lot of rules that you need to abide by,” Rajagopalan told TechCrunch, describing the rules of the tax code. “Once you have a codified version of it, the reasoning on top of it starts becoming deterministic.” Pramaana’s system still runs on a conventional LLM, giving it the flexibility to answer natural language questions and tackle complex problems that conventional computers can’t handle. But there’s a deterministic layer on top of that LLM ensuring the LLM’s work checks out. This combination of an LLM engine with deterministic verification is a popular setup ; Pramaana’s unique approach is to use the tools of formal verification — drawing on the open-source LEAN programming language used to verify mathematical proofs. There's real precedent for much of this work; Rajagopalan points to France's CATALA project , which formalizes much of the country's tax and benefit system into executable code. For each use case, Pramaana will build its own LEAN-style formal verification system, overseen by domain experts. For tax law, the company is working with former IRS commissioner Danny Werfel, while professors from IIT Delhi, IIT Madras, and UC Berkeley oversee the cybersecurity and drug discovery system. "The world's hardest problems are not unsolvable. They are unformalized,” says Rajagopalan. “Every domain where being wrong can cost someone their health, money, or freedom has rules.” Now, those rules just need to be codified. Topics AI , formal verification , reliability When you purchase through links in our articles, we may earn a small commission . This doesn’t affect our editorial independence. Russell Brandom AI Editor Russell Brandom has been covering the tech industry since 2012, with a focus on platform policy and emerging technologies. He previously worked at The Verge and Rest of World, and has written for Wired, The Awl and MIT's Technology Review. He can be reached at russell.brandom@techcrunch.com or on Signal at 412-401-5489. View Bio June 18 Los Angeles Get an inside look at what it takes to scale and succeed from leaders at Mach Industries, Founders Fund, and Shinkei Systems. Through candid fireside chats and high-impact networking, you'll walk away with valuable insights and new connections. REGISTER NOW Most Popular SpaceX to acquire Cursor for $60B in stock, days after blockbuster IPO Sean O'Kane The US government's Anthropic models ban was never about an AI jailbreak Zack Whittaker The AI layoff wave is becoming a powder keg Connie Loizos Amazon CEO reportedly raised Anthropic model concerns before government crackdown Anthony Ha The FBI built its own replica small town to simulate real-world cyberattacks Zack Whittaker Meta's months-old AI unit is a soul-crushing gulag, say the engineers stuck inside it Connie Loizos Jeff Bezos's Prometheus raises $12B to build an ‘artificial general engineer' for the physical world Marina Temkin