MathCode0.2.0发布，引入前缀缓存整形令API成本骤降九成

Math-AI 团队发布数学形式与定理证明 AI 智能体 MathCode 0.2.0，通过前缀缓存请求整形与策略控制，将 API 成本降低达 90%。新版本针对大模型在长程证明和多轮交互中的高额开销，优化提示词结构稳定性以提升 Prompt 缓存命中率。在定理证明场景下，模型需频繁读取庞大代码库与公理库。MathCode 0.2.0 引入前缀缓存请求整形诊断与策略控制 Prefix-cache request-shape diagnostics and policy controls 机制。系统屏蔽提示词头部归属以保障结构稳定性，新增多断点缓存 `MATHCODE_CACHE_MULTI_BREAKPOINT`、显式最小前缀网关与空闲感知 TTL 策略，通过底层请求形状对齐最大化 Provider 原生缓存命中率，将长会话账单压至一成。新版本还强化了任务管理与思考深度控制。为防长程运行超支，系统支持通过 MATHCODE_GOAL_MAX_TOKEN_BUDGET 设定 Token 预算上限，并限制嵌套斜 slash 命令上限防范无限循环。此外，证明会话支持通过 --effort 或 /effort 动态调整思考深度，提供 low`、`medium`、`high`、`max 等级别，且支持随时退回默认配置。在编译加速与部署方面，新版本支持外接 Project Numina 开发的编译器 Kimina Lean Server 作为子进程常驻运行，并将编译检查请求路由至 /verify 接口。同时，安装脚本 setup.sh 迎来重构，新增 --status`、`--clean 等指令，支持 release 校验和自动验证与复用系统 Lean/Lake environment 环境，降低部署门槛。[原文链接](动察 Beating)