最初发表于tamiz.pro.
在目前人工智能的地貌下,两个截然不同的工程挑战主导了论述:模型推论的黑盒性质和复杂数据管道的脆弱性.
一方面,我们有大语言模型(LLMs)和神经网络,这些网络在统计学上强大但逻辑上不透明.
另一方面,我们拥有像ClickHouse这样的大规模实时分析平台,这些平台以极高的效率处理多字节的数据,但缺乏对应用在这些数据上的转换的正确性的语义保证.
对于建设关键AI基础设施的系统设计师来说,例如金融交易、自主车辆控制系统或保健诊断工具,这种二分法是不可接受的。
我们需要不仅迅速和可扩展,而且可数学核查的系统。
本文章探索了弥补这一差距的新建筑模式:用"精益4"正式验证AI逻辑和数据转换,用"ClickHouse"进行高通量,实时分析并存储.
通过将Lean 4 的类型理论和证明助手与 ClickHouse 的专栏存储和向量化执行相结合,我们可以创建一个AI 基础设施,在它触及生产数据之前,规范数据摄取、模型推论和输出生成的逻辑被正式证明是正确的.
这不仅仅是测试,而是通过数学证明保证正确性。
问题:AI基础设施传统软件工程中传统测试瀑布短板为何依赖于单位测试,集成测试,以及基于地产的测试.
这些方法虽然对许多领域有效,但在AI基础设施应用时却有很大的局限性: 覆盖范围差距:单位测试涵盖特定的输入-输出对.
它们无法证明一个函数对所有可能输入,特别是无限域(如实值传感器数据)的正确行为.
语义漂流:在AI管道中,数据转换(清理,特征工程)经常会涉及复杂的heuristic.
很难写出能够捕捉到变换意图的测试,只为少数样本的输出.
货币和种族条件:实时分析系统每秒处理数百万个事件.
确保数据不会被同时写作或阅读所腐蚀,这在传统测试中是众所周知的难以做到的。
模型不确定性:AI模型产生概率输出.
验证一个系统正确处理不确定性(例如拒绝低信心预测)需要推理概率和阈值,这在标准代码测试中难以表达.
正式方法,特别是互动定理的证明,提供了克服这些局限性的途径。
通过将系统属性表示为数学定理,并使用证明助手进行验证,我们就能达到测试不能提供的确定性水平.
引入Lean 4:一个可验证逻辑的证明助手Lean 4是一个强大的交互式定理证明和编程语言.
它基于依赖型理论,它使我们能够将复杂的逻辑属性表现为类型.
在Lean 4中,一个证明就是程序,一个程序就是证明.
这种统一对我们的结构至关重要。
为什么精益四为AI基础设施?
依赖类型:精度4允许我们直接将变异物编码入类型系统.
例如,我们可以定义一个只接受大于零的实际数字的类型.
这样可以防止无效数据在编译时进入我们的系统.
Metaprogramming:Lean 4拥有一个强力的metaprogramming API,让我们能够写出将验证生成和验证自动化的战术和工具.
这对于将正式核查扩大到大型密码库至关重要。
互通性:精益4可以通过FFI(Foreign函数接口)被嵌入到其他语言(如Python和Rust)中.
这样我们就可以在"精益4"中写出性能关键代码,并融入现有的AI生态系统