Pramaana Labs が Khosla Ventures からシードラウンドで 2700 万ドルを調達し、AI の形式検証を実現へ
Pramaana Labs は Khosla Ventures などから 2700 万ドルのシードラウンドを調達し、AI システムの信頼性を担保する形式検証技術の実用化を加速させる。
キーポイント
大規模資金調達の成功
Pramaana Labs は Khosla Ventures を含む投資家から 2700 万ドルのシードラウンドに成功し、事業拡大の基盤を確立した。
形式検証技術の実用化
AI システムの論理的整合性を数学的に証明する「形式検証」技術を、実環境で即座に適用可能なレベルまで引き上げることを目指す。
信頼性向上への注力
生成 AI のハルシネーションや誤動作を防止し、医療・金融など高リスク領域での AI 導入を可能にする信頼性の確保が主目的である。
影響分析・編集コメントを表示
影響分析
本ニュースは、生成 AI の普及における最大の課題である「信頼性の欠如」に対する解決策として、形式検証という厳密な数学的アプローチが実社会で採用され始めていることを示唆しています。Khosla Ventures からの投資は、単なる研究段階ではなく、産業応用に向けた本格参入を意味しており、今後は AI システムの監査や認証において形式検証ツールが標準的なコンポーネントとなる可能性が高まります。
編集コメント
AI の安全性確保において、確率論的なテストから数学的証明へのシフトは重要な転換点です。Khosla Ventures の参画は、この技術が将来的にインフラとして不可欠になることを示す強力なシグナルと言えます。
企業が AI のパイロットプログラムを実際の業務に組み込むことに苦戦する中、信頼性が中心課題となっています。ある新興企業は、数学的形式化のツールを活用し、コンピュータサイエンスで最も信頼性の高いシステムの 1 つと、最も混沌としたシステムの 1 つを組み合わせることで、この問題の解決を目指しています。
水曜日、Pramaana Labs は Khosla Ventures が主導し、Accel、BoldCap、Nexus Venture Partners、Premji Invest、Unbound が参加する形で、シードラウンドとして 2700 万ドルの資金調達を発表しました。
Pramaana は、エラーが重大な結果を招く可能性があり、信頼性が極めて重要となる法務、創薬、税務申告といった高感度な分野に注力します。これらのシステムで AI を導入するには、現状よりも幻覚現象やエラーに対する強力な保護策が必要です。しかし、Pramaana の共同設立者兼 CEO である Ranjan Rajagopalan 氏は、同社が形式化に適したユニークな立場にあると見ています。
「税務コードのルールのように、遵守すべき多くの規則が存在する点で数学と同じです」と Rajagopalan 氏は TechCrunch に語り、税務コードをコード化されたバージョンとして捉えることで、「その上で推論を行うことが決定論的になり始めます」と説明しました。
Pramaana のシステムは依然として従来の大規模言語モデル（LLM: Large Language Model）上で動作しており、自然言語での質問に柔軟に対応し、従来のコンピュータでは処理できない複雑な問題に取り組む能力を備えています。しかし、その LLM の作業が正しいことを保証する決定論的なレイヤーがその上に存在します。
LLM エンジンと決定論的検証を組み合わせたこの構成は 人気のあるセットアップですが、Pramaana の独自のアプローチは、数学的証明の検証に用いられるオープンソースの LEAN プログラミング言語を活用した形式検証（formal verification）ツールを使用することです。この作業の多くには実例が存在します。Rajagopalan 氏は、フランスの CATALA プロジェクト を挙げています。これは同国の税制や給付制度の多くを実行可能なコードとして形式化するプロジェクトです。
各ユースケースにおいて、Pramaana はドメイン専門家の監督のもと、独自の LEAN スタイルの形式検証システムを構築します。税法については元 IRS 長官の Danny Werfel と協力しており、サイバーセキュリティや創薬システムの監督には、インド工科大学（IIT）デリー校、IIT マドラス校、およびカリフォルニア大学バークレー校の教授たちがあたっています。
「世界で最も困難な問題が解決不可能なのではありません。それらは形式化されていないのです」と Rajagopalan は述べています。「誰かの健康、金銭、自由を損なう可能性があるすべての分野にはルールが存在します」
今や必要なのは、そのルールをコードとして記述することだけです。
*当記事内のリンクを通じて購入された場合、私たちは少額のコミッションを受け取る可能性があります。これは当社の編集の独立性には影響しません。*
ラッセル・ブランドムは2012年以来、プラットフォーム政策と新興技術に焦点を当てながらテクノロジー業界の報道を行ってきました。以前はThe VergeやRest of Worldで勤務し、Wired、The Awl、MIT's Technology Reviewにも寄稿しています。
彼への連絡先は russell.brandom@techcrunch.com または Signal（412-401-5489）です。
原文を表示
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.
*When you purchase through links in our articles, we may earn a small commission. This doesn’t affect our editorial independence.*
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.
関連記事
Google DeepMind が ASI（人工超知能）への道を探る
Google DeepMind が、人間を超える能力を持つ人工超知能（ASI）の実現に向けた研究経路について詳細な分析を行っている。
リリース前にデプロイをシミュレーションしてモデルの挙動を予測する手法
OpenAI は、モデルを実際に公開する前にデプロイ環境をシミュレーションすることで、その挙動を事前に予測・評価する新しい手法を発表した。
今日の最先端 AI 企業は、もはや AI の能力フロンティアを超えることはない（18 分読）
TLDR AI は、現在の最先端 AI 企業が将来的に AI の能力フロンティアをさらに上回ることはないと主張している。
今日のまとめ
AI日報で今日の重要ニュースをまとめ読み