3,094
个编辑
更改
→自指的可用性依赖于编号系统：KRT 可以被分级
'''工具二（工程终点）：哥德尔机。'''Schmidhuber 把"资源有界的自引用"推到了最雄心勃勃的形式<ref name="schmidhuber2003">'''Schmidhuber, J. (2003).''' ''Gödel machines: self-referential universal problem solvers making provably optimal self-improvements''. arXiv:cs/0309048【正式版本见 LNCS 3394 (2005), 1–23 及 Springer《Artificial General Intelligence》(2006)；IDSIA 技术报告 IDSIA-19-03】</ref>：机器的初始代码包含自身硬件、环境、效用函数乃至整个初始软件的公理化描述，一个基于 Levin 通用搜索的偏置最优证明搜索器（BIOPS）持续寻找证明——'''一旦证明某个对自身代码的改写能提升未来效用，就立即改写（包括改写证明搜索器本身）'''。由于改写前必须证明"继续搜索其他改写不值当"，每次自改进都是全局最优的，没有局部极值。它的边界同样是哥德尔式的：只能改写"在形式系统内可证明有用"的部分，超出可证明范围的好处再大也拿不到。这条工程谱系与上文的[[#自省程序与自省式自改进程序|自省程序]]一脉相承：自省程序"知道自己的有界执行轨迹"，哥德尔机则"能证明地改写自己的任何部分"——自指从存在性工具，最终长成了资源有界的自改进机制<ref name="zhang2026" />。
'''工具二（工程终点）：哥德尔机。'''Schmidhuber 把"资源有界的自引用"推到了最雄心勃勃的形式<ref name="schmidhuber2003">'''Schmidhuber, J. (2003).''' ''Gödel machines: self-referential universal problem solvers making provably optimal self-improvements''. arXiv:cs/0309048【正式版本见 LNCS 3394 (2005), 1–23 及 Springer《Artificial General Intelligence》(2006)；IDSIA 技术报告 IDSIA-19-03】</ref>：机器的初始代码包含自身硬件、环境、效用函数乃至整个初始软件的公理化描述，一个基于 Levin 通用搜索的偏置最优证明搜索器（BIOPS）持续寻找证明——'''一旦证明某个对自身代码的改写能提升未来效用，就立即改写（包括改写证明搜索器本身）'''。由于改写前必须证明"继续搜索其他改写不值当"，每次自改进都是全局最优的，没有局部极值。它的边界同样是哥德尔式的：只能改写"在形式系统内可证明有用"的部分，超出可证明范围的好处再大也拿不到。这条工程谱系与上文的[[#自省程序与自省式自改进程序|自省程序]]一脉相承：自省程序"知道自己的有界执行轨迹"，哥德尔机则"能证明地改写自己的任何部分"——自指从存在性工具，最终长成了资源有界的自改进机制<ref name="zhang2026" />。
==== 自指的可用性依赖于编号系统：KRT 可以被分级 ====
==== KRT 可以被分级 ====
该词条表述的 SRT 默认在一个'''[[可接受编号]]'''（acceptable numbering，即同时满足通用性与[[s-m-n定理]]的编号系统）中工作；在此类编号之间，[[#Rogers 同构定理（1958）|Rogers同构]]保证了彼此可计算互译。一个自然的追问是：'''换掉编号，递归定理还剩多少？'''
该词条表述的 SRT 默认在一个'''[[可接受编号]]'''（acceptable numbering，即同时满足通用性与[[s-m-n定理]]的编号系统）中工作；在此类编号之间，[[#Rogers 同构定理（1958）|Rogers同构]]保证了彼此可计算互译。一个自然的追问是：'''换掉编号，递归定理还剩多少？'''