Grigore Rosu：程序执行即证明生成，可无限产出训练数据
LingmingZhang · x · 2026-09-19
形式化方法学者 Grigore Rosu 提出「程序执行就是证明生成」：在语义框架下，程序执行扎根于形式语言语义，每一步都有依据。把这些步骤组合起来，一次有限执行就成为程序从初始状态到最终状态的推导证明。
由此带来的机会是：由于执行遵循形式规则，跨无限程序与输入，代码能供给无限多的有限执行证明，且可保留程序状态、所应用规则及推导过程——这意味着可以直接从代码生成训练数据。
「研究」频道最新
- 思维链监控不是审计日志：模型解释与其真实决策脱节 — ziv_ravid · 2026-09-19
- 多篇论文质疑思维链忠实性:填充词可涨 13 分,解释常是表演 — ziv_ravid · 2026-09-19
- TokenRhythm 发布 NeoHorse-1:4B/9B,宣称首个 RSI 闭环验证 — jiqizhixin · 2026-09-19
- 用强化学习训练语言模型写代码作画，代码可编辑替代反复调提示词 — measure_plan · 2026-09-19
- Bountied 验证子网十天攻破六道悬置数十年的 Erdős 公开难题 — markjeffrey · 2026-09-19
- 斯坦福学者：基因表达预测模型受限于数据而非规模 — anshulkundaje · 2026-09-19