实体
AlgoVeri
AlgoVeri
PulseAugur coverage of AlgoVeri — every cluster mentioning AlgoVeri across labs, papers, and developer communities, ranked by signal.
总计 · 30天
2
90 天内 2
发布 · 30天
0
90 天内 0
论文 · 30天
2
90 天内 2
层级分布 · 90 天
主题
最近 · 第 1/1 页 · 共 2 条
-
新的大语言模型方法通过集成规划和证明搜索来增强可验证代码生成
研究人员开发了新的可验证代码生成方法，其中大语言模型（LLMs）同时生成可执行程序和机器可检查的正确性证明。第一种方法 P$^{3}$ 集成了程序和证明规划，以提高效率和有效性，在 Lean4Commit0 等基准测试上实现了更高的解决率并降低了成本。第二种方法 Goedel-Code-Prover 在 Lean 4 中采用了分层证明搜索，将复杂的验证目标分解为更简单的子目标，在其基准测试上实现了 62.0% 的证明成功率。
-
新基准揭示AI在验证代码生成方面存在困难
一个名为AlgoVeri的新基准已被开发出来，用于评估AI模型在为经典算法生成形式化验证代码方面的性能。该基准在三种语言：Dafny、Verus和Lean中测试模型，揭示了显著的能力差距。虽然Gemini-3 Flash在Dafny中表现出中等成功，但在Verus和Lean中的表现却显著下降，这凸显了在内存约束和显式证明构建方面的挑战。