反例引导的可执行语义状态抽象发现

基于摘要分析。本文研究固定计算系统中的语义表示何时能够构成独立执行的高层模型：仅能预测输出并不意味着表示包含确定后续演化所需的全部信息。作者从给定语义变量与候选辅助变量中选择状态，并合成复现系统状态转移及指定输出的高层程序。 核心难点是状态的闭合性：选入一个辅助变量后，还必须能够确定该变量的后继值，因此增加特征不一定能解决闭合问题。作者给出一个可验证的充分条件，使依赖图能够确定唯一的最小可容许状态。若不满足该条件，作者报告，即使显式有限表系统具有对合转移与常量响应，最少辅助状态选择仍为 NP-complete；在所供函数为二次函数的有理数盒域上，该问题仍为 NP-hard。 方法通过状态对反例与单状态反例区分状态信息不足和程序不可表达。作者报告，对于关于 p 个未知系数呈仿射形式的固定模板，精确合成最多需要 p+1 次验证调用；按代价排序的搜索在预设有限程序类内最优。在验证裕量为正且定义域不变性得到认证的条件下，数值合成可终止，并给出有限执行过程的误差界。这些结论均依赖所述模板、程序类与验证条件，不能直接推广到任意网络或状态空间。 作者报告，在多项式实例及十个已训练网络上展示了精确发现、不可行性认证，以及最大选择与最少选择的差异；另以 120 个有限表系统检验辅助变量更新要求对最少状态选择的影响。在相同冻结网络上更换特征库的实验进一步区分了状态充分性与程序可表达性，并展示可能存在多个极小选择而不存在最小选择。具体网络任务、特征构造、实验协议、消融及统计信息尚未验证。 本文主要贡献是计算系统抽象与程序合成的理论和验证框架，而非 EEG 解码方法。摘要未提供神经信号任务或具体迁移验证；已有 EEG 相关工作尚未检索确认，因此不能据此认定其具有 BCI 有效性。