衔接抽象数学与系统工程:用于 Rust Tiny ML 的范畴论

高层数学抽象与底层系统编程的交汇点很少是实际软件工程的沃土。通常,范畴论被归类为 Haskell 等纯函数式语言的领域,而机器学习 (ML) 则被视为一系列数值线性代数运算。然而,一个名为 Category Theory for Tiny ML in Rust 的新项目正试图通过将 ML 不仅仅视为计算,而是视为对象、变换和约束的结构化流水线来弥补这一差距。

该工作草案由 Hamze Ghalebi 和 Farzad Jafarranmani 开发,提出了一种框架,其中范畴论的数学严谨性可作为一种工程工具,用于在 Rust 中构建可靠、可审计且可维护的 ML 系统。通过将数学概念直接映射到 Rust 的类型系统,作者旨在使范畴论的“抽象废话”变得可执行且具体。

概念映射:从数学到 Rust

该项目的核心是将范畴概念转化为 Rust 编程语言的惯用法。目标是摆脱将 ML 视为张量“黑盒”的做法,转而将其视为态射 (morphisms) 的组合。

领域对象作为 Rust 类型

在范畴论中,一个范畴由对象和态射组成。在这个框架中,领域对象被直接映射到 Rust 类型。这确保了流经 ML 流水线的数据是严格类型的,从而减少了运行时错误,并使系统的架构在代码中显式化。

态射作为类型化变换

态射(对象之间的箭头)被实现为类型化变换。在 ML 的语境下,一个态射可以是一个神经网络中的层,或者是一个预处理步骤。通过将这些定义为态射,系统强调了这些函数的组合,确保一个变换的输出在数学上和程序上都与下一个变换的输入兼容。

训练作为自同态

书中一个更具启发性的想法是将训练视为一种自同态。自同态是一种将对象映射回自身的态射。在这个框架中,训练被视为模型状态的重复变换,其中状态是正在被变换以随时间提高其性能的对象。

从理论到生产

该项目由两个截然不同的视角驱动:Farzad Jafarranmani 提供的数学基础(专注于证明论和指示语义)以及 Hamze Ghalebi 的生产工程视角(专注于 GenAI 和可审计的 AI 系统)。

这种双重性旨在解决 AI 开发中的一个常见问题:原型与生产就绪系统之间的差距。通过使用 Rust,作者利用了内存安全性和性能,同时范畴论为创建可评估、可监控并保持在人类问责范围内的系统提供了蓝图。

批判性视角与社区辩论

与任何融合高层数学与系统代码的项目一样,社区的反应是复杂的,这引发了关于此类抽象实用性的重要问题。

“装饰性抽象”的批评

一些批评者认为,范畴论可能只是被“钉”在实现上。一位评论者指出,常规的类型化编程已经使用了类型来表示领域对象,并使用函数来进行变换,这表明范畴术语可能更多是描述性的而非规范性的:

"我无法理解,这对我来说看起来就像普通的 Rust,或者说普通的编程……范畴论术语可以用来描述常规类型化程序的结构。"

缺失的环节:HKTs 与定理

从更技术性的角度来看,一些开发者指出了 Rust 类型系统的局限性。具体而言,Rust 中缺乏 Higher-Kinded Types (HKTs) 使得实现某些范畴模式(如 Functors 或 Monads)不像在 Haskell 中那样优雅变得困难。

此外,一些研究人员认为,为了让范畴论在 ML 中真正发挥作用,它应该允许推导关于实现的定理。他们建议该框架应该向 Markov categories 迈进,或者使用 adjunctions 来刻画 ML 算法,这将为系统的行为提供更强的数学保证。

结论

Category Theory for Tiny ML in Rust 代表了将机器学习的“管道工程”形式化的雄心尝试。虽然怀疑论者质疑增加的数学层是否比标准类型化编程提供切实的利益,但该项目对可审计性和结构的关注为可靠 AI 的未来提供了一个引人注目的愿景。通过将数学结构转化为可执行的 Rust 代码,作者正在挑战开发者,使其不再将 ML 流水线视为一系列矩阵乘法,而是将其视为类型化变换的严谨组合。

Sources