Show HN：使用Lean 4进行机器学习模型的形式化验证

Show HN：使用Lean 4进行机器学习模型的形式化验证
Show HN: Formal Verification for Machine Learning Models Using Lean 4

原始链接: https://github.com/fraware/leanverifier

本项目利用 Lean 4 促进机器学习模型的形式化验证，这对于需要可靠性和公平性的高风险应用至关重要。它提供了一个 Lean 库，其中包含各种机器学习模型（神经网络、线性模型、决策树、卷积神经网络、循环神经网络、Transformer）及其关键属性（鲁棒性、公平性、可解释性）的形式化定义。一个基于 Python 的模型转换器可以自动将训练好的模型（例如 PyTorch 模型）转换为 Lean 代码。一个 web 界面 (proof-pipeline-interactor.lovable.app) 允许用户上传模型，触发 Lean 验证，可视化模型架构并检查证明日志。该项目包含一个 Docker 化环境和 GitHub Actions 用于持续集成，确保可重复性。用户可以克隆代码库，构建 Docker 镜像，运行容器并访问 web 界面以开始验证其模型。该项目采用 MIT 许可证，欢迎贡献代码。

Hacker News 最新 | 过去 | 评论 | 提问 | 展示 | 招聘 | 提交登录 Show HN: 使用 Lean 4 对机器学习模型进行形式化验证 (github.com/fraware) 14 分，来自 MADEinPARIS，44 分钟前 | 隐藏 | 过去 | 收藏 | 1 评论 mentalgear 4 分钟前 [–] 这看起来非常有趣——也许一些对此更了解的人可以比较一下其他框架，以及这些保证能达到什么程度？（例如，公平性似乎甚至难以客观定义）回复加入我们 6 月 16-17 日在旧金山举办的 AI 初创公司学校！指南 | 常见问题 | 列表 | API | 安全 | 法律 | 申请 YC | 联系我们搜索：

Llemma：数学领域的开放语言模型 2023-10-19

（评论） 2025-03-17

Show HN：Torch Lens Maker – PyTorch 中的可微几何光学 2025-03-21

评论 2023-10-19

原文

Welcome to the Formal Verification of Machine Learning Models in Lean project. This repository provides a framework for specifying and proving properties—such as robustness, fairness, and interpretability—of machine learning models using Lean 4.

A live, interactive webpage is available at: proof-pipeline-interactor.lovable.app

In high-stakes applications (e.g., healthcare, finance, autonomous systems), ensuring that machine learning models meet strict reliability and fairness properties is essential. This project provides:

Lean Library: Formal definitions for neural networks, linear models, decision trees, and advanced models (ConvNets, RNNs, Transformers), along with properties like adversarial robustness, fairness, interpretability, monotonicity, and sensitivity analysis.
Model Translator: A Python-based tool that exports trained models (e.g., from PyTorch) to a JSON schema and automatically generates corresponding Lean code.
Web Interface: A Flask application for uploading models, triggering Lean verification, visualizing model architectures (using Graphviz), and viewing proof logs.
CI/CD Pipeline: A reproducible, Dockerized environment using Lean 4’s Lake build system with GitHub Actions for continuous integration and deployment.

Formal Verification: Prove key properties of ML models including adversarial robustness and fairness.
Advanced Model Support: Extendable to support convolutional networks, recurrent architectures, transformers, and even symbolic models.
Interactive Web Portal: Upload model JSON files, view generated Lean code, trigger Lean proof compilation, and visualize the model architecture.
Automated Build Pipeline: Docker and GitHub Actions integration for reliable, reproducible builds.

Clone the Repository:

git clone https://github.com/fraware/formal_verif_ml.git
cd formal_verif_ml

Build the Docker Image:
```
docker build -t formal-ml .
```
Run the Container:
```
docker run -p 5000:5000 formal-ml
```
Access the Web Interface:

Open http://localhost:5000 in your browser.

For detailed usage and contribution guidelines, please refer to the User Guide and Developer Guide.

Contributions, improvements, and bug reports are welcome. Please see the docs/ folder for additional developer guidelines and contribution standards.

This project is licensed under the MIT License.

Show HN：使用Lean 4进行机器学习模型的形式化验证 Show HN: Formal Verification for Machine Learning Models Using Lean 4

Show HN：使用Lean 4进行机器学习模型的形式化验证
Show HN: Formal Verification for Machine Learning Models Using Lean 4