摘要
本文介紹一個以 MoonBit 實(shí)現(xiàn)的符號計(jì)算內(nèi)核 Symbit,目標(biāo)是通過AI輔助,在保留 sympy 風(fēng)格符號表達(dá)與精確計(jì)算能力的同時,將大部分算法移植到 MoonBit,利用 native 與 WebAssembly 后端提升執(zhí)行效率并降低用戶訪問門檻,理想情況下用戶只需要用瀏覽器即可訪問此計(jì)算系統(tǒng)。
我們重點(diǎn)討論表達(dá)式表示的差異化設(shè)計(jì),并通過 differential testing 與基準(zhǔn)測試評估其正確性與性能。在若干典型 workload 上,該實(shí)現(xiàn)相對原始 Python/sympy 路徑取得數(shù)倍的 native 性能提升,在瀏覽器上使用 WASM 亦可得到 2x 的平均性能提升,更提高了可訪問性。
引言
計(jì)算機(jī)代數(shù)系統(tǒng)(computer algebra system, CAS)是計(jì)算機(jī)科學(xué)和數(shù)學(xué)領(lǐng)域的重要工具,可以對表達(dá)式進(jìn)行構(gòu)造、變換、化簡與求解。與數(shù)值計(jì)算不同,符號計(jì)算更強(qiáng)調(diào)精確性、可解釋性與結(jié)構(gòu)保持,操作的對象通常是表達(dá)式樹。例如,有理數(shù)應(yīng)以精確分?jǐn)?shù)而非浮點(diǎn)近似表示,多項(xiàng)式應(yīng)保留其代數(shù)結(jié)構(gòu)而非退化為采樣結(jié)果,矩陣運(yùn)算與方程求解也往往需要在精確域上完成。
在現(xiàn)有開源生態(tài)中,sympy 以 Python 為宿主語言,為符號表達(dá)、代數(shù)變換、微積分、矩陣、方程求解和多項(xiàng)式計(jì)算等任務(wù)提供了統(tǒng)一而靈活的抽象接口。其優(yōu)勢在于能夠與 Python 的科學(xué)計(jì)算生態(tài)自然結(jié)合。
然而,這種設(shè)計(jì)也繼承了動態(tài)語言運(yùn)行時的若干工程特征:大量細(xì)粒度對象分配、深層遞歸遍歷、頻繁的動態(tài)分派,以及在表達(dá)式重寫過程中反復(fù)進(jìn)行的結(jié)構(gòu)構(gòu)造與析構(gòu)。在以表達(dá)式規(guī)范化、多項(xiàng)式操作、精確線性代數(shù)為代表的一類高頻符號負(fù)載中,這些開銷會逐步累積,并成為性能瓶頸之一。換言之,符號計(jì)算系統(tǒng)的效率問題并不總是來自「數(shù)學(xué)算法本身不夠好」,也常常來自其承載算法的數(shù)據(jù)表示與運(yùn)行時執(zhí)行模型。此外,因?yàn)?Python 是動態(tài)類型語言,sympy 的實(shí)現(xiàn)也很難通過靜態(tài)分析來保證運(yùn)行時無類型錯誤。
除了執(zhí)行效率,符號計(jì)算系統(tǒng)的可部署性同樣值得關(guān)注。盡管桌面或服務(wù)器環(huán)境中的 Python 生態(tài)已經(jīng)相當(dāng)成熟,但當(dāng)目標(biāo)場景轉(zhuǎn)向?yàn)g覽器時,傳統(tǒng)方案往往面臨更高的接入成本:用戶也許會期望「打開網(wǎng)頁即可使用」,而不是預(yù)先安裝解釋器、環(huán)境或依賴;另一方面,前端交互式教學(xué)、在線計(jì)算工具和嵌入式數(shù)學(xué)組件等應(yīng)用,也要求核心引擎能夠以更輕量的方式部署到 Web 環(huán)境中。對于此類場景而言,一個既能在 native 環(huán)境高效運(yùn)行、又能以 WebAssembly 形式直接進(jìn)入瀏覽器的符號計(jì)算內(nèi)核,具有明確的工程意義。
基于上述動機(jī),我們提出 Symbit,一個用 MoonBit 實(shí)現(xiàn)的符號計(jì)算內(nèi)核。其算法設(shè)計(jì)主要參照 sympy,但在實(shí)現(xiàn)層面上,我們重新審視了表達(dá)式對象設(shè)計(jì)、規(guī)范化、精確有理數(shù)、多項(xiàng)式操作與矩陣消元等核心結(jié)構(gòu),并通過差分測試驗(yàn)證其正確性。最后我們將在 native 與 WebAssembly 兩類環(huán)境中評估其性能表現(xiàn)。
設(shè)計(jì)邊界
本節(jié)討論我們的設(shè)計(jì)的目標(biāo)與非目標(biāo)。
語義兼容性的目標(biāo)
Symbit 的首要目標(biāo)是在可觀測語義上盡可能保持 sympy 風(fēng)格的符號行為。這里的「可觀測語義」至少包括四層:
API 的基本行為:一個用戶在構(gòu)造表達(dá)式、調(diào)用化簡、求解、多項(xiàng)式操作或矩陣運(yùn)算時,得到的對象種類與主要結(jié)果形態(tài)應(yīng)與 sympy 保持一致;
對象語義:例如 Add、Mul、Pow 等核心表達(dá)式節(jié)點(diǎn)在構(gòu)造時如何進(jìn)行扁平化、系數(shù)合并、參數(shù)保序與未求值保留;
精確數(shù)值與集合語義:整數(shù)、有理數(shù)、有限集合、區(qū)間、條件集合等對象必須按照精確代數(shù)語義傳播,而不能為了簡化實(shí)現(xiàn)輕易退化為浮點(diǎn)近似或字符串占位丟失信息;
觀測語義:打印、展示與前端集成行為,這一層較為靈活,輸出字符串可與 sympy 不同,但是語義等價。
工程目標(biāo)
在語義兼容之外,Symbit 將通過新的實(shí)現(xiàn)基座改善執(zhí)行效率,尤其是 native 場景下的表達(dá)式重寫、多項(xiàng)式計(jì)算、精確矩陣運(yùn)算與部分求解。當(dāng)然性能目標(biāo)并不是抽象的「整體更快」盡管使用 MoonBit 重寫確實(shí)可以免費(fèi)獲得這一點(diǎn),但更多的也包含一些算法決策級別的優(yōu)化。
MoonBit 是多后端編程語言,這帶來了一些額外好處:我們可以近乎免費(fèi)地獲得 WebAssembly 部署能力,理論上用戶可以直接在瀏覽器中使用 Symbit,而不需要安裝 Python 環(huán)境或依賴。這對于在線教學(xué)、交互式計(jì)算工具和嵌入式數(shù)學(xué)組件等應(yīng)用場景具有明顯的吸引力。令人驚喜的是,我們最終也完成了這個目標(biāo)。
非目標(biāo)
Sympy 有部分包還依賴于 Python 的一些特性,例如 multidispatch 利用 class 機(jī)制做多重分派,這在 MoonBit 中并無直接對應(yīng),也有依賴于其他復(fù)雜 Python 庫的包,例如 plotting 依賴于 matplotlib,因此本文并不宣稱已經(jīng)完整遷移 sympy 全部頂層包,而是把目標(biāo)限定在核心 symbolic engine 相關(guān)的包,例如 core、polys、matrices、solvers 等,它們占據(jù)了 sympy 90% 的代碼。
評估邊界
我們采用如下方法評定 Symbit 的完成度:
新增功能必須同時具備局部行為測試與 parity/oracle (差分) 測試,且后者必須覆蓋到核心語義邊界;
通過靜態(tài)類型系統(tǒng)把所有類型錯誤暴露在編譯階段,而不是運(yùn)行時;
在 native 場景下,Symbit 的算法應(yīng)該比對應(yīng)的 sympy 算法有數(shù)倍的性能提升。
系統(tǒng)架構(gòu)
一個符號計(jì)算系統(tǒng)的難點(diǎn)在于如何將這些算法如何被組織到統(tǒng)一的對象模型之下,否則就很難稱為一個「系統(tǒng)」,而更像是一些獨(dú)立的工具庫。如果表達(dá)式表示、精確數(shù)值、多項(xiàng)式、矩陣和求解器各自維護(hù)一套局部規(guī)則,那么系統(tǒng)規(guī)模一旦變大,就會出現(xiàn)語義不一致、重復(fù)實(shí)現(xiàn)、難以測試等問題。因而本章節(jié)將討論 Symbit 的整體架構(gòu),以及它與 sympy 在組織方式上的相似與不同。
Sympy 的對象模型
Sympy 的核心是圍繞 Basic / Expr 的基于類繼承的表達(dá)式樹。無論是 Add、Mul、Pow 這表表達(dá)式基礎(chǔ)結(jié)構(gòu),還是矩陣、集合、關(guān)系、函數(shù)應(yīng)用與特殊對象,都需要接入這一套動態(tài)對象模型,通過繼承來組織表達(dá)式,其關(guān)系大致是 Add <: Expr <: Basic,在解析 + 的時候會構(gòu)造一個 Add 對象,Add 的參數(shù)又是其他 Expr 對象,依此類推。一旦某個對象被納入 Basic 體系,它就自動獲得了打印、比較、替換、遍歷、匹配、重寫等一系列通用能力。
classBasic(Printable):
__slots__ = ('_mhash','_args','_assumptions')
is_number =False
is_Atom =False
is_Symbol =False
is_Add =False
is_Mul =False
is_Pow =False
...
@sympify_method_args
classExpr(Basic, EvalfMixin):
__slots__ = ()
...
這讓系統(tǒng)在可擴(kuò)展性和可讀性上都非常成功,特別適合逐步長出一個覆蓋面極廣的 CAS 生態(tài)。但它也存在許多不足:很多原本可以在更低層被隔離的成本,最終都會回落到通用對象系統(tǒng)中,例如對象構(gòu)造開銷、動態(tài)分派、運(yùn)行時比較與容器重建。并且因?yàn)?Python 的動態(tài)類型系統(tǒng),若寫出類型 / 類不匹配的問題時很難在編譯階段發(fā)現(xiàn)。
Symbit 的代數(shù)數(shù)據(jù)類型
Symbit 在總體上仍然保留了 sympy 的主題劃分,例如 symcore、sympolys、symmatrices、symsolvers、symsimplify 等包大體對應(yīng)上游的數(shù)學(xué)模塊。其中最底層的是 symcore 與 symnum。前者負(fù)責(zé)表達(dá)式節(jié)點(diǎn)、規(guī)范化、比較、替換、遍歷以及若干基礎(chǔ)對象語義,后者則提供精確整數(shù)、有理數(shù)以及部分?jǐn)?shù)值兼容層 (因此我們也重寫了 Python 的任意精度浮點(diǎn)數(shù)庫 mpmath)。
盡管我們可以用 tagless final 和 trait 來模仿 class 風(fēng)格的代碼組織,但這里我們選擇了一種更直接的風(fēng)格:用一個單一的代數(shù)數(shù)據(jù)類型來表示所有表達(dá)式節(jié)點(diǎn),因此 Parser 的代碼會相對耦合一些,借助模式匹配和窮盡檢查等功能(擴(kuò)展變體可讓類型檢查器發(fā)現(xiàn)遺漏之處),代碼也能保持相當(dāng)清晰。
pub(all)enumExpr{
Number(@symnum.BigRational)
Float(Float)
NumberSymbol(NumberSymbolKind)
Boolean(Bool)
Apply(Expr, Array[Expr])
Add(Array[Expr])
Mul(Array[Expr])
Pow(Expr, Expr)
Mod(Expr, Expr)
Tuple(Array[Expr])
Dict(Array[(Expr, Expr)])
...
}
這本質(zhì)上算是一個表達(dá)式問題,但考慮到未來 MoonBit 可能會加入 Extensible Variants 的支持,且數(shù)學(xué)領(lǐng)域很多東西也是多年不變的,我們認(rèn)為此種做法或不會受到太多維護(hù)成本的影響,并且相比 sympy 在許多方面是更優(yōu)的。另一方面,sympy 很多表達(dá)式處理都是借助節(jié)點(diǎn)的「內(nèi)在屬性」,因而有時候需要傳遞一些額外的參數(shù)來維持這些屬性,例如evaluate=False來控制是否在構(gòu)造時進(jìn)行規(guī)范化。
classAdd(Expr, AssocOp): ... classAssocOp(Basic): @cacheit def__new__(cls, *args, evaluate=None, _sympify=True): ...Symbit 則使用「智能構(gòu)造子」形式來應(yīng)對不同場景的規(guī)范化需求,可以在一定程度上解耦合(實(shí)際上,在編寫 Symbit 引擎的過程中我們還發(fā)現(xiàn)了 sympy 真實(shí)存在的因?yàn)閰?shù)傳遞和弱類型導(dǎo)致的 bug):
pubfnexpr_new_raw(op:ExprOp,args:Array[@symcore.Expr])-> @symcore.Expr{
matchop{
ExprOp::Add => @symcore.raw_add(args)
ExprOp::Mul => @symcore.raw_mul(args)
ExprOp::Pow => @symcore.raw_pow(args[0], args[1])
ExprOp::Function(name) => @symcore.raw_function(name, args)
...
}
}
pubfnexpr_new_eval(op:ExprOp,args:Array[@symcore.Expr])-> @symcore.Expr{
matchop{
ExprOp::Add => @symcore.add(args)
ExprOp::Mul => @symcore.mul(args)
ExprOp::Pow => @symcore.pow(args[0], args[1])
ExprOp::Function(name) => @symcore.function(name, args)
...
}
}
在此之上則是各種代數(shù)基礎(chǔ)設(shè)施包,例如之前提到的 sympolys 和 symmatrices (分別用于多項(xiàng)式處理和矩陣計(jì)算)。還有一個 sympy 包,顧名思義,是一個 parity 層,專門用來調(diào)用 sympy 進(jìn)行 oracle 測試。下一節(jié)我們將討論它的設(shè)計(jì),以及它在整個系統(tǒng)中的作用。
測試系統(tǒng)
符號系統(tǒng)面對的是結(jié)構(gòu)對象,這些對象往往存在多種語義等價但結(jié)構(gòu)不同的表示形式,并且很多錯誤并不會立刻表現(xiàn)為程序崩潰,而是表現(xiàn)為規(guī)范形不穩(wěn)定、定義域被忽略、過早求值或錯誤地返回了一個看似合理的表達(dá)式。因此,Symbit 的測試系統(tǒng)從一開始就并不只是依賴于簡單的單元測試,而采用一個分層驗(yàn)證體系:用快照測試記錄可觀察表示,用行為測試約束局部語義,用 parity / oracle 測試對照 sympy,并在必要時直接嵌入 CPython 運(yùn)行時來復(fù)用其參考語義。
更形式化地說,我們希望驗(yàn)證的并不是單個函數(shù)的一個輸出值,而是一個 MoonBit 實(shí)現(xiàn) f_mb與一個 sympy 參考實(shí)現(xiàn) f_sp在輸入域 D 上的觀測等價性(當(dāng)然,D 的表示也因語言不同而存在差異)

其中關(guān)系 并不總是簡單的字符串相等。在某些場景下,可以是完全結(jié)構(gòu)相等;在另一些場景下,它可能是經(jīng)規(guī)范化后的表達(dá)式相等、殘差為零(下方公式) 、集合意義下等價,或在浮點(diǎn)物理量場景中滿足一定誤差界,測試設(shè)計(jì)者應(yīng)該根據(jù)對象語義選擇合適的比較關(guān)系。

MoonBit 的快照式測試
在最基礎(chǔ)的一層,Symbit 大量使用 MoonBit 自帶的 inspect(..., content=...) 風(fēng)格測試來記錄穩(wěn)定輸出。這種測試主要用來固定一段當(dāng)前實(shí)現(xiàn)的可觀察表示,尤其適合打印器、parser、debug representation 以及某些公開 API 的回歸驗(yàn)證。與傳統(tǒng)手寫 assert_eq 相比,這種寫法在符號系統(tǒng)里尤其自然,更大的便利是當(dāng)輸出改變時可以直接給出 diff,檢查正確后可用 moon test -u 來更新快照,而不需要手動修改斷言文本。如果沒有成體系的快照更新機(jī)制,這類工作往往會退化成機(jī)械地逐條修改斷言文本,既低效,也容易遺漏。
test"prelude constructors round trip through printers"{
letexpr = add([
integer(1),
mul([Symbol("x"), pow(Symbol("y"),integer(2))]),
])
debug_inspect(expr, content="(+ (* sym:x (^ sym:y 2)) 1)")
inspect(expr, content="x*y**2 + 1")
}
這里的兩個 inspect 實(shí)際上對應(yīng)兩類不同的斷言。前者是內(nèi)部結(jié)構(gòu)快照(通過 Debug trait 實(shí)現(xiàn)),用來保證表達(dá)式構(gòu)造與規(guī)范化沒有悄悄改變底層表示;后者是用戶可見輸出快照,用來保證打印行為與 API 接口的穩(wěn)定性。這兩類快照都很重要,因?yàn)閷τ诜栂到y(tǒng)而言, 「內(nèi)部結(jié)構(gòu)變化但外部字符串不變」與「外部字符串變化但內(nèi)部結(jié)構(gòu)不變」都可能導(dǎo)致一些意外的回歸問題。
Oracle / Parity Testing 的原理
僅靠快照測試仍然不夠。符號系統(tǒng)中更難的問題在于, 「看起來不同」的結(jié)果可能是等價的,而「看起來合理」的結(jié)果也可能在語義上是錯的。因此,Symbit 在包級遷移中采用了第二層測試機(jī)制:在 src/sympy/* 下維護(hù)一棵鏡像式的 parity/oracle 樹(諭示機(jī)),專門把 MoonBit 的實(shí)現(xiàn)結(jié)果與 sympy 參考結(jié)果進(jìn)行對照。這一層基本上綁定了 sympy 全部的外部接口。而實(shí)現(xiàn)層應(yīng)永遠(yuǎn)不依賴 sympy,只有測試層可以調(diào)用 sympy 作為參考語義。也就是說,MoonBit 代碼能夠算出自己的答案,而 oracle 層會將這個答案轉(zhuǎn)換成 sympy 對象,并調(diào)用 sympy 對應(yīng)的 API 來驗(yàn)證它的正確性?;蛘咧苯訉⑼瑯拥妮斎?轉(zhuǎn)換為 sympy 對象并調(diào)用 sympy 函數(shù),得到結(jié)果后與 symbit 進(jìn)行比較。
在代碼層面上, symbit/src/sym* 負(fù)責(zé)實(shí)現(xiàn),而 symbit/src/sympy/* 則按包鏡像上游模塊,包含 *_oracle.mbt、*_port_test.mbt、port_support_test.mbt 等文件。例如 core、polys、solvers、physics 等子樹都各自維護(hù)了對應(yīng)的 oracle 層。
在比較關(guān)系 R 的設(shè)計(jì)上,正如我們之前所言,Symbit 并不假設(shè)所有對象都適合用同一種比較方式。實(shí)踐中我們主要使用了三類 parity 技巧。
第一類是直接的結(jié)構(gòu)或文本 oracle。如果一個對象的輸出形式本身就是穩(wěn)定語義的一部分,例如 srepr、latex 或某些調(diào)試表示,那么最直接的做法就是把 MoonBit 對象轉(zhuǎn)換成 sympy 對象,再調(diào)用 sympy 的對應(yīng) printer 取得參考輸出,并和 MoonBit 的序列化結(jié)果進(jìn)行字符串比較。例如 core_oracle 中:
pub fn core_expr_sstr(expr :@symcore.Expr) ->Stringraise {
letobj =@sympy.expr_to_sympy(expr)
py_str_obj(
objenum_to_obj(
sympy_call_must("sympy.sstr", [@sympy.OracleArg::PyObj(obj)]),
),
)
}
第二類是經(jīng)規(guī)范化后的表達(dá)式等價。對于許多代數(shù)結(jié)果而言,直接比較字符串會過于脆弱。例如 x - y 與 -y + x 在文本上不同,但在表達(dá)式意義下等價。這時更合適的比較關(guān)系是:

這種比較方式特別適合 simplify、factor、expand、solve 等場景。在求解器中,進(jìn)一步常見的做法是比較殘差而不是比較解的打印形式。如果一個候選解 滿足

并且其定義域條件與 sympy 一致,那么即便解集的內(nèi)部排列或局部打印形式不同,它仍然應(yīng)被視為正確結(jié)果。因此在 solver oracle 測試中,我們可以運(yùn)行最后的結(jié)果放置在無序容器中進(jìn)行比較,而不是試圖要求所有結(jié)果逐字符一致。
第三類是數(shù)值近似語義的 oracle。這類場景主要出現(xiàn)在物理、控制、繪圖或某些數(shù)值 API 中。在這些路徑里,sympy 本身也未必總返回純精確對象,而 MoonBit 側(cè)有時會經(jīng)過不同的數(shù)值后端或離散化過程。此時更合適的關(guān)系通常是

這類比較在系統(tǒng)中并不是主流,但它們提醒我們:oracle 測試的關(guān)鍵不在于「永遠(yuǎn)追求字符串一致」,而在于為每種對象語義選擇恰當(dāng)?shù)谋容^關(guān)系。
sympy 對象構(gòu)造
在 parity/oracle 測試?yán)?,我們盡量直接通過 FFI 構(gòu)造 sympy 對象,而不是先把 MoonBit 表達(dá)式打印成字符串再交給 Python 解析。如果 oracle 建立在字符串 round-trip 之上,那么 parser、printer 與對象橋接這三類問題就會纏在一起。此時一旦出現(xiàn)不一致,很難判斷究竟是 MoonBit 側(cè)對象語義錯了,還是打印錯了,還是 Python 側(cè)解析路徑改變了,非常不利于 debug。
因此,在 pybridge.mbt 中, Symbit 把 Expr 直接映射到 sympy 對象:
pub fn expr_to_sympy(expr :@symcore.Expr) ->@py.PyObject raise {
letdummy_cache : Map[Int,@py.PyObject] = {}
letwild_cache : Map[String,@py.PyObject] = {}
expr_to_sympy_cached(
@symcore.normalize_legacy_expr(expr),
dummy_cache,
wild_cache,
)
}
更進(jìn)一步,Add、Mul、Pow這些對象在橋接時會顯式傳入evaluate=false,以保留結(jié)構(gòu)語義而不是讓 sympy 在橋接階段重新化簡:
@symcore.Expr::Add(args) =>
sympy_nary_obj("sympy.Add", args,"0", dummy_cache, wild_cache, kwargs={
"evaluate":OracleArg::Bool(false),
})
@symcore.Expr::Mul(args) =>
sympy_nary_obj("sympy.Mul", args,"1", dummy_cache, wild_cache, kwargs={
"evaluate":OracleArg::Bool(false),
})
@symcore.Expr::Pow(base, exp) =>
sympy_call_obj(
"sympy.Pow",
[OracleArg::PyObj(base_obj),OracleArg::PyObj(exp_obj)],
kwargs={"evaluate":OracleArg::Bool(false) },
)
因?yàn)?oracle testing 想比較的是「兩個系統(tǒng)對同一對象的理解是否一致」,而不是「MoonBit 打印出的字符串能否再次被 sympy 接受并重寫成某種形態(tài)」。通過對象級橋接,oracle 層可以最大程度剝離 parser/printer 噪聲,把測試焦點(diǎn)放回真正的符號語義上。
利用 CFFI 接入 CPython 運(yùn)行時的經(jīng)驗(yàn)
要讓上述 parity/oracle 機(jī)制可用,還需要一個現(xiàn)實(shí)前提: MoonBit 必須能夠穩(wěn)定地嵌入 CPython 運(yùn)行時,并以足夠低的摩擦調(diào)用 sympy。在 Symbit 中,這部分實(shí)現(xiàn)集中在 symbit/src/sympy 這層 Python bridge。從代碼組織上看,它又可以拆成三小層:
types.mbt:定義跨邊界參數(shù)類型 OracleArg
py_pack.mbt:負(fù)責(zé)參數(shù)打包與 Python 對象構(gòu)造
py_call.mbt / pybridge.mbt:負(fù)責(zé)運(yùn)行時初始化、調(diào)用和對象級橋接
例如 types.mbt 中,所有跨邊界參數(shù)都先被封裝成一個統(tǒng)一的代數(shù)數(shù)據(jù)類型:
pub(all)enumOracleArg{
Null
Str(String)
Int(Int)
Bool(Bool)
StrList(Array[String])
IntList(Array[Int])
List(Array[OracleArg])
Dict(Map[String, OracleArg])
PyObj(@py.PyObject)
}
有了這些方便的函數(shù)我們就不必再到處手寫不同的 FFI 調(diào)用,而是通過一層統(tǒng)一的參數(shù)打包協(xié)議。絕大多數(shù) oracle helper 都可以在 OracleArg 這一層復(fù)用相同的參數(shù)傳遞邏輯,而不用每個包都自己拼接 Python 參數(shù)。
隨后在 py_pack.mbt 中,這些參數(shù)被打包成真實(shí)的 Python 對象:
pubfnpy_pack(arg:OracleArg)-> @py.PyObject{
matcharg{
OracleArg::Str(s) => @py.PyString::from(s).obj()
OracleArg::Int(n) => @py.PyInteger::from(n.to_int64()).obj()
OracleArg::Bool(b) => @py.PyBool::from(b).obj()
OracleArg::PyObj(obj) => {
@cpython.py_incref(obj.obj_ref())
obj
}
...
}
}
一個常見的坑時引用計(jì)數(shù)問題,但跨邊界傳入現(xiàn)有的 PyObj 時,必須顯式 incref,否則一些的生命周期錯誤會非常難查(它們甚至看起來是隨機(jī)發(fā)生的)。
oracle 層盡量不依賴「把字符串塞進(jìn) Python 的 eval 函數(shù)」,這對代碼可讀性、錯誤定位和測試穩(wěn)定性都非常不利。我們僅在 core_oracle.mbt 等受限場景下調(diào)用 Python eval,但這類邏輯主要用于便捷地獲取參考值;而真正從 MoonBit 對象進(jìn)入 sympy 對象的主路徑,仍然是前面提到的 expr_to_sympy。這種分工可以概括為:

而不應(yīng)該是

后者雖然實(shí)現(xiàn)更快(且我們早期確實(shí)希望通過這個簡化實(shí)現(xiàn),但帶來的收益不如帶來的麻煩多),但它把 parser、printer、引用環(huán)境和語義比較混成了一條鏈,對于遷移工程來說噪聲過大。
最后,CFFI 接入還有一個經(jīng)驗(yàn)是:橋接層必須被視為「測試基礎(chǔ)設(shè)施」,而不是「核心實(shí)現(xiàn)的一部分」。實(shí)現(xiàn)層不能夠依賴 sympy_call(...) 這類接口來獲得最終結(jié)果,否則整個遷移項(xiàng)目就會失去意義。
評估
到目前為止,本文討論了系統(tǒng)目標(biāo)、對象架構(gòu)、一個代表性多項(xiàng)式算法以及測試與 oracle 機(jī)制。最后一個問題自然是:這些設(shè)計(jì)在實(shí)際運(yùn)行中帶來了什么結(jié)果。對于一個 CAS 實(shí)現(xiàn)而言,評估不能只給出若干「更快」的例子,因?yàn)榉栂到y(tǒng)的性能高度依賴負(fù)載的結(jié)構(gòu):有些路徑主要受精確算術(shù)支配,有些受表達(dá)式重寫支配,有些則受數(shù)據(jù)結(jié)構(gòu)構(gòu)造、項(xiàng)排序與規(guī)范化頻率支配。因此我們應(yīng)該給不同的包,挑選大部分具有代表性的 API 進(jìn)行測試,實(shí)踐中我們借助 symbench 把負(fù)載按包與 API 家族組織起來,分別給出 native 與 WebAssembly 路徑上的結(jié)果。
實(shí)際上這里還有個相當(dāng)有趣的問題就是構(gòu)造「有趣」的數(shù)學(xué)表達(dá)式以用于測試,這并非一個顯然的問題,我們使用了很多 property based testing 中的生成器設(shè)計(jì)方法來完成此事,對此感興趣的讀者可以見我們之前發(fā)表的關(guān)于 QuickCheck 的文章。
評估方法
Symbit 的 benchmark 系統(tǒng)建立在 symbench 之上。每個 benchmark case 都包含三部分:MoonBit 側(cè)輸入構(gòu)造器、sympy 側(cè) oracle 定義,以及統(tǒng)一的運(yùn)行入口。在進(jìn)入計(jì)時之前,所有 case 都必須先通過語義校驗(yàn),也就是先確認(rèn)

再把同一 workload 交給基準(zhǔn)腳本計(jì)時。無論何時我們都應(yīng)該先驗(yàn)證語義正確性,再比較性能,畢竟更快地得到錯誤結(jié)果并沒有什么意義。
考慮到 Python 具有啟動成本,benchmark 為盡可能聚焦算法內(nèi)核本身的運(yùn)行代價,應(yīng)該啟動之后多次重復(fù)執(zhí)行同一樣例來攤薄啟動成本。至于 Symbit 則使用 native-binary + release 路徑,在這一定義下,本文采用如下速度比:

若該值大于 ,則表示 Symbit 更快。本文收集了幾種常見這些報表按負(fù)載家族分別整理,例如 sympolys-all、symsolvers-all、symseries-all 等,基本上也能對應(yīng)到 symbit / sympy 的包結(jié)構(gòu)。
基準(zhǔn)測試結(jié)果
Native 路徑上的結(jié)果相當(dāng)不錯,在當(dāng)前已經(jīng)整理成穩(wěn)定分包報表的 workload 上,Symbit 在多數(shù)包內(nèi)都取得了穩(wěn)定領(lǐng)先,且這種領(lǐng)先并不局限于某一種類型的算法。在多項(xiàng)式、求解器、整數(shù)論、級數(shù)、集合運(yùn)算、積分以及部分組合函數(shù) workload,都表現(xiàn)出了明顯的優(yōu)勢。
下表匯總了若干當(dāng)前已經(jīng)穩(wěn)定維護(hù)的分包報表。其中「范圍」表示該包內(nèi)最慢與最快樣例的加速比區(qū)間,而「代表 case」則列出若干最能體現(xiàn)該類 workload 特征的樣例。

下圖給出了 symseries 分包報表中的加速比分布,可以直觀看到不同多項(xiàng)式工作負(fù)載之間的差異。其中橫軸是具體 benchmark 樣例,縱軸是相對于 sympy 的加速比。

可見不同的負(fù)載均得到了提升,而不是某一個特例。更多結(jié)果表明,在 sympolys 中,gcd、resultant、discriminant、sturm sequence、Groebner basis 與有理插值都明顯快于 sympy;在 symsolvers 中,線性方程組、非線性方程組、solveset 與線性規(guī)劃也都表現(xiàn)出穩(wěn)定優(yōu)勢。這說明速度提升并不是來自某一個特殊路徑,而是來自對象表示、規(guī)范化、精確域算術(shù)與底層算法組織方式的共同變化。在結(jié)構(gòu)更復(fù)雜、對象層成本更突出的 case 上,提升還會繼續(xù)擴(kuò)大。當(dāng)然,在一些已經(jīng)相對緊湊的組合或微積分核上,結(jié)果也可能只領(lǐng)先 1.x 到 3.x。我們也對 WebAssembly 平臺進(jìn)行了測試(對不 sympy 本地解釋),也有 1.x ~ 3.x 的整體提升,不過幅度并未有 native 這么大,它更大的優(yōu)勢是瀏覽器部署,并且輸出小巧。
結(jié)果解讀與局限
這些評估結(jié)果支持了本文的基本判斷:把 sympy 風(fēng)格的符號對象系統(tǒng)遷移到 MoonBit,并改變對象表示、規(guī)范化鏈路與底層精確算術(shù)的執(zhí)行特性,確實(shí)帶來了可觀的性能提升。在一批經(jīng)過 oracle 校驗(yàn)的代表性負(fù)載上,這種變化最終表現(xiàn)為穩(wěn)定的 native 優(yōu)勢,以及仍具競爭力的 WebAssembly 路徑。
但與此同時,本文并不將這些數(shù)字解釋為「所有符號負(fù)載都會自動得到同等提升」。首先,當(dāng)前報表雖然已經(jīng)覆蓋了多項(xiàng)式、求解器、整數(shù)論、積分、集合、級數(shù)、函數(shù)與部分微積分,但它們?nèi)匀皇墙?jīng)過篩選和構(gòu)造的 kernel family,而不是完整地覆蓋整個 sympy API 空間。其次,benchmark 結(jié)果本身也是系統(tǒng)演化過程的一部分。某些樣例在項(xiàng)目早期曾經(jīng)顯著落后,后來通過對齊 sympy 代碼路徑、調(diào)整對象表示或改進(jìn) exact kernel 而被拉回;這意味著評估系統(tǒng)同時也是性能診斷系統(tǒng),而不僅是展示系統(tǒng)。若要把它推廣為一個更完整的學(xué)術(shù)評估,還需要在未來補(bǔ)充更多內(nèi)容:例如更系統(tǒng)的 workload 分類、更大規(guī)模的隨機(jī)與性質(zhì)測試集、更細(xì)粒度的 profiler 分析,以及跨版本的 longitudinal benchmark。
綜合來看,Symbit 的評估結(jié)果并不是「證明一切都已經(jīng)完成」,而是表明這條技術(shù)路線是成立的:一個保持 sympy 風(fēng)格語義與精確計(jì)算能力的符號系統(tǒng),確實(shí)可以在編譯型語言中獲得顯著的內(nèi)核運(yùn)行收益,并同時保留進(jìn)入瀏覽器環(huán)境的現(xiàn)實(shí)可行性。
瀏覽器 Demo
本項(xiàng)目還利用 MoonBit 的多后端能力打造了一個 Symbit Web-Demo,名為 symweb:https://caimeo.space/symweb
我們將計(jì)算內(nèi)核編譯到 WASM 加速,而前端 GUI 部分則使用 Rabbita 編譯到 JavaScript。兩者之間通過一層很薄的 JSON bridge 通訊。另外借助 KaTeX 來渲染 LaTeX 輸出,整個系統(tǒng)在瀏覽器端形成了一個小型的 CAS 交互界面。 sympy 的經(jīng)典用法往往需要安裝 Python 環(huán)境、配置依賴、編寫腳本或 notebook,而我們通過 Symweb 把這些交互直接搬到了瀏覽器里,輕量用戶可以直接在頁面里編輯表達(dá)式、切換 parser 選項(xiàng)、觀察結(jié)構(gòu)化結(jié)果,并即時得到反饋。我們在 Demo 里面實(shí)現(xiàn)了大部分常用的 symbolic API,例如 simplify、expand、factor、solve、series 等,并且在一些頁面里還展示了表達(dá)式的結(jié)構(gòu)化表示、LaTeX 輸出以及求值結(jié)果等多層信息。并且頁面相當(dāng)小,整個前端代碼和內(nèi)核編譯之后不到 3 MB,相比之下若我們想要把 sympy 運(yùn)行在瀏覽器上,需要打包 Pyodide 運(yùn)行時、自己單獨(dú)寫膠水代碼和 std 支持,然后加載 sympy 和 mpmath 本體,肯定不會這么簡潔 (運(yùn)行性能更不用說了)。

Symbit Playground - caimeo.space/symweb
當(dāng)然,symweb 仍然只是一個 demo,而不是完整的 notebook 或 CAS IDE。它目前更適合展示一個函數(shù)如何解析輸入、如何形成結(jié)構(gòu)化結(jié)果、以及在當(dāng)前 kernel 中給出什么輸出,而不是承擔(dān)長會話、多文檔、任意插件或大規(guī)模可視化等更重的任務(wù)。對于這種復(fù)雜任務(wù),我們建議直接本地安裝 Symbit 體驗(yàn)。
未來工作
雖然我們已經(jīng)取得了許多進(jìn)展,但未來仍有很多工作需要完成。除了繼續(xù)部分關(guān)鍵包的語義,減少與 Sympy 在語義上的差距。并逐步推進(jìn)一些更復(fù)雜的算法實(shí)現(xiàn)和 Bug 修復(fù):即使是 Sympy 本身也有數(shù)千個 issues 待修復(fù)和 PR 等待合并,我們希望 Symbit 能一定程度上跟隨這些變化和改進(jìn),甚至走在前面。
結(jié)論
本文致此完結(jié),我們討論了 Sympy 風(fēng)格的符號表達(dá)、精確計(jì)算與常見 CAS 算法,并不必然依賴 Python 這一宿主環(huán)境。通過 MoonBit 這樣的編譯型多后端語言,可以把同樣的語義重建為一個能夠同時面向 native 與 WebAssembly 的符號計(jì)算內(nèi)核;在這一過程中,表達(dá)式表示、規(guī)范化、精確數(shù)值、多項(xiàng)式與矩陣算法、測試基礎(chǔ)設(shè)施與部署方式都會被重新組織。當(dāng)前結(jié)果表明,這條路線不僅在工程上可行,而且在若干典型 workload 上已經(jīng)能夠提供穩(wěn)定的性能收益,并形成一個真實(shí)可交互的瀏覽器前端。這并不意味著 Symbit 已經(jīng)完成,但至少說明:構(gòu)建一個編譯型、可部署、且保持精確語義的現(xiàn)代 CAS 內(nèi)核,是一條成立且值得繼續(xù)推進(jìn)的方向。
若讀者覺得這個項(xiàng)目有趣,歡迎訪問 https://github.com/CAIMEOX/symbit.git 以了解更多細(xì)節(jié)。
-
內(nèi)核
+關(guān)注
關(guān)注
4文章
1476瀏覽量
43098 -
計(jì)算機(jī)
+關(guān)注
關(guān)注
19文章
7841瀏覽量
93489 -
AI
+關(guān)注
關(guān)注
91文章
41305瀏覽量
302685 -
python
+關(guān)注
關(guān)注
58文章
4889瀏覽量
90327
原文標(biāo)題:用 MoonBit 構(gòu)建現(xiàn)代符號計(jì)算內(nèi)核:Symbit 的設(shè)計(jì)與實(shí)現(xiàn)
文章出處:【微信號:OSC開源社區(qū),微信公眾號:OSC開源社區(qū)】歡迎添加關(guān)注!文章轉(zhuǎn)載請注明出處。
發(fā)布評論請先 登錄
LMV7219電特性表里面的失調(diào)電壓和內(nèi)部滯環(huán)的計(jì)算是帶符號計(jì)算嗎?
【「AI芯片:科技探索與AGI愿景」閱讀體驗(yàn)】+AI的未來:提升算力還是智力
科學(xué)計(jì)算與matlab語言教程下載
鮮大權(quán)《西南科技大學(xué)MATLAB教學(xué)ppt課件》
高效學(xué)習(xí)Linux內(nèi)核——內(nèi)核模塊編譯
matlab與科學(xué)計(jì)算下載
用Maple和MATLAB解決科學(xué)計(jì)算問題
符號計(jì)算系統(tǒng)Mathematica電子教案
matlab主要功能
SymPy: 符號計(jì)算庫是什么
MATLAB符號計(jì)算和代數(shù)運(yùn)算
一個關(guān)于MATLAB極限的實(shí)驗(yàn)介紹和總結(jié)示例
開源編程語言MoonBit 2024年度技術(shù)盤點(diǎn)
基于MoonBit的高效符號計(jì)算內(nèi)核Symbit實(shí)現(xiàn)方案
評論