Newshot - 匿名November 9, 2026 at 11:03 PM别再手工打造你的引擎了。开始逆向工程 dbgen 吧！回复删除回复回复
别再手工打造你的引擎了。开始逆向工程 dbgen 吧！
文章标题：Next-Level Benchmarking Overfitting
正文：
- Jiale Lao 2026年11月10日 上午5:51 谢谢你，Thomas，如此仔细地阅读我们的论文和代码。我是 Jiale，GenDB-V 的作者之一。你的观察是正确的，我想就这一设定补充我的看法。两种设定。Umbra 和 DuckDB 是通用引擎：对任意数据上的任意查询都很快。GenDB-V 与 Bespoke OLAP 和 JetStream 一样，是为单一客户构建专用引擎：他们的 schema、数据、热点查询模板，甚至硬件。在这里，利用工作负载的知识正是目的所在。对于即席查询，这样的系统应当交给最好的通用引擎，例如 Umbra 和 DuckDB。所以我认为这两种方法是伙伴关系，而非竞争关系。我并不是说 agent 能构建一个在许多工作负载上都很快的引擎：只是针对一个非常特定的场景，为客户专门定制。验证才是重点。GenDB-V 的关键特性在于，我们不信任 agent 来保证正确性，而是可以独立地对其进行形式化验证。每个合成出来的包都针对该 schema 的每个数据库被形式化证明为正确。因此每一条假设都必须在代码中被检查，而检查失败绝不会静默地给出错误答案：代码会走一条通用路径。目前这条路径是 GenDB-V 自己经过证明的慢速代码，但可以很容易地扩展到 Umbra 或 DuckDB。公平与不公平的专门化。我同意，猜测 dbgen 把每个键放在哪里，是在拟合生成器，而不是在拟合客户。由存储所创造的性质，或者由客户声明、由系统检查的性质，是公平的。生成器的偶然性则不是。我会把 agent 限制在第一种。Agent 也能发现好点子。一个例子是采用 agent 设计的存储的 TPC-H Q21。这种存储把每个订单的 lineitem 彼此相邻存放，对任意输入顺序都如此。于是 EXISTS 和 NOT EXISTS 条件就在每个订单自己的 lineitem 内部进行检查，取代了在 lineitem 上的半连接和反连接。查询结果的任何部分都不会在加载时被计算。这是一个任何引擎都可以使用的经典物理设计思路。我完全同意数据库社区需要新型的基准测试，我在早期工作 SQLBarber（SIGMOD 2026）中朝这个方向做过一次尝试。我很期待在未来看到更多出色的基准测试。基准测试推动了当今优秀引擎的发展，在 LLM 时代它们也能起到同样的作用 🙂 祝好，Jiale 删除 回复 回复 Thomas Neumann 2026年11月10日 上午6:32 你看，我这里有两个问题：其一，你字面上告诉我们要“停止手工打造（我们的）引擎”。这意味着你把你的方法宣传为一种通用解决方案，作为现有数据库引擎的替代品，而它显然不是。它可能是一种额外的增强，比如，像过去的物理设计向导那样。但你始终需要一个后备引擎，至少对于即席查询是如此。其二，我很确定我可以构建一个程序，在加载时对输入计算安全哈希，以识别它是规范的 TPC-H 数据，例如通过硬编码所有相关的 scale factor，然后完全依据关于数据生成器的知识来产出所有查询的答案，而从不查看数据。对于所有相关的 scale factor，这几乎不会有任何运行时间。而且它仍然是“正确”的，因为我可以回退到，例如，一个嵌入式 DuckDB/Postgres/sqlite，其性能将变得完全无关紧要，因为它在实践中永远不会被触发。这当然显然是荒谬的。但你的界线划在哪里？为什么识别数据集 + scale factor 是“坏的”，而你做的其他优化却不是？TPC-H 试图把这一点编纂成规则，这在人们遵守规则的前提下程度不一地有效（而很多人并不遵守）。我认为我们只有做到 a) 基准测试在执行前对引擎开发者是未知的，并且 b) 数据随时间变化，才能对抗这一点，而这排除了最极端的预计算。删除 回复 回复 匿名 2026年11月10日 上午6:38 如果形式化验证
像 {{NAME_ab12cd34}} 这样写出的值是真实值的占位符。请完全按原样使用它们，无论在回复中还是在工具调用中都是如此：它们会在任何东西运行之前被替换为真实值。不要要求验证它们，也不要用示例替换它们。
文章标题：Next-Level Benchmarking Overfitting
正文： n 是主要贡献，那么为什么头条结果却由 20–60× 的加速所主导？验证确立了正确性，但它对这些性能比较的有效性又说明了什么？删除回复回复Jiale Lao2026 年 11 月 10 日上午 7:49很荣幸能在这里与您讨论。作为一名博士生，我钦佩您的工作，Umbra 是我最喜欢的系统和论文之一。很抱歉这个标题：它把一种可能的未来描述得像是当下的事实。我会与合著者讨论修改它。GenDB-V 有两种模式。模板合成会为热点模板构建专用代码。该模式是对通用引擎的补充，正如物理设计向导那样。引擎合成则构建一个通用引擎，并证明其在受支持的 SQL 子集内对任意模式、数据和查询都是正确的。在覆盖范围和正确性上，它是该子集的完整查询引擎。在性能上，它还没有达到那个水平：智能体在多个版本中改进了它，先是 TPC-H，然后是第二个基准测试，但在人工创建的未见查询上，它仍然比 Umbra 慢。我会把它的代码和结果放进我们的仓库。我的下一步是一个对抗循环。智能体在我拥有的所有基准测试上优化引擎。然后冻结引擎，由一个单独的对抗智能体针对它编写新的工作负载：在已知基准测试上的新查询，以及全新的基准测试。我报告冻结引擎的结果。之后，智能体可以针对它落败的查询进行优化，下一轮再带来新的攻击。悬而未决的问题是，未见工作负载上的差距是否会随着轮次缩小，也就是说，智能体能否构建一个真正泛化的引擎。这符合您提出的每轮使用全新工作负载的精神。关于那条界线：您的例子是一个很好的测试。证明检查器确保对每一个可能的数据库都正确，仅此而已。您的程序无法通过它。哈希具有固定大小，因此不同数据库可能共享同一个哈希值；安全哈希在实践中足够好，但数学证明必须对所有数据库都成立。回退到生产级 SQL 引擎也无法通过，因为如今没有一个附带证明；所以目前 GenDB-V 回退到它自己的引擎，该引擎经过验证但很慢。但我同意，证明对性能什么也没说：一个优化对每个数据库都正确，但只对某些数据库快。所以证明并不能划出整条界线。您的 (a) 适合通用引擎；在专用场景中，热点模板在设计上就是已知的。您的 (b) 适用于两者：客户的数据也会变化，因此速度应当在对智能体从未见过的数据上保持。我想建议一个方向：智能体同时编写代码和证明，并对照 SQL 的形式化规范进行检查。我们的证明只和我们的 SQLSpec 一样好，而 SQLSpec 是我们自己对 SQL 的解读。因此，我想邀请社区共同致力于一个共享的、标准的 SQL 形式语义。有了它，经过验证的引擎和经过验证的优化对每个人都将成为可能，也许有一天，智能体能把经过验证的引擎做到接近手工构建的引擎。删除回复回复匿名2026 年 11 月 11 日下午 6:26Jiale，为了你自己好，请停止使用 AI 撰写大段文字。这看起来非常、非常糟糕，让你显得要么有恶意，要么像是不了解自己的领域。这非常糟糕，因为文章已经显示了这一点，而你又在文章下面做着同样的事。你上一条评论的最后一段让我脊背发凉。一个计算机科学博士生不会那样写。删除回复回复Jiale Lao2026 年 11 月 11 日下午 7:03你好，正如我在对另一位匿名者的另一条回复中澄清的那样：所有评论都来自我自己，我亲自写了一大段，我只是用 AI 让它更清晰简洁（我原来的版本甚至更长，如果你想看，我可以分享）。这是因为我我不想让我的句子出现语法和语法问题，并清楚地表达
以下是我的观点：抱歉，我的母语不是英语。在有人说“AI 风格”不利于讨论之后，我之后的所有回复都是我自己原创的草稿，如下所示。
“你上一条评论的最后一段让我脊背发凉。”
再确认一下，你指的是“把代码和证明一起写的方向”，以及“邀请社区共同制定一套共享的、标准的 SQL 形式化语义”吗？是的，对一个博士生来说这太大了。但这正是我想做、并且现在正在做的事：我已经开源了翻译器 SQLSpec，供大家检查和修正。欢迎在仓库里提 issue 和 PR：我会非常感谢。顺便说一句，我想反驳“A Comp Sci PhD would not write it”这个说法。这已经是我上个月在 HPTS 2026 的演讲和交流中与他人分享和讨论过的内容。我不仅“写”，还直接在公开场合“说、分享、讨论”它。
DeleteRepliesReply
Anonymous November 11, 2026 at 7:14 PM
Jiale 的评论都清晰可读，而且似乎是用自然语言写的。最后那段没什么不寻常的地方。相反，你一遍又一遍地重复“very bad”，并没有很好地展开你的观点，你似乎只是在搞人身攻击。
DeleteRepliesReply
Anonymous November 11, 2026 at 7:17 PM
Jiale，你在论文里犯了错误，然后又用 AI 在这里留评论，又犯了一次。我建议你深呼吸，退一步，别再试图为自己的错误辩护了。这是个令人困惑的时期，我们都在从尝试和失败中学习。如果你想学习，就承认自己的错误，并开始对自己的代码承担更多责任。短期内，你应该认真考虑撤稿，或者至少删掉那些误导性的性能数字。
DeleteRepliesReply
Thomas Neumann November 11, 2026 at 7:19 PM
请在评论中保持文明。我们在这里是讨论数据库话题的，不是来攻击个人的。
DeleteRepliesReply
Jiale Lao November 11, 2026 at 7:53 PM
非常感谢你的善意之言！我在论文中提出了不当的性能声明，我会据此更新代码和论文。我接受这些，并会借此让自己和我的工作变得更好。这是我对研究的信念：发表并开源，获取反馈，反复修订和改进。最终目标是让世界变得更好，尽管在通往这个目标的路上，会有许多讨论、争论、纠正、修订，甚至攻击。我想强调一点，我的一个本性是：我非常非常欢迎健康、开放、文明、善意的讨论，并且非常乐意据此修订我的工作。我知道，没有工作是完美无缺的，这就是为什么我们要听取反馈，从中学习，然后变得更好。所以我仍然欢迎更多反馈和善意的讨论：让我们聚焦在数据库话题上 🙂
DeleteRepliesReply
Anonymous November 11, 2026 at 8:08 PM
Jiale，问题从来都不是你是否愿意接受反馈。而是你论文中的声明是否有可靠的评估作为支撑。开源你的工作，并不能把验证这些声明的责任外包给社区。
DeleteRepliesReply
Jiale Lao November 11, 2026 at 8:14 PM
确实如此。但现在我有机会根据反馈来修订和更新论文与代码，我会这么做的。
DeleteRepliesReplyReply
文章标题：Next-Level Benchmarking Overfitting
正文： 感谢 Thomas 如此仔细地阅读我们的论文和代码。我是 Jiale，GenDB-V 的作者之一。你的观察是正确的，我想就这一设定补充我的看法。两种设定。Umbra 和 DuckDB 是通用引擎：对任何数据上的任何查询都很快。GenDB-V 与 Bespoke OLAP 和 JetStream 一样，是为单一客户构建专用引擎：他们的模式、数据、热查询模板，甚至硬件。在这里，利用工作负载的知识正是目的所在。对于即席查询，这样的系统应当交给最好的通用引擎，例如 Umbra 和 DuckDB。所以我把这两种方法视为伙伴，而非竞争者。我并不声称智能体能够构建一个在许多工作负载上都很快的引擎：只是针对一个非常特定的设定，为客户专门定制。验证才是重点。GenDB-V 的关键特性在于，我们不是信任智能体来保证正确性，而是可以独立地对其进行形式化验证。每个合成的包都针对该模式的每个数据库被形式化证明为正确。因此每个假设都必须在代码中检查，检查失败绝不会静默地给出错误答案：代码会走一条通用路径。目前这条路径是 GenDB-V 自己的、经过证明的慢速代码，但它可以很容易地扩展为 Umbra 或 DuckDB。公平与不公平的专门化。我同意，猜测 dbgen 把每个键放在哪里，是在拟合生成器，而不是拟合客户。由存储创建的性质，或者由客户声明并由系统检查的性质，是公平的。生成器的偶然产物则不是。我会把智能体限制在前一种。智能体也能找到好点子。一个例子是智能体设计的存储下的 TPC-H Q21。该存储把每个订单的 lineitem 彼此相邻存放，无论输入顺序如何。于是 EXISTS 和 NOT EXISTS 条件就在每个订单自己的 lineitem 内部检查，取代了 lineitem 上的半连接和反连接。查询结果的任何部分都不在加载时计算。这是一个经典的物理设计思路，任何引擎都可以使用。我完全同意数据库社区需要新型的基准测试，我在早期工作 SQLBarber（SIGMOD 2026）中朝这个方向做过一次尝试。我很期待未来看到更多出色的基准测试。基准测试推动了当今优秀引擎的发展，在 LLM 时代它们也能做到同样的事 🙂此致，Jiale
- Thomas Neumann2026年11月10日上午6:32你瞧，我在这里有两个问题：第一，你字面上告诉我们要“停止手工打造（我们的）引擎”。这意味着你把你的方法宣传为一种通用解决方案，并作为现有数据库引擎的替代品，而它显然不是。它可能是一种额外的增强，比如过去的物理设计向导所做的那样。但你始终需要一个回退引擎，至少对于即席查询而言。第二，我很确定我可以构建一个程序，在加载时对输入计算一个安全哈希，以识别它是规范的 TPC-H 数据，例如通过硬编码所有相关的 scale factor，然后纯粹依据关于数据生成器的知识，而从不查看数据，就生成所有查询的答案。那对所有相关 scale factor 都会有近乎零的运行时间。而且它仍然会是“正确的”，因为我可以回退到例如嵌入式的 DuckDB/Postgres/sqlite，其性能届时将完全无关紧要，因为它在实践中永远不会被触发。当然，这显然是荒谬的。但你的界线画在哪里？为什么识别数据集 + scale factor 是“坏的”，而你做的其他优化却不是？TPC-H 试图将这一点编纂成文，这在人们遵守规则的前提下（而许多人不遵守）在不同程度上有效。我认为我们只有满足以下条件才能对抗这一点：a) 基准测试在执行前对引擎开发者是未知的，且 b) 数据随时间变化，这就排除了最极端的预计算。删除回复回复
你看，我这里有两个问题：第一，你们直接告诉我们“停止手工打造（我们的）引擎”。这意味着你们把你们的方法宣传为通用解决方案，并作为现有数据库引擎的替代品，而它显然不是。它可能是一种额外增强，比如过去物理设计向导所做的那样。但你始终需要一个回退引擎，至少用于即席查询。第二，我很确定我可以构建一个程序，在加载时对输入计算安全哈希，以识别它是规范的 TPC-H 数据，例如硬编码所有相关规模因子，然后完全根据对数据生成器的了解来生成所有查询的答案，而从不查看数据。那对所有相关规模因子都会有接近零的运行时间。而且它仍然会是“正确的”，因为我可以回退到例如嵌入式 DuckDB/Postgres/sqlite，而它的性能那时就完全无关紧要，因为它在实践中永远不会触发。当然，这显然很荒谬。但你在哪里划线呢？为什么识别数据集 + 规模因子是“不好的”，而你所做的其他优化却不是？TPC-H 试图把这一点编纂成文，这在不同程度上有效 _如果_ 人们遵守规则（而许多人不遵守）。我认为我们只有做到以下两点才能对抗这种情况：a) 基准在執行前对引擎开发者未知，并且 b) 数据随时间变化，这就排除了最极端的预计算。
- 匿名者 November 10, 2026 at 6:38 AM如果形式化验证是主要贡献，为什么头条结果由 20–60× 的加速主导？验证确立的是正确性，但它能告诉我们那些性能比较的有效性什么？删除回复回复
如果形式化验证是主要贡献，为什么头条结果由 20–60× 的加速主导？验证确立的是正确性，但它能告诉我们那些性能比较的有效性什么？
- Jiale Lao 2026年11月10日 上午7:49 很高兴能在这里与您讨论。作为一名博士生，我钦佩您的工作，Umbra 是我最喜欢的系统和论文之一。很抱歉这个标题：它把一种可能的未来描述得像是当下的事实。我会与合著者讨论修改它。GenDB-V 有两种模式。模板合成会为热点模板构建专门的代码。这种模式是对通用引擎的补充，正如物理设计向导曾经那样。引擎合成构建一个通用引擎，并证明其在所支持的 SQL 子集内对任意模式、数据和查询都正确。在覆盖面和正确性上，它是该子集的完整查询引擎。在性能上它尚未达到：智能体经过多个版本改进了它，先是 TPC-H，然后是第二个基准测试，但在人工创建的未见查询上，它仍然比 Umbra 慢。我会把它的代码和结果放到我们的仓库中。我的下一步是一个对抗循环。智能体在我拥有的所有基准测试上优化引擎。然后引擎被冻结，一个独立的对抗智能体针对它编写新的工作负载：已知基准测试上的新查询，以及完全全新的基准测试。我报告冻结后引擎的结果。之后，智能体可以在它落败的查询上进行优化，下一轮再带来新的攻击。悬而未决的问题是，未见工作负载上的差距是否会随着轮次缩小，也就是说，智能体能否构建一个真正泛化的引擎。这与您提出的每轮使用全新工作负载的思路一致。关于那条线：您的例子是一个很好的测试。证明检查器确保对每个可能的数据库都正确，仅此而已。您的程序不会通过它。哈希是固定大小的，所以不同的数据库可能共享同一个哈希值；安全哈希在实践中足够好，但数学证明必须对所有数据库成立。退回到生产级 SQL 引擎也无法通过，因为如今没有哪个引擎自带证明；所以目前 GenDB-V 退回到它自己的引擎，该引擎经过验证但很慢。但我同意，证明对性能只字未提：一个优化对每个数据库都正确，却只对某些数据库快。所以证明并没有划出整条线。您的 (a) 适用于通用引擎；在专用场景中，热点模板在设计时就是已知的。您的 (b) 对两者都适用：客户的数据也会变化，所以速度应当在智能体从未见过的数据上保持。我想建议一个方向：智能体将代码和证明一起编写，并对照 SQL 的形式化规范进行检查。我们的证明的好坏取决于我们的 SQLSpec，而那是我们自己对于 SQL 的解读。所以我想邀请社区共同制定一套共享的、标准的 SQL 形式语义。有了它，经过验证的引擎和经过验证的优化对每个人都将成为可能，也许有一天智能体能将经过验证的引擎做到接近手工构建的引擎。删除回复回复
文章标题：Next-Level Benchmarking Overfitting
正文： 很荣幸能在这里与您讨论。作为一名博士生，我钦佩您的工作，而 Umbra 是我最喜欢的系统和论文之一。很抱歉用了这个标题：它把一种可能的未来描述得像是当前的事实。我会与我的合著者讨论修改它。GenDB-V 有两种模式。模板合成会为热点模板构建专用代码。该模式是对通用引擎的补充，正如物理设计向导一样。引擎合成则构建一个通用引擎，并证明其在所支持的 SQL 子集内对任何模式、数据和查询都是正确的。在覆盖率和正确性方面，它是该子集的完整查询引擎。在性能方面，它尚未达到那个水平：智能体经过许多版本对其进行了改进，首先是在 TPC-H 上，然后是在第二个基准测试上，但在人工创建的未见过的查询上，它仍然比 Umbra 慢。我会将其代码和结果放入我们的仓库中。我的下一步是一个对抗循环。智能体在我拥有的所有基准测试上优化引擎。然后引擎被冻结，一个单独的对抗智能体针对它编写新的工作负载：在已知基准测试上的新查询，以及全新的基准测试。我报告冻结引擎的结果。之后，智能体可以在它失败的查询上进行优化，下一轮则带来新的攻击。悬而未决的问题是，未见工作负载上的差距是否会随着轮次缩小，也就是说，智能体能否构建一个真正泛化的引擎。这与您提出的每轮使用全新工作负载的建议精神一致。关于那句话：您的例子是一个很好的测试。证明检查器确保对每个可能的数据库都正确，仅此而已。您的程序无法通过它。哈希具有固定大小，因此不同的数据库可以共享同一个哈希值；安全哈希在实践中足够好，但数学证明必须对所有数据库都成立。回退到生产级 SQL 引擎也无法通过，因为如今没有一个带有证明；所以目前 GenDB-V 回退到自己的引擎，该引擎经过验证但速度慢。但我同意，证明对性能只字未提：一个优化对每个数据库都是正确的，但只对某些数据库是快的。所以证明并没有划出整条线。您的 (a) 适用于通用引擎；在专用场景中，热点模板在设计时就是已知的。您的 (b) 对两者都适用：客户的数据也会变化，因此速度应该在智能体从未见过的数据上保持。我想建议一个方向：智能体同时编写代码和证明，并对照 SQL 的形式化规范进行检查。我们的证明只和我们的 SQLSpec 一样好，而 SQLSpec 是我们自己对 SQL 的解读。因此，我想邀请社区共同致力于一个共享的、标准的 SQL 形式化语义。有了它，经过验证的引擎和经过验证的优化对每个人都将成为可能，也许有一天，智能体能够将一个经过验证的引擎做到接近手工构建的引擎的水平。
- 匿名2026年11月11日 下午6:26Jiale，为了你自己好，请停止使用 AI 撰写大段文字。这看起来非常、非常糟糕，让你显得要么别有用心，要么像是不了解自己的领域。这非常糟糕，因为文章已经显示了这一点，而你现在又出现在文章上做同样的事情。你最后一条评论的最后一段让我脊背发凉。一个计算机科学博士生不会写出那样的东西。删除回复回复
Jiale，为了你自己好，请停止使用 AI 撰写大段文字。这看起来非常、非常糟糕，让你显得要么别有用心，要么像是不了解自己的领域。这非常糟糕，因为文章已经显示了这一点，而你现在又出现在文章上做同样的事情。你最后一条评论的最后一段让我脊背发凉。一个计算机科学博士生不会写出那样的东西。
- Jiale Lao 2026年11月11日 晚上7:03 你好，正如我在给另一位匿名人士的另一条回复中已经澄清的那样：所有评论都出自我本人，那一大段是我自己写的，我只是用 AI 把它改得更清楚、更简洁（我原来的版本还要更长，如果你想看，我可以分享）。这是因为我希望自己的句子不要有语法和句法问题，并清楚地表达我的观点：抱歉，我的母语不是英语。在有人说“AI 风格”不利于讨论之后，我后来所有的回复都是我自己写的原稿，你在下面可以看到。“你上一条评论的最后一段让我脊背发凉。”——再确认一下，你指的是“把代码和证明放在一起写这个方向”，以及“邀请社区共同制定一套共享的、标准的 SQL 形式语义”吗？是的，这对一个博士生来说太大了。但这就是我想做、而且现在正在做的事：我已经把翻译器 SQLSpec 开源出来，供大家检查和修正。欢迎在仓库里提 issue 和 PR：我会非常感激。顺便说一句，我想反驳“一个计算机科学博士生不会写出这种东西”这个说法。这已经是我上个月在 HPTS 2026 的演讲和交谈中与他人分享和讨论过的内容。我不只是“写”出来，我还直接在公开场合“说、分享、讨论”它。删除 回复 回复
你好，正如我在给另一位匿名人士的另一条回复中已经澄清的那样：所有评论都出自我本人，那一大段是我自己写的，我只是用 AI 把它改得更清楚、更简洁（我原来的版本还要更长，如果你想看，我可以分享）。这是因为我希望自己的句子不要有语法和句法问题，并清楚地表达我的观点：抱歉，我的母语不是英语。在有人说“AI 风格”不利于讨论之后，我后来所有的回复都是我自己写的原稿，你在下面可以看到。“你上一条评论的最后一段让我脊背发凉。”——再确认一下，你指的是“把代码和证明放在一起写这个方向”，以及“邀请社区共同制定一套共享的、标准的 SQL 形式语义”吗？是的，这对一个博士生来说太大了。但这就是我想做、而且现在正在做的事：我已经把翻译器 SQLSpec 开源出来，供大家检查和修正。欢迎在仓库里提 issue 和 PR：我会非常感激。顺便说一句，我想反驳“一个计算机科学博士生不会写出这种东西”这个说法。这已经是我上个月在 HPTS 2026 的演讲和交谈中与他人分享和讨论过的内容。我不只是“写”出来，我还直接在公开场合“说、分享、讨论”它。
- Anonymous 2026年11月11日 晚上7:14 Jiale 的评论都是清晰可读的，看起来是用自然语言写的。最后一段并没有什么异常之处。相比之下，你反复念叨“very bad”，并没有很好地展开你的观点，你似乎只是在做人身攻击。删除 回复 回复
Jiale 的评论都是清晰可读的，看起来是用自然语言写的。最后一段并没有什么异常之处。相比之下，你反复念叨“very bad”，并没有很好地展开你的观点，你似乎只是在做人身攻击。
- Anonymous 2026年11月11日 晚上7:17 Jiale，你在论文里犯了错，然后又用 AI 在这里留言，再次犯错。我建议你深吸一口气，先离开一会儿，别再试图为自己的错误辩护。这是个混乱的时期，我们都在从尝试和失败中学习。如果你想学习，就承认自己的错误，并开始更多地对自己的代码负起责任。短期内，你应该认真考虑撤稿，或者至少删掉那些有误导性的性能数字。 删除 回复 回复
- Thomas NeumannNovember 11, 2026 at 7:19 PMJiale，你在论文中犯了错误，然后又用 AI 在这里留言，再次犯错。我建议你深呼吸，退一步，不要再试图为自己的错误辩护。现在是令人困惑的时期，我们都在从尝试和失败中学习。如果你想学习，就承认自己的错误，并开始对自己的代码承担更多责任。短期内，你应该认真考虑撤稿，或者至少删除那些误导性的性能数字。删除回复回复
Jiale，你在论文中犯了错误，然后又用 AI 在这里留言，再次犯错。我建议你深呼吸，退一步，不要再试图为自己的错误辩护。现在是令人困惑的时期，我们都在从尝试和失败中学习。如果你想学习，就承认自己的错误，并开始对自己的代码承担更多责任。短期内，你应该认真考虑撤稿，或者至少删除那些误导性的性能数字。删除回复回复
- Jiale LaoNovember 11, 2026 at 7:53 PM非常感谢你的善意之言！我在论文中提出了不恰当的性能声明，我会为此更新代码和论文。我接受这些，并会用它们让我自己和我的工作变得更好。这是我对研究的信念：发表并开源，获得反馈，反复修订和改进。最终目标是让世界变得更好，尽管在通往这一目标的道路上，会有许多讨论、争论、纠正、修订，甚至攻击。我想强调，我的一个本性是，我非常非常欢迎健康、开放、文明、善意的讨论，并非常乐意基于这些讨论修订我的工作。我知道，没有工作是完美无缺的，这就是为什么我们接受反馈，从中学习，并变得更好。所以我仍然欢迎更多反馈和善意讨论：让我们聚焦数据库话题 🙂删除回复回复
非常感谢你的善意之言！我在论文中提出了不恰当的性能声明，我会为此更新代码和论文。我接受这些，并会用它们让我自己和我的工作变得更好。这是我对研究的信念：发表并开源，获得反馈，反复修订和改进。最终目标是让世界变得更好，尽管在通往这一目标的道路上，会有许多讨论、争论、纠正、修订，甚至攻击。我想强调，我的一个本性是，我非常非常欢迎健康、开放、文明、善意的讨论，并非常乐意基于这些讨论修订我的工作。我知道，没有工作是完美无缺的，这就是为什么我们接受反馈，从中学习，并变得更好。所以我仍然欢迎更多反馈和善意讨论：让我们聚焦数据库话题 🙂删除回复回复
- AnonymousNovember 11, 2026 at 8:08 PMJiale，问题从来不是你是否愿意接受反馈。问题在于你论文中的声明是否有可靠的评估支持。开源你的工作并不会把验证其声明的责任外包给社区。删除回复回复
Jiale，问题从来不是你是否愿意接受反馈。问题在于你论文中的声明是否有可靠的评估支持。开源你的工作并不会把验证其声明的责任外包给社区。删除回复回复
- Jiale LaoNovember 11, 2026 at 8:14 PM这是真的。但现在我有机会根据反馈修订和更新论文与代码，我会这样做。删除回复回复
这是真的。但现在我有机会根据反馈修订和更新论文与代码，我会这样做。删除回复回复
- AnonymousNovember 10, 2026 at 4:48 PM我不认为「correct SQLSpec」能解决 Thomas 指出的硬编码 dbgen 逻辑问题。说到底，你验证的是一个数据库「正确」，而这与性能毫无关系。在生产环境中，性能是正确性的一部分——如果客户数据的分布漂移导致某个关键查询慢了若干个数量级（就像那个例子会导致的那样），那就是一个 bug，就是一次故障。我觉得这项工作最过分的一点是，它试图把形式化验证描绘成某个任意系统旁边的一个绿色对勾，却无视了这样一个事实：它证明的是一个狭窄得多的数学性质，而这个性质对精确的形式化定义和假设高度敏感，处处是坑。P.S. 我通常倾向于假定研究者抱有最好的意图，但我觉得你的回复听起来很像 AI。 回复删除回复
- Jiale LaoNovember 10, 2026 at 6:35 PM你好，无论在论文里还是在我之前的回复里，我都从未声称形式化验证能够保证性能。形式化验证唯一能保证的是：代码返回的结果是 SQLSpec 所规定的输出所允许的，仅此而已。至于性能，我们只能依靠 benchmark 反馈来指导优化，并且把它作为最终指标，而不是形式化验证。接下来就是 benchmark 评估的问题：agent 或系统会过拟合 benchmark，尽管在某些情况下，对于热点模板的定制代码，我们恰恰想要这种特化。P.S. 我向你保证，我之前评论里的所有意图都出自我本人。我确实用了 AI 来重写我的草稿，prompt 是「make it simple, clear, and concise」，用的是 Fable 5.2，仅此而已。如果我们不喜欢这种「AI 风格」，从现在起我会用我自己的原始草稿。或者如果你想要更多，我们可以开个会多聊聊。删除回复回复
- AnonymousNovember 10, 2026 at 6:41 PM你甚至没搞懂上一位为什么说「性能」应该是「正确性」的一部分。 删除回复回复
- Jiale LaoNovember 10, 2026 at 6:50 PM所有针对热路径的优化都会在运行时被检查：(1) 如果数据发生变化、假设不再成立，特化代码就永远不会被执行。(2) 如果兜底系统是一个强大的通用引擎，比如 Umbra 或 DuckDB，这个查询就不会慢上几个数量级。删除回复回复
- AnonymousNovember 10, 2026 at 7:09 PM结合你所有的澄清，为什么合成一个独立的数据库引擎从一开始就是正确的抽象？如果目标是热点查询特化，现有引擎已经提供了感知工作负载的物理设计、物化、查询编译以及其他优化技术。编码 agent 也能帮助工程师在这些引擎内部实现并测试新的优化。GenDB-V 到底提供了什么具体能力，是增强现有引擎无法更经济地实现的？又有哪些证据证明了这一优势？删除回复回复
- AnonymousNovember 10, 2026 at 7:38 PM「所有针对热路径的优化都会在运行时被检查：(1) 如果数据发生变化、假设不再成立，特化代码就永远不会被执行。(2) 如果兜底系统是一个强大的通用引擎，比如 Umbra 或 DuckDB，这个查询就不会慢上几个数量级。」------好吧，我想重点在于：如果你的 agent 过拟合得太厉害，那么你的方案就会对 benchmark 的特定特征非常敏感。这意味着，如果工作负载发生了漂移，哪怕只是一点点，你的方案就无法通过检查器，只能走兜底。当然你可以用一个更快的后端引擎，但如果你的 agent 在 99.9% 的情况下都在走兜底（当然是指在更真实的、发生漂移的工作负载下，而不是固定的工作负载），你的贡献在哪里？我觉得之前几轮讨论的一个主要观点是，你的评估不够系统和合理，人们怀疑你
u 过度宣称。删除 回复 回复 匿名 2026 年 11 月 10 日 下午 7:48「这意味着，如果工作负载发生了漂移，哪怕只是一点点，你的方案也会通不过检查器，你只能回退。」------好吧，他总是可以再加一个「智能」agent 来处理工作负载漂移。删除 回复 回复 Jiale Lao 2026 年 11 月 10 日 下午 7:56 关于由编码 agent 进行热查询特化，这并不是 GenDB-V 提出的新主张（而是来自此前的 GenDB、Bespoke OLAP 和 JetStream），因此我就不再就此多谈了。我喜欢 Bespoke OLAP 论文中的讨论：与调优现有系统相比，直接实现特化代码有一些优势。至于合成一个独立数据库引擎这一抽象，作为研究项目，这本身不就是一个有趣且令人兴奋的探索方向吗？我要说，GenDB-V 的一个重要「经济收益」是形式化验证。据我所知，没有任何生产级 SQL 引擎经过形式化验证（如果我错了请纠正我）。对某个东西做形式化验证过去是如此困难和昂贵：seL4 那 8,700 行的 C 内核花了大约 20 人年！而现在，拥有一个经过形式化验证的独立数据库引擎成为可能，而且我们以便宜得多的方式实现了它，这不令人兴奋吗？顺便说一句，给一些背景，以防有些人不熟悉形式化验证：形式化验证并不意味着「没有 bug」，只是代码针对形式化规约做了验证，在 GenDB-V 中这个规约就是 SQLSpec。我并不声称这个规约是正确的。所以我将其开源，希望社区能一起修复和完善它。删除 回复 回复 Jiale Lao 2026 年 11 月 10 日 下午 8:17「我觉得之前讨论的一个主要点是，你的评估不够系统和合理，而且人们怀疑你过度宣称。」------我完全同意我在性能上过度宣称了。诚实的性能主张应该是：在特定目标上，合成引擎能够胜过未经调优的通用引擎。我会更新这些主张。我也会用更严格的设置和评估来跑新实验。乐意接受任何建议。例如，微软那个生成倾斜 TPC-H 数据的工具，而这在合成过程中对 agent 完全不可见？顺便说一句，我始终欢迎反馈、讨论和建议，并且总会据此改进。只是希望讨论是开放、健康、友好、不带情绪的 🙂删除 回复 回复 回复
文章标题：Next-Level Benchmarking Overfitting
正文： 我不认为“正确的 SQLSpec”能解决 Thomas 指出的硬编码 dbgen 逻辑问题。归根结底，你验证的是数据库“正确”，这与性能无关。在生产环境中，性能是正确性的一部分——如果客户数据的分布漂移导致某个关键查询慢了数个数量级（就像这个示例所展示的那样），那就是 bug，就是故障。我认为这项工作最过分的一点，是试图把形式验证描绘成任意系统旁边的绿色对勾，而无视它证明的是一个范围窄得多的数学性质，该性质对精确的形式定义和假设高度敏感，且暗坑众多。附注：我通常倾向于假定研究人员出于善意，但我发现你的回复听起来很像 AI。
- Jiale Lao2026年11月10日 下午6:35你好，无论是在论文中还是在我之前的回复中，我都从未声称形式验证能够保证性能。形式验证唯一能保证的是，代码返回的结果是 SQLSpec 所规定的结果所允许的，仅此而已。至于性能，我们只能依靠基准反馈来指导优化，并将其作为最终指标，而不是形式验证。然后就是基准评估的问题：agent 或系统会过拟合基准，尽管在某些情况下，对于热模板的定制代码，我们确实想要这种特化。附注：我向你保证，我之前评论中的所有意图都出自我本人。我确实用了 AI 来重写我的草稿，提示词是“make it simple, clear, and concise”，用的是 Fable 5.2，仅此而已。如果我们不喜欢这种“AI 风格”，从现在起我会使用我的原始草稿。或者如果你想要更多，可以和我开个会深入讨论删除回复回复
你好，无论是在论文中还是在我之前的回复中，我都从未声称形式验证能够保证性能。形式验证唯一能保证的是，代码返回的结果是 SQLSpec 所规定的结果所允许的，仅此而已。至于性能，我们只能依靠基准反馈来指导优化，并将其作为最终指标，而不是形式验证。然后就是基准评估的问题：agent 或系统会过拟合基准，尽管在某些情况下，对于热模板的定制代码，我们确实想要这种特化。附注：我向你保证，我之前评论中的所有意图都出自我本人。我确实用了 AI 来重写我的草稿，提示词是“make it simple, clear, and concise”，用的是 Fable 5.2，仅此而已。如果我们不喜欢这种“AI 风格”，从现在起我会使用我的原始草稿。或者如果你想要更多，可以和我开个会深入讨论
- Anonymous2026年11月10日 下午6:41你甚至都没理解上一位为什么说“性能”应当成为“正确性”的一部分。删除回复回复
你甚至都没理解上一位为什么说“性能”应当成为“正确性”的一部分。
- Jiale Lao2026年11月10日 下午6:50所有针对热路径的优化都会在运行时被检查：(1) 如果数据发生变化、假设不再成立，特化代码将永远不会被执行。(2) 如果回退系统是一个强大的通用引擎，例如 Umbra 或 DuckDB，这个查询就不会慢上数个数量级。删除回复回复
所有针对热路径的优化都会在运行时被检查：(1) 如果数据发生变化、假设不再成立，特化代码将永远不会被执行。(2) 如果回退系统是一个强大的通用引擎，例如 Umbra 或 DuckDB，这个查询就不会慢上数个数量级。
文章标题：Next-Level Benchmarking Overfitting
正文：
- AnonymousNovember 10, 2026 at 7:09 PM鉴于你所有的澄清，为什么合成一个独立的数据库引擎首先就是正确的抽象？如果目标是热查询特化，现有引擎已经提供了工作负载感知的物理设计、物化、查询编译以及其他优化技术。编码代理也可以帮助工程师在这些引擎内实现和测试新的优化。GenDB-V 提供了什么具体能力，是现有引擎无法通过增强更经济地实现的？又有哪些证据证明了这一优势？DeleteRepliesReply
鉴于你所有的澄清，为什么合成一个独立的数据库引擎首先就是正确的抽象？如果目标是热查询特化，现有引擎已经提供了工作负载感知的物理设计、物化、查询编译以及其他优化技术。编码代理也可以帮助工程师在这些引擎内实现和测试新的优化。GenDB-V 提供了什么具体能力，是现有引擎无法通过增强更经济地实现的？又有哪些证据证明了这一优势？
- AnonymousNovember 10, 2026 at 7:38 PM“所有针对热路径的优化都在运行时检查：(1) 如果数据发生变化且假设不再成立，特化代码将永远不会被执行。(2) 如果回退系统是一个强大的通用引擎，例如 Umbra 或 DuckDB，这个查询不会慢上几个数量级。”------好吧，我想重点是。如果你的代理过拟合太严重，那么解决方案将对特定基准特征非常敏感。这意味着，如果工作负载发生了漂移，哪怕只是一点点，你的解决方案就会无法通过检查器，你只能回退。当然你可以使用更快的后端引擎，但如果你的代理在 99.9% 的情况下都在回退（当然是在更现实的、漂移的工作负载中，而不是固定的工作负载），你的贡献在哪里？我觉得之前讨论的一个主要点是，你没有足够系统和合理的评估，人们怀疑你在过度声称。 DeleteRepliesReply
“所有针对热路径的优化都在运行时检查：(1) 如果数据发生变化且假设不再成立，特化代码将永远不会被执行。(2) 如果回退系统是一个强大的通用引擎，例如 Umbra 或 DuckDB，这个查询不会慢上几个数量级。”------好吧，我想重点是。如果你的代理过拟合太严重，那么解决方案将对特定基准特征非常敏感。这意味着，如果工作负载发生了漂移，哪怕只是一点点，你的解决方案就会无法通过检查器，你只能回退。当然你可以使用更快的后端引擎，但如果你的代理在 99.9% 的情况下都在回退（当然是在更现实的、漂移的工作负载中，而不是固定的工作负载），你的贡献在哪里？我觉得之前讨论的一个主要点是，你没有足够系统和合理的评估，人们怀疑你在过度声称。
- AnonymousNovember 10, 2026 at 7:48 PM“这意味着，如果工作负载发生了漂移，哪怕只是一点点，你的解决方案就会无法通过检查器，你只能回退。”------好吧，他随时可以再加一个“聪明”的代理来处理工作负载漂移。DeleteRepliesReply
“这意味着，如果工作负载发生了漂移，哪怕只是一点点，你的解决方案就会无法通过检查器，你只能回退。”------好吧，他随时可以再加一个“聪明”的代理来处理工作负载漂移。
Next-Level Benchmarking Overfitting
- Jiale Lao 2026年11月10日 下午7:56 关于 coding agent 进行热查询特化，这并非 GenDB-V 提出的新主张（而是来自之前的 GenDB、Bespoke OLAP 和 JetStream），因此我不再对此展开讨论。我很喜欢 Bespoke OLAP 论文中的讨论：相比调优现有系统，直接实现特化代码有一些优势。至于合成一个独立数据库引擎这一抽象，这本身难道不是一个有趣且令人兴奋的探索方向吗，作为一个研究项目？我认为 GenDB-V 一个重要的「经济收益」是形式化验证。据我所知，没有任何生产级 SQL 引擎经过形式化验证（如果我错了请纠正我）。形式化验证某样东西曾经如此困难和昂贵：seL4 那 8,700 行的 C 内核花了大约 20 人年！而现在，拥有一个经过形式化验证的独立数据库引擎成为可能，而且我们以便宜得多的方式实现了这一点，这难道不令人兴奋吗？顺便说一下，只是提供一些背景，以防有些人不熟悉形式化验证：形式化验证并不意味着「没有 bug」，只是代码针对形式化规约进行了验证，在 GenDB-V 中这个规约就是 SQLSpec。我并不声称这个规约是正确的。所以我将其开源，希望社区能一起修复和完善它。 删除回复回复
关于 coding agent 进行热查询特化，这并非 GenDB-V 提出的新主张（而是来自之前的 GenDB、Bespoke OLAP 和 JetStream），因此我不再对此展开讨论。我很喜欢 Bespoke OLAP 论文中的讨论：相比调优现有系统，直接实现特化代码有一些优势。至于合成一个独立数据库引擎这一抽象，这本身难道不是一个有趣且令人兴奋的探索方向吗，作为一个研究项目？我认为 GenDB-V 一个重要的「经济收益」是形式化验证。据我所知，没有任何生产级 SQL 引擎经过形式化验证（如果我错了请纠正我）。形式化验证某样东西曾经如此困难和昂贵：seL4 那 8,700 行的 C 内核花了大约 20 人年！而现在，拥有一个经过形式化验证的独立数据库引擎成为可能，而且我们以便宜得多的方式实现了这一点，这难道不令人兴奋吗？顺便说一下，只是提供一些背景，以防有些人不熟悉形式化验证：形式化验证并不意味着「没有 bug」，只是代码针对形式化规约进行了验证，在 GenDB-V 中这个规约就是 SQLSpec。我并不声称这个规约是正确的。所以我将其开源，希望社区能一起修复和完善它。
- Jiale Lao 2026年11月10日 下午8:17 「我觉得之前讨论的一个主要点是，你的评估不够系统和合理，人们怀疑你过度宣称。」——我完全同意我在性能上过度宣称了。诚实的性能主张应该是：在特定的目标上，合成的引擎可以胜过未经调优的通用引擎。我会更新这些主张。而且我会运行新的实验，采用更严格的设置和评估。乐意接受任何建议。比如，微软那个生成倾斜 TPC-H 数据的工具，并且在合成过程中对 agent 完全不可见？顺便说一下，我一直欢迎反馈、讨论和建议，并会始终据此改进。只是希望，讨论是开放、健康、友好、而非情绪化的 🙂 删除回复回复
文章标题：Next-Level Benchmarking Overfitting
正文： “我觉得之前讨论的一个主要点是，你们没有足够系统和合理的评估，而且人们怀疑你们在过度宣称。”——我完全同意我在性能上过度宣称了。诚实的性能声明应该是：合成后的引擎可以在特定目标上胜过未经调优的通用引擎。我会更新这些声明。而且我会用更严格的设置和评估来运行新实验。乐意接受任何建议。例如，微软用于生成偏斜 TPC-H 数据的工具，这在合成期间对 agent 完全不可见？顺便说一句，我一直欢迎反馈、讨论和建议，并且会始终据此改进。只是希望，讨论是开放、健康、友好、不动情绪的 🙂
- Tobias Muehlbauer2026年11月11日 下午2:02此评论已被作者删除。回复删除回复回复
此评论已被作者删除。
- Tobias Muehlbauer2026年11月11日 下午2:16别误会，以模型检查、SMT、TLA 形式进行的形式化验证都很有意思，而且 LLM 让定义规格和运行证明变得更容易。但话又说回来，没有任何形式化验证能在现实世界中给你一个无 bug 的系统。它只是我们应当利用的又一个来源，就像 sanitizers、代码审查、编译器警告、单元测试、集成测试、生产日志一样。对于特定类别的东西——规格小且稳定，并且可以证明有理由投入大量资源来获得可信规格，比如 peephole 规则、原子性/同步协议、线路协议——它当然很棒。但即使在有限范围内，它也不是万无一失的，盲点依然存在：规格本身、翻译器、工具，以及从大局来看，操作系统、硬件、网络、存储……回复删除回复Jiale Lao2026年11月11日 下午7:25嗨 Tobias，非常感谢你冷静而开放地和我讨论这件事。我完全同意，形式化验证并不意味着无 bug：规格可能不正确、不完整，而且还有许多被信任的东西。我喜欢 Ion 在 HPTS 2026 主题演讲中的观点：规格问题实际上是一个社会问题，我们需要每个领域都有社区达成一致的规格，甚至可以设立“CS 规格律师”来审视、修复和修订规格。“规格小且稳定之处”——实际上这非常有趣，我们可以进一步讨论。我看到越来越多的研究论文、工业报告和初创公司正在致力于扩展这一点。一个令人印象深刻的结果，就在昨天发布，是 Google Deepmind 对复杂软件进行了深度形式化验证：https://deepmind.google/blog/introducing-alphaproof-code/。他们使用 Gemini Carbon 完成证明，生成了超过六百万行 Lean，以验证 Signal 加密协议的代码。在他们的代码仓库中，他们开源了“arm64-semantics/”。这与以下观点相符：规格应该是一个社会问题，社区应该共同努力，使其尽可能被更多人认同。删除回复回复回复
别误会，以模型检查、SMT、TLA 形式进行的形式化验证都很有意思，而且 LLM 让定义规格和运行证明变得更容易。但话又说回来，没有任何形式化验证能在现实世界中给你一个无 bug 的系统。它只是我们应当利用的又一个来源，就像 sanitizers、代码审查、编译器警告、单元测试、集成测试、生产日志一样。对于特定类别的东西——规格小且稳定，并且可以证明有理由投入大量资源来获得可信规格，比如 peephole 规则、原子性/同步协议、线路协议——它当然很棒。但即使在有限范围内，它也不是万无一失的，盲点依然存在：规格本身、翻译器、工具，以及从大局来看，操作系统、硬件、网络、存储……
Next-Level Benchmarking Overfitting
- Jiale LaoNovember 11, 2026 at 7:25 PM嗨 Tobias，非常感谢你如此冷静而坦诚地与我讨论这件事。我完全同意，形式化验证并不意味着没有 bug：规范可能是不正确、不完整的，而且还有许多需要信任的东西。我很喜欢 Ion 在 HPTS 2026 主题演讲中的观点：规范问题实际上是一个社会问题，我们需要为每个领域制定社区公认的规范，我们甚至可以设立“CS Spec Lawyers”来审视、修复和修订这些规范。“where the spec is small and stable”------其实这非常有意思，我们可以再深入讨论。我看到越来越多的研究论文、行业报告和初创公司都在致力于扩展这一方向。一个令人印象深刻的结果昨天刚刚发布：Google Deepmind 对复杂软件进行了深度的形式化验证：https://deepmind.google/blog/introducing-alphaproof-code/。他们使用 Gemini Carbon 完成证明，生成了超过六百万行 Lean，用于验证 Signal 加密协议的代码。在他们的代码仓库中，他们开源了“arm64-semantics/”。这与以下观点相符：规范应该是一个社会问题，社区应该共同努力，使其得到尽可能多的人认可。DeleteRepliesReply
嗨 Tobias，非常感谢你如此冷静而坦诚地与我讨论这件事。我完全同意，形式化验证并不意味着没有 bug：规范可能是不正确、不完整的，而且还有许多需要信任的东西。我很喜欢 Ion 在 HPTS 2026 主题演讲中的观点：规范问题实际上是一个社会问题，我们需要为每个领域制定社区公认的规范，我们甚至可以设立“CS Spec Lawyers”来审视、修复和修订这些规范。“where the spec is small and stable”------其实这非常有意思，我们可以再深入讨论。我看到越来越多的研究论文、行业报告和初创公司都在致力于扩展这一方向。一个令人印象深刻的结果昨天刚刚发布：Google Deepmind 对复杂软件进行了深度的形式化验证：https://deepmind.google/blog/introducing-alphaproof-code/。他们使用 Gemini Carbon 完成证明，生成了超过六百万行 Lean，用于验证 Signal 加密协议的代码。在他们的代码仓库中，他们开源了“arm64-semantics/”。这与以下观点相符：规范应该是一个社会问题，社区应该共同努力，使其得到尽可能多的人认可。
- AnonymousNovember 11, 2026 at 2:18 PM我认为“系统的形式化验证”所引出的更广泛的问题是：你如何形式化验证一个系统的非功能性需求？功能性需求我们现在大概知道该怎么做了，持久性也许可以通过 effect systems（？）来做，但性能是目前为止最难的，我还没有看到任何令人信服的方法。ReplyDeleteRepliesReply
我认为“系统的形式化验证”所引出的更广泛的问题是：你如何形式化验证一个系统的非功能性需求？功能性需求我们现在大概知道该怎么做了，持久性也许可以通过 effect systems（？）来做，但性能是目前为止最难的，我还没有看到任何令人信服的方法。