形式検証でAI誤答防ぐ新興企業、27億円調達
詳細を読む
AIスタートアップのPramaana Labsは6月17日、Khosla Venturesが主導するシードラウンドで2700万ドルを調達したと発表しました。Accel、BoldCap、Nexus Venture Partners、Premji Invest、Unboundも参加しています。同社は数学的形式化の手法を使い、AIの信頼性という課題の解決を目指します。
企業が実証実験を本格運用に移す際、AIの信頼性が最大の壁になっています。同社は法務、創薬、税務など誤りが高くつく分野に絞って展開する方針です。共同創業者でCEOのRanjan Rajagopalan氏は、これらの領域はルールが多く、形式化に向いていると説明します。
仕組みの中核は、通常のLLMの上に決定論的な検証層を重ねる構成です。LLMが自然言語の質問に柔軟に答え、その出力が正しいかを検証層が確認します。LLMと検証を組み合わせる手法自体は広がりつつありますが、同社の独自性は数学の証明検証に使うオープンソース言語LEANを応用する点にあります。
用途ごとに専門家が監修する形式検証システムを構築する計画です。税法では元IRS長官のDanny Werfel氏が、サイバーセキュリティと創薬ではIITデリー、IITマドラス、カリフォルニア大学バークレー校の教授が監修します。フランスが税・給付制度を実行可能なコードに落とし込んだCATALAプロジェクトという先行例も参考にしています。
Rajagopalan氏は「世界で最も難しい問題は解けないのではなく、形式化されていないだけだ」と語ります。健康や金銭、自由を左右する領域には必ずルールがあり、あとはそれをコード化すればよいという考えです。経営者にとっては、規制の厳しい業務へAIを導入する際の現実的な選択肢になり得ます。