arXiv 预印本Xiaoyu Li
极限语言生成的充要刻画:有限见证与分离宽度层次
原标题:Characterizing Language Generation in the Limit: Finite Witnesses and a Separation-Width Hierarch
论文75
极限语言生成要求从未知无限语言的每个穷举正例呈现中,生成有效的未见元素。我们针对可数论域上的任意语言族刻画了这一任务。当且仅当可以为每个目标分配一个有限正见证,使得由任意有限样本激活的目标具有无限公共交集时,生成才是可能的。必要性方向源于一种通用归一化:通过搜索未确认的历史,可将任何成功的生成器转换为仅依赖于已观察集合的生成器。接着,我们探讨兼容见证必须有多大。正分离宽度记录了最小的一致大小界限,此外还有两个层级分别对应无界有限见证以及不存在任何兼容有限见证分配的情形。每个层级均会出现。可数族容许单元素见证,显式构造的族能实现任意有限宽度,而两个具有无限公共核的族的并集则需要无界有限见证。最后,可数支集与有限剖面阻碍解释了为何局部组合数据无法决定极限生成。该刻画及完整的宽度层次结构已在 Lean 中得到验证,包括简化的归一化和一个直接对角线捕获引理。配套的 Lean 项目维护于 https://github.com/xiaoyulics/language-generation-characterization
为什么值得读
在形式语言与学习理论中彻底厘清了极限生成的数学充要条件,并由交互式定理证明器 Lean 完成全量形式化验证。
标签
Learning TheoryFormal VerificationLeanLanguage GenerationTheoretical Computer Science