Verimath —— AI 数学推理验证
分层验证架构：符号计算层（SymPy，确定性）→ LLM 翻译层（Lean 语句）→ 形式化裁决层（Prover）。每层只输出确定性信号，不评分。CLI 输出单行 JSON，直接解析后向用户报告。
使用流程
- 整理输入：把用户给的解题过程切分为独立步骤（每步一个可验证单元）。优先整理成符号层支持的模式（见 api_reference.md 第 2 节），如
由x^2 - 1 = 0可得x = 1或x = -1。 - 调用 CLI：按需求选子命令，见下。
- 解析并报告：把 JSON 结果转成用户可读结论，附错误定位与反例。
验证提示词
需要把任意模型/用户的自然语言解答规范化为可验证推理链时，使用 references/verification_prompt.md（角色定义 → 输出约束 → Few-Shot 示例 → CoT 引导，输出 JSON 直接对接 batch --input）。提示词中的示例步骤均已通过引擎实测。
CLI 调用
所有命令在 skill 目录下执行（SKILL_DIR=$(dirname $(dirname $0)) 或直接写绝对路径）：
# 验证单个步骤
python3 scripts/verify_cli.py step "<步骤文本>" [--problem "<题目>"]
# 批量验证整份解答（步骤多时用 --input 传 JSON 文件）
python3 scripts/verify_cli.py batch --problem "<题目>" --steps "步骤1" "步骤2"
python3 scripts/verify_cli.py batch --input cases.json
# cases.json: {"statement": "题目", "steps": ["...", "..."]}
# 多模型对比
python3 scripts/verify_cli.py compare --problem "<题目>" --input solutions.json
# solutions.json: [{"model": "m1", "steps": ["..."]}, {"model": "m2", "steps": ["..."]}]
# 数据飞轮统计（翻译盲区/反例/负样本案例库）
python3 scripts/verify_cli.py flywheel
# 自检
python3 scripts/verify_cli.py selftest
首次使用若缺依赖：pip install sympy fastapi uvicorn pydantic httpx。完整参数与输出字段见 api_reference.md。
结果解读
VERIFIED→ 步骤正确；REJECTED→ 步骤有明确错误，用error_location+error_type定位，formal_result.counterexample（如{"x": 1/2}）作为反例证据INCONCLUSIVE→ 无法判定（符号层能力外/翻译放弃/形式化未完成），不得当错误报告，如实说明"该步骤无法自动验证"layer字段告诉用户是哪个层级裁决的（symbolic / formalization）overall_status：CORRECT/INCORRECT（看first_error_step）/PARTIALLY_VERIFIED
示例结论话术：
> 第 3 步"由x > 0可得x >= 1"被形式化层判定为错误：存在反例 x = 1/2 满足前提 x > 0 但不满足结论 x >= 1。整体解答 INCORRECT，首个错误出现在步骤 1。
注意
- 默认
mock后端为演示级验证；向用户声称"形式化验证通过"前，如需内核级证明请用--backend lean_repl或axle（配置见 api_reference.md 第 3 节） - 不要修改
verimath/（vendor 的引擎包）内的代码；如需扩展符号层规则，回到主工程改后重新 vendor - 不要把 INCONCLUSIVE 折算成扣分或失败
