[论文] Flood and Harvest: The Provable Necessity of Trivia for Generating Val...

论文概要

研究领域: CL
作者: Xiaoyu Li, Andi Han, Dai Shi
发布时间: 2026-06-12
arXiv: 2606.14688

中文摘要

与证明助手耦合的AI系统现在大规模生成形式数学，而检查器能验证的内容与数学家认为有价值的内容之间的差距已成为约束性限制。我们将有价值数学的生成建模为极限中的嵌套语言生成：一个可验证的形式语言F，通过成员预言机（证明检查器）访问，包含一个未知的有价值语言H，仅通过对核心C（H的子集，精确密度alpha，即文献）的对抗性枚举揭示。每个输出是有价值的（在H中）、平凡的（在F\H中）或幻觉（不在F中）。我们解决了四个问题。第一，验证器不是品味：允许广度生成的集合正是无预言机模型的集合，由Angluin条件逐纤维刻画。第二，验证器确实购买了可靠的覆盖，覆盖所有未见的有价值陈述，同时只断言有效的陈述：有它可能，没有它不可能；它将不可避免的错误从虚假重新定位为平凡。第三，也是核心地，紧密族上的尖锐二分：发射有限量平凡陈述的生成器实现最优覆盖alpha/2，而任何无限的平凡陈述允许，即使以消失速率，将最优值跳到1-alpha/2（两者都是紧的，对于呈现为候选交集的核心），而一个生成器同时达到两个端点。过渡在于平凡陈述的数量，而非速率；差距1-alpha是未记录的质量。第四，两种机制在数学压缩模型中实例化。完美的验证器不能替代品味：正确但无价值陈述的无界流不是工程事故，而是可证明的必要性，因为覆盖未记录的有价值数学需要无限但渐近可忽略的认证平凡陈述流。

原文摘要

AI systems coupled to proof assistants now generate formal mathematics at scale, and the gap between what a checker can verify and what a mathematician would value has become the binding constraint. We model the generation of valuable mathematics as nested language generation in the limit: a verifiable formal language F, accessed through a membership oracle (the proof checker), contains an unknown valuable language H in H revealed only through an adversarial enumeration of a core C subset of H of exact density alpha (the literature). Every output is valuable (in H), trivial (in F \ H), or a hallucination (not in F). We settle four questions. First, the verifier is not taste: the collections admitting generation with breadth are exactly those of the oracle-free model, characterized fiber-wi...

自动采集于 2026-06-16

#论文 #arXiv #CL #小凯