Show HN: Formal Verification for Machine Learning Models Using Lean 4
文章介绍了使用 Lean 4 进行机器学习模型形式化验证的项目。该项目提供框架，用于指定和证明机器学习模型的属性，如鲁棒性、公平性和可解释性。核心组件包括：Lean 库，用于定义模型和属性；Model Translator，将训练模型导出为 Lean 代码；Web 界面，用于上传模型、触发验证和可视化；以及 CI/CD 流程，实现持续集成和部署。项目支持多种模型，并提供交互式 Web 界面和自动化构建流程，旨在确保高风险应用中机器学习模型的可靠性和公平性。
Show HN：使用 Lean 4 进行机器学习模型的形式化验证
导航菜单
-
产品
-
解决方案
-
资源
-
企业
搜索或跳转到...
搜索代码、仓库、用户、问题、拉取请求...
fraware / leanverifier Public
-
Framework for specifying and proving properties—such as robustness, fairness, and interpretability—of machine learning models using Lean 4.
-
License
-
Code
-
Issues 0
-
Pull requests 0
-
Actions
-
Projects 0
-
Security
-
Insights
fraware/leanverifier
机器学习模型在 Lean 中的形式化验证
欢迎来到 机器学习模型在 Lean 中的形式化验证 项目。该仓库提供了一个框架，用于使用 Lean 4 指定和证明机器学习模型的属性——例如鲁棒性、公平性和可解释性。
一个实时的、交互式的网页可以在这里访问：proof-pipeline-interactor.lovable.app
概述
在高风险应用（例如医疗保健、金融、自主系统）中，确保机器学习模型满足严格的可靠性和公平性至关重要。本项目提供：
- Lean Library：神经网络、线性模型、决策树和高级模型（ConvNets、RNNs、Transformers）的形式化定义，以及对抗鲁棒性、公平性、可解释性、单调性和敏感性分析等属性。
- Model Translator：一个基于 Python 的工具，用于将训练好的模型（例如来自 PyTorch）导出到 JSON schema，并自动生成相应的 Lean 代码。
- Web Interface：一个 Flask 应用程序，用于上传模型、触发 Lean 验证、可视化模型架构（使用 Graphviz）和查看证明日志。
- CI/CD Pipeline：一个可重现的、Docker 化的环境，使用 Lean 4 的 Lake 构建系统，并使用 GitHub Actions 进行持续集成和部署。
功能特性
- 形式化验证：证明 ML 模型的关键属性，包括对抗鲁棒性和公平性。
- 高级模型支持：可扩展以支持卷积网络、循环架构、transformers 甚至符号模型。
- 交互式 Web Portal：上传模型 JSON 文件，查看生成的 Lean 代码，触发 Lean 证明编译，并可视化模型架构。
- 自动化 Build Pipeline：Docker 和 GitHub Actions 集成，实现可靠、可重现的构建。
快速开始
- 克隆仓库:
git clone https://github.com/fraware/formal_verif_ml.git
cd formal_verif_ml
- 构建 Docker 镜像:
docker build -t formal-ml .
- 运行容器:
docker run -p 5000:5000 formal-ml
- 访问 Web 界面:
在浏览器中打开 http://localhost:5000。
有关详细的使用和贡献指南，请参阅用户指南和开发者指南。
贡献
欢迎贡献、改进和错误报告。请查看 docs/ 文件夹，了解其他开发者指南和贡献标准。
许可证
本项目采用 MIT 许可证。