最新

我觉得我们都处在一个有点黑暗的境地。你们都还好吗？感觉怎么样？我们来倾诉一下吧。你们现在在想些什么？

据我所知，这是多边形相交算法的第一个经过形式化验证的实现。 在这个项目中与 AI 代理合作的经历，随着近期模型版本的发布发生了很大变化，我在自述文件中对此进行了描述。Opus 4.8 能够一次性提供带有形式化证明的算法实现，而之前的模型则需要我分多步提供证明策略。 对正确性的信任完全来自于 Lean 验证器和对少量规范的人工审查，而不是来自于 LLM。 另外，请查看自述文件中链接的、围绕已验证核心构建的 Web 演示：https://schildep.github.io/verified-polygon-intersection/。它支持多边形，包括带孔的多边形、自相交和重叠边。

我最近尝试了 Garry Tan 的 GStack 等技能，花了一周时间，发现它存在一些缺陷（我将另发文章详述）。 我的问题是：我如何知道一个技能或提示是否好用（例如 GStack 的 `/office-hours`）？ 我该如何比较类似的技能（例如不同的“深度研究”技能）？ 发现软件缺陷（相对而言）很容易——它会崩溃、报错。而有缺陷的技能不会。那些完美无瑕、听起来自信满满的技能却会经常误导我，浪费我的时间，甚至让我觉得不如不使用 LLM。 AI 技能也是软件——它们应该附带回归测试。 LLM 团队拥有大量的提示回归测试。LLM 包装的 SaaS 公司也拥有大量的提示回归测试。但对于开源技能，SKILL.md 文件看起来很合理，却没有任何测试（例如，截至撰写本文时，GStack 的 `/office-hours` 就没有）。 Garry Tan，如果你听到我说话——请考虑为你的 `/office-hours`、`/plan-ceo-review`、`/plan-eng-review` 等技能提供回归测试。 回归测试应该： 1. 证明技能能正确工作 2. 展示正确和不正确的用法 3. 证明技能的价值 4. 附带评分标准，以便对技能进行基准测试 5. 最后一个是最有价值的，因为它允许你对相似的技能进行相互基准测试。 于是我开始自己做这件事。 这是一个正在进行中的例子：`plan-cmo-review`，一个用于补充 GStack 的技能，因为 GStack 在撰写本文时缺少营销方面的评审。我不是营销专家，分享这个技能的目的是概述其回归测试的设置。 简而言之，这是我的探索过程： * 我对几个产品使用了 GStack，并发现生成的 `design_document.md` 导致我失败，主要是营销方面。 * 我借助 Claude Opus 4.8 手动深入研究了该技能的失败之处，并最终找到了正确的解决方案。 * 我让 Claude 构建了一个 `plan-cmo-review` 技能，运行它，结果得出了一个有缺陷的解决方案（与 GStack 的输出类似）。 * 我让 Claude 分析了正确的（手动）解决方案，并将其作为带有评分标准的回归测试固定项。 * Claude 运行了（盲测）回归测试——失败了。我们进行了几次迭代，发现了关键问题：Claude 盲目信任我的提示，将其视为最终真理。Claude 认为 GStack 知道自己在做什么。GStack 认为我知道我在做什么。但我当时正在进行产品/创业研究——根据定义，“研究”就是当你不知道自己在做什么时所做的事情。这种信任链导致了技能的失败。 * 我们解决了信任问题，回归测试通过了。我们又添加了一些。它们也通过了。 * 我让 Claude 多次运行回归测试——出现了裂痕。Claude 迭代了该技能。现在它们都通过了。 * 这种方法仍然存在缺陷。我想尝试运行不同的 LLM，进行跨模型判断，以及更多的回归测试。 技能 GitHub 地址：github.com/remakeai/plan-cmo-review。笔记在 iliaov.substack.com。

我理解需要更多的资金和计算能力。但如果他们如此先进和伟大，为什么他们自己的私人投资者和股东会让这个价值数万亿美元的机会溜走呢？私人市场和家族办公室的规模也达到万亿美元级别。当然，他们可以在私人融资轮次中一直融资到字母Z，像一些公司那样，在整个过程中都保持私有？为什么要出售这家有史以来最伟大企业的股权？ 标准石油公司从未上市，在其鼎盛时期占GDP的10%以上，而真正能自我进化的AI的价值将是其数倍？而且，由于已经存在多个竞争对手，甚至不存在垄断瓦解的风险。 或者简单地说，他们不相信当前的估值能够支撑显著的未来增长。他们需要退出其头寸，尤其是在当前估值存在波动风险的情况下？