Ranjan Rajagopalan 攤開美國(guó)稅法典的打印件，紅筆劃出一段又一段條款。他在想，這些密密麻麻的文字，其實(shí)可以拆解成一串串“如果—那么”的邏輯鏈條——就像數(shù)學(xué)里的公理推導(dǎo)一樣。周三，他的公司 Pramaana Labs 宣布拿到2700萬(wàn)美元的種子輪，由 Khosla Ventures 領(lǐng)投，Accel、Boldcap、Nexus Venture Partners、Premji Invest 和 Unbound 參投。這筆錢要干的事，就是把法律、藥物發(fā)現(xiàn)、稅務(wù)這些容不得半點(diǎn)差錯(cuò)的領(lǐng)域，用形式驗(yàn)證的方法重新“格式化”一遍。

正方 CEO 的邏輯很直接：高敏感場(chǎng)景里的規(guī)則本來(lái)就像數(shù)學(xué)。報(bào)稅的時(shí)候，稅法就是一組必須遵守的規(guī)則。Rajagopalan 對(duì) TechCrunch 解釋說(shuō)：“一旦你有了編碼化的版本，基于它的推理就會(huì)變得確定起來(lái)。”換句話說(shuō)，只要把人類社會(huì)的規(guī)則寫成機(jī)器可以嚴(yán)格校驗(yàn)的形式，AI 就不會(huì)再自由發(fā)揮、胡言亂語(yǔ)。他們選擇的工具是開源的 LEAN 編程語(yǔ)言，這原本是用來(lái)驗(yàn)證數(shù)學(xué)證明的。法國(guó)有一個(gè)叫 CATALA 的項(xiàng)目，已經(jīng)把很大一部分稅務(wù)和福利體系編譯成了可執(zhí)行代碼，Rajagopalan 把這個(gè)當(dāng)作重要的先例?，F(xiàn)在，Pramaana 打算為每一個(gè)具體的行業(yè)用例，都定制一套類似 LEAN 的形式驗(yàn)證系統(tǒng)，并且每一套都由相關(guān)領(lǐng)域的專家來(lái)監(jiān)督。比如在稅務(wù)法律方面，他們已經(jīng)和前美國(guó)國(guó)稅局局長(zhǎng) Danny Werfel 展開合作；網(wǎng)絡(luò)安全和藥物發(fā)現(xiàn)這兩條線，則由印度理工學(xué)院德里分校、馬德拉斯分校以及加州大學(xué)伯克利分校的教授們來(lái)把關(guān)。

反方視角卻很自然會(huì)冒出一個(gè)疑問(wèn)：大語(yǔ)言模型最大的魅力，也是它最大的麻煩，就在于靈活。它能聽懂自然語(yǔ)言，能處理傳統(tǒng)計(jì)算機(jī)搞不定的模糊問(wèn)題，可這也正是幻覺(jué)和錯(cuò)誤的來(lái)源。即便在上面蓋了一層確定性很強(qiáng)的驗(yàn)證層，驗(yàn)證范圍到底能覆蓋多少現(xiàn)實(shí)世界中的復(fù)雜情況？稅法條文經(jīng)常互相沖突，判例的解釋也一直在變；藥物分子的相互作用常常出現(xiàn)反直覺(jué)的特例。用一套事先定義好的規(guī)則去兜住所有邊緣案例，這件事本身就未必能徹底形式化。而且，每引入一個(gè)新領(lǐng)域，就要由一批高水平的專家從頭構(gòu)建驗(yàn)證框架，這個(gè)模式能多快鋪開，也是未知數(shù)。

但回到 Pramaana 的架構(gòu)上來(lái)看，它并不是要用形式系統(tǒng)替代大語(yǔ)言模型，而是讓兩者搭班干活。底層的 LLM 依然負(fù)責(zé)對(duì)話理解、模糊查詢和復(fù)雜問(wèn)題的生成，上層則加了一個(gè)確定性檢查層，專門負(fù)責(zé)判斷模型輸出的每一步是否符合既定的規(guī)則。這種組合在業(yè)界并不罕見，只是 Pramaana 的特異之處在于把純數(shù)學(xué)領(lǐng)域的那套形式驗(yàn)證工具搬了過(guò)來(lái)。Rajagopalan 強(qiáng)調(diào)，要瞄準(zhǔn)的是那些“一旦出錯(cuò)，就會(huì)讓人損失健康、金錢或自由”的垂直場(chǎng)景。這些場(chǎng)景恰恰有一個(gè)共同點(diǎn)：它們底下都埋著一整套明文或慣例的規(guī)則，只差最后一步編碼。他的判斷是：“世界上最難的問(wèn)題，不是不可解的，而是沒(méi)有被形式化的?！?/p>

這筆2700萬(wàn)美元的融資，從布局來(lái)看，更像一波長(zhǎng)期基礎(chǔ)設(shè)施的投入。稅務(wù)合規(guī)、藥物研發(fā)審批、法律合同審核，每一條線都得慢慢啃下來(lái)。Pramaana 不只是在賣一套軟件，而是要逐個(gè)建立經(jīng)過(guò)領(lǐng)域?qū)＜冶硶囊?guī)則庫(kù)。前國(guó)稅局局長(zhǎng)的加入，側(cè)面印證了這個(gè)打法的底層邏輯：如果不先解決“誰(shuí)有權(quán)定義規(guī)則”和“規(guī)則本身是否足夠權(quán)威”這兩個(gè)前提，任何形式驗(yàn)證層都會(huì)變成空中樓閣。而學(xué)術(shù)界頂尖教授團(tuán)隊(duì)的介入，則透露出另一重信號(hào)——這種項(xiàng)目可能不是一家公司能單獨(dú)啃動(dòng)的，它必須長(zhǎng)在科研、行業(yè)和開源社區(qū)的交叉點(diǎn)上。

Rajagopalan 在采訪中沒(méi)怎么談遠(yuǎn)大的產(chǎn)業(yè)愿景，翻來(lái)覆去說(shuō)的是“規(guī)則應(yīng)該是確定的”。這句話放在一個(gè)動(dòng)輒討論通用人工智能的時(shí)代里，聽起來(lái)甚至有點(diǎn)保守。但是，當(dāng)大模型正在闖進(jìn)一個(gè)絕對(duì)不允許它犯錯(cuò)的圈子時(shí)，先老老實(shí)實(shí)把已有的規(guī)則弄清楚、寫明白，或許恰恰是最不保守的選擇。