企業がAIのパイロットプログラムを実際の業務に組み込むのを支援する"Pramaana Labs"がSeedで$27Mを調達

Pramaana Labsは、Khosla Venturesがリードし、Accel、BoldCap、Nexus Venture Partners、Premji Invest、Unboundが参加したSeedで$27Mを調達しました。

企業がAIのパイロットプログラムを実際の業務に組み込むのを支援するPramaana Labsは、数学的形式化の手法を活用し、コンピューターサイエンスにおいて最も信頼性の高いシステムの一つと、最も混沌としたシステムの一つを組み合わせようとしています。

Pramaanaは、法律、創薬、税務申告といった高い機密性が求められる分野に注力します。これらの分野ではミスによるコストが大きく、信頼性が極めて重要です。こうしたシステムにAIを導入するためには、現在の技術以上に強力なハルシネーションやエラー対策が必要になります。しかし、Pramaanaの共同創業者兼CEOであるRanjan Rajagopalanによれば、これらの分野は形式化にも非常に適しているとのことです。

「税務は数学に似ています。従わなければならないルールが数多く存在するからです。そのルールをコード化できれば、その上で行われる推論は決定論的なものになり始めます。」とPramaanaの共同創業者兼CEOは述べています。

Pramaanaのシステムは依然として従来型のLLM上で動作しており、自然言語による質問への回答や、従来のコンピューターでは扱えない複雑な問題への対応といった柔軟性を備えています。しかし、そのLLMの上には決定論的なレイヤーが存在し、LLMの出力結果が正しいかどうかを検証します。

LLMエンジンと決定論的検証を組み合わせるアプローチ自体は一般的です。Pramaanaの独自性は、形式検証の手法を活用している点にあります。同社は、数学的証明の検証に利用されるオープンソースのLEANプログラミング言語を活用しています。この取り組みにはフランスのCATALAプロジェクトという先例もあります。同プロジェクトでは、フランスの税制や社会保障制度の多くを実行可能なコードとして形式化しています。

Pramaanaは、それぞれのユースケースごとに独自のLEANスタイルの形式検証システムを構築し、各分野の専門家が監督します。税法分野では元IRS長官のDanny Werfelと協力しており、サイバーセキュリティおよび創薬システムについてはIIT Delhi、IIT Madras、UC Berkeleyの教授陣が監督しています。

「世界で最も難しい問題は、解決不可能なのではありません。形式化されていないだけなのです。人々の健康、資産、あるいは自由に影響を与える可能性のあるあらゆる分野にはルールが存在します。あとは、そのルールをコード化するだけです。」と同氏は述べています。