# 命题形式化：交付自然语言与形式声明的语义对照

工作单元：W-M05；版本：2026-10-21.workunits.2；复核：2026-10-20
将明确的数学定义和命题转为可编译、语义忠实的形式接口，供证明和复用；独立接收声明而非只查编译。

## 当前用法
可委派完整形式接口候选与语义检查材料；先接收题意对应，再接收证明。
依据：自动形式化及ShadowBench专属评估显示可编译与语义对应是不同指标，不继承数学证明分数。
来源状态：active
本站记录：本单元AI运行、成功率及人时均为null；未执行上述连续函数例。

条件：
- 可信原文及定义齐备
- 目标库与工具链可用
- 有能区分错题意的边界或语义检查

## 请求与范围
自然语言研究/课程命题需要进入形式库，或已有形式化被怀疑弱化原题。
定义、量词、对象域、边界和库映射同包；证明搜索可帮助暴露歧义，最终证明是否完成另按W-M01接收。

## 输入
- 原文与允许解释：可信原命题、定义、领域约定、非平凡/边界实例；哪些歧义需要显式选择。
- 目标形式项目：Lean/Mathlib工具链、可复用库、名称约定及可信原文边界；允许引入的定义/接口及既有批准基础，不能以新增未批准公理补缺库。

## 交付物
- 自然语言—形式定义/声明对应表、可编译Prop接口与锁定依赖；例如def Target : Prop := ...表达待证目标，不把命题定义当定理证明
- 边界/反例/等价改写检查及缺库项；必要shadow/双向蕴涵检查
- 题意歧义、已选解释和仍未解接口；不把占位证明当成果

## 验收
1. 对象与量词忠实
   方法：独立逐项核对隐含域、空集/零/极限、量词顺序和前提；对合法等价表达接受双向论证，不要求同字符串。
   拒收：把“所有x存在y”改“存在y所有x”；漏去非零条件使原命题变弱或无意义。
2. 编译与语义分别通过
   方法：干净项目检查定义/Prop接口可编译，不靠sorry/admit或新增未批准公理伪装接口；用原文边界实例和独立反例尝试区分原陈述/生成陈述，必要时用shadow检查。机器通过仍需明确语义对照的覆盖范围，完整证明状态单独记录。
   拒收：能类型检查但把结论加为假设；语义judge单独认定正确。
3. 后续证明接口可用
   方法：固定最终声明、依赖和定义；用小引理或已有定理检验接口组合，缺库明确交付而非伪定义。
   拒收：为了可证偷偷改定义；未告知使用者改动原目标。


## 具体例子
输入：设计例：实数连续函数在闭区间[a,b]达到最大值；区间非空、端点关系和连续性域需对照原文。
预期产物：固定项目的定义/Prop目标接口（如def Target : Prop := ...）、自然语言对应及空区间/端点相等检查；声明可独立接收，目标theorem证明后续委派。没有本例运行结果。
失败：把闭区间换成开区间或只写有上界；形式声明编译仍不能接收。

## 工作重组
以前：数学作者写自然语言定义/命题，形式化者再选库对象、补隐含条件并来回确认含义；常在证明失败后才发现声明翻译失真。
现在：代理以原文和目标项目为边界，组织定义/声明映射、库检索和边界实例；编译反馈解决接口问题，等价表达、区分性反例或试证帮助暴露语义歧义。声明语义接收后即可交给W-M01，毋须先完成主命题证明。
保留：
- 可信原文、定义和允许解释
- 形式接口与使用目的的接收
新增：
- 区分可编译与语义对齐
- 保留量词/对象域/边界的对应证据
- 把歧义与缺库接口作为可接续产物

## 人的责任与失败接管
接收者确认原文约定、歧义解释和形式接口的使用范围；代理可完成库映射、声明草拟和语义检查材料。领域接收与自动区分检查互补，不把人或模型赞同当完备语义算法，也不要求人工逐行指定翻译。
编译失败时交未映射的定义、缺库接口/依赖及可重现错误；语义未定时交候选解释、它们的形式差异和区分性实例/反例。可编译且语义对应的声明可独立接收，即使主证明未完成；明确标“声明已接收/证明未完成”，转W-M01。不得新增未批准公理消除接口难点，不把占位proof当已证成果。

## 尚待补足
- 新领域抽象定义需逐项映射
- 自动语义评价本身可能误判

## 职业与团队下一步
数学形式化、形式接口维护、研究库建设
可信原文与可编译形式接口、定义/量词对照、边界与等价表达检查；展示一次可编译却语义失配的声明及其修订。
选择目标数学领域与形式库，提交一组原文—接口对照和缺库/歧义处理记录；完整证明单独标状态，必要时接入W-M01。
/explore?purpose=career&domain=math
瓶颈在原文歧义、库对象不匹配、接口编译还是语义区分检查？
代理组织定义/声明、库检索和语义检查；接收者集中处理原文解释与接口使用取舍。声明接收与后续证明搜索分别计进展。
试点含边界、同义改写和新定义的命题；分别记录接口可编译、语义接收、缺库与歧义成本，不用证明找到与否评价翻译是否忠实。
/explore?purpose=team&domain=math

## 证据与关系
- 研究与本科数学陈述自动形式化的可靠评价：https://aclanthology.org/2025.emnlp-main.907/
  定位：Abstract；论文评测设置与BEq+、ProofNetVerif/RLM25；公开 2025-11；核查 2026-10-20；复查 2026-11-20
  支持：给出自动形式化与语义评估的研究证据。
  未覆盖：不将论文最佳分数套给本任务或2026模型。
- ShadowBench v1：语义对齐与编译率分离：https://arxiv.org/html/2608.29270v1
  定位：§3 SA-Pass；§5.1配置；§5.2编译与语义；§6专家一致性；公开 2026-08-29；核查 2026-10-20；复查 2026-11-20
  支持：支持形式陈述的shadow与专家一致性检查。；用区分性检查拒绝看似可编译的错题意。
  未覆盖：shadow不是对任意命题的完备语义算法。；本连续函数例仅任务设计，尚未验证。


## 任务级判断与证据
采用方式：分阶段接收
从证据到建议：已有专属评估使候选接口值得委派；语义评价仍不完备，故以可核对原文和可区分反例接收，而非编译率推成正确率。
当前可用性：mixed；Lean与部分数据/生成设置可获得，但ShadowBench隐藏checker不是公开可自部署验收器。公开原文/生成数据不等同完整复现同一评分；本任务可自建语义控制并独立审查。
- 自动形式化评估资料：https://aclanthology.org/2025.emnlp-main.907/
  EMNLP2025论文/配套资料；可读评估入口；不能当已安装服务。
- ShadowBench：https://arxiv.org/html/2608.29270v1
  v1 2026-08-29；公开论文、任务/提交说明及部分设置；隐藏checker未公开，本轮未提交或重放，不能称完整开源评估。

### 专属研究评估自然语言到形式声明，区分研究级上下文与本科题；不是完成证明分数。
依据身份：外部报告结果；状态：active
- 研究与本科数学陈述自动形式化的可靠评价：https://aclanthology.org/2025.emnlp-main.907/
  定位：Abstract；评测设置/BEq+；关系：direct
  支持：给出自动形式化与语义评估的研究证据。
  限制：不将论文最佳分数套给本任务或2026模型。
  核查：2026-10-20；来源状态：active
配置：EMNLP2025；ProofNet#/RLM25，BEq+与人工判断，原论文模型/采样条件限定；本文不转抄最高分为本站概率。
适用限制：不将论文最佳分数套给本任务或2026模型。

### ShadowBench在178题上，Claude Code(Opus4.8)+Numina-Lean-Agent编译率61.8%，SA-Pass为11.2%；同一配置可编译远多于语义检查通过。
依据身份：外部报告结果；状态：active
- ShadowBench v1：语义对齐与编译率分离：https://arxiv.org/html/2608.29270v1
  定位：§3、§5.2、§6；关系：direct
  支持：支持形式陈述的shadow与专家一致性检查。
  限制：shadow不是对任意命题的完备语义算法。
  核查：2026-10-20；来源状态：active
配置：arXiv v1；178研究生/研究级题；Claude Code+Opus4.8，Medium thinking，加Numina-Lean-Agent搜索/编译；每题单次运行；Table3指标与Table10配置。隐藏shadow checker不可自部署；非Agent采样参数不混入此行。
适用限制：shadow不是对任意命题的完备语义算法。
相关进展（本条判断）：
- shadow辅助命题检查可编译但错题意的声明：/explore?purpose=understand&domain=math&window=all#P-M-SHADOW
  首次公开 2026-08-29

### 按题意映射、边界实例和独立语义检查接收接口，之后再接收证明。
依据身份：有条件的编辑推断；状态：active
- ShadowBench v1：语义对齐与编译率分离：https://arxiv.org/html/2608.29270v1
  定位：§6及case studies；关系：method
  支持：用区分性检查拒绝看似可编译的错题意。
  限制：本连续函数例仅任务设计，尚未验证。
  核查：2026-10-20；来源状态：active
适用限制：本连续函数例仅任务设计，尚未验证。

## 情境变化
### 研究新定义
输入变化：抽象对象库中尚不存在。
判断变化：先接收定义接口和语义实例，缺库可独立交付。
验收变化：定义一致性、非平凡实例及与原文映射，不能为了可证换定义。
### 固定现成声明
输入变化：可信形式声明已经给定。
判断变化：直接用W-M01，不重复自动形式化。
验收变化：不允许改声明，只验完整证明。
### 既有定义的自然语言命题
输入变化：原文对象在目标库已有表示，但量词、隐含前提和表达可能不同。
判断变化：可整包委派声明及语义对照，主证明仍另收。
验收变化：核库对象/量词/边界，接受合法等价表达；有定义不代表翻译自动正确。

研究前沿：178题上的Opus4.8+Numina-Lean-Agent编译61.8%而SA-Pass11.2%，具体显示了当前该配置“能编译”与“题意对齐”的差距；这不是本形式化任务或职业普遍率。
下一项验证：以正确等价声明、弱化/换量词/假设结论三种控制校准语义验收，再试未见领域声明。
未来改判信号：
- 扩大：同义改写和新库上下文下语义对照稳定、独立专家一致；可验证检查覆盖提高。
- 收缩：只优化compile rate，无法识别循环假设或弱化；缩到接口候选。

## 与本单元直接关联的进展
### shadow辅助命题检查可编译但错题意的声明
公开 2026-08-29
语义评价比编译更贴近原目标。
支持范围：不是模型突然变强；assessmentChangedAt为空。
来源状态：active
/explore?purpose=understand&domain=math&window=all&kind=all#P-M-SHADOW

领域背景与未来情景：/explore?purpose=understand&domain=math


## 工具与采用佐证