Skip to content

AutoMCM-Pro v0.3.1

Latest
Latest

Choose a tag to compare

View all tags
@RealSeaberry RealSeaberry released this 10 Sep 18:33
v0.3.1
90c4727

AutoMCM-Pro v0.3.1

v0.3.1 在 v0.3.0 自动化数学建模流水线上新增 LeanGate，并完善 Skill 的安装、更新与卸载体验。

LeanGate：Lean 4 形式化验证

LeanGate 是可选的 Lean 4 Addon，用于对数学建模中适合形式化的关键结论进行机器检查。它不替代 Python 求解、数值验证或人工审查，而是为可行性、守恒律、不变量、精确代数性质和求解证书增加由 Lean 内核裁决的验证通道。

主要能力：

  • 固定 leanprover/lean4:v4.32.0 工具链；
  • off、selected 和 required 三种启用策略；
  • 形式化适用性分类、规格语义审查与冻结；
  • Python 精确证书到 Lean 内核检查的端到端资源分配案例；
  • quality_gate.py formal 及 verify 阶段强制门禁；
  • 证明、证书、审查证据和项目配置的新鲜度跟踪；
  • 可复现形式化成果包导出。

LeanGate 会拒绝 sorry、admit、unsafe、非白名单公理、路径穿越、符号链接输入和过期证据。Agent 可生成证明，但不能通过自行撰写 PASS 绕过 Lean 编译与公理审计。

Skill 生命周期

  • 支持 Claude Code、Codex、OpenCode 和 DeepSeek Harness（DSH）；
  • 支持符号链接安装与受管拷贝安装；
  • 增加回执驱动的安全更新、回滚与选择性卸载；
  • 只在回执证明工具链由本安装器创建时，才允许显式删除 Lean 工具链；
  • 保留用户自行管理的 Python 包和 Lean 环境。

依赖授权

每个新的 Agent 会话首次触发 AutoMCM Skill 时，会询问是否准备核心 Python 建模依赖和可选 LeanGate。询问前不进行环境预扫描或静默安装；只有获得明确同意后才执行安装。Headless 运行时会显示问题并暂停，不会擅自选择。

Mind-Reader 原生启动器也改为只报告缺失依赖；仅显式传入 --install 才会调用 pip。

安装与更新

# 安装 Skill
bash install.sh

# 明确准备 LeanGate
bash install.sh --with-lean

# 更新已安装版本
bash update.sh

# 卸载
bash uninstall.sh

LeanGate 默认关闭，不会改变原有 v0.3.0 建模流程。可使用 --lean-policy selected 或 --lean-policy required 启用。

验证结果

  • 31 项自动化测试通过；
  • LeanGate 在固定 Lean 4 工具链下编译通过；
  • 安装、更新、卸载和回滚场景已覆盖；
  • OpenCode 与使用 deepseek-v4-flash 的 DSH 独立复核通过。

完整文档

  • README.md：安装、使用与免责声明；
  • CHANGELOG.md：v0.3.1 完整变更；
  • LEAN_GATE_DESIGN.md：LeanGate 技术设计、边界和验收标准。

完整性校验

SHA-256: 0dc02a00cfb8db872474ee029838fa9fbe38d90487d786998bbc86fd5fac0bfe

请下载 AutoMCM-Pro-0.3.1.tar.gz.sha256 与发布包一同校验。

Assets 4
Loading