返回首页
最新
《华尔街日报》文章（“人工智能黑客正在危险地接近击败人类”）：<a href="https://www.wsj.com/tech/ai/ai-hackers-are-coming-dangerously-close-to-beating-humans-4afc3ad6" rel="nofollow">https://www.wsj.com/tech/ai/ai-hackers-are-coming-dangerously-close-to-beating-humans-4afc3ad6</a>，<a href="https://archive.ph/L4gh3" rel="nofollow">https://archive.ph/L4gh3</a>
你好，
我已经在一个小众产品的最小可行产品（MVP）上工作了一个多月，我相信它已经准备好进行Beta测试。
在发布之前，有哪些步骤可以帮助我进行一次成功的Beta发布？
以下是我在发布前的清单：
1. 网页展示产品的功能以及解决了什么问题。
2. 加入一个Beta候补名单，加入一个社区，以获得支持、视频和功能请求。
3. 在社交网站的特定社区（如Reddit、Discord）上发布消息。
4. 提供一个合理价格的终身通行证，给予用户一个增强计划。
当前问题：
我不知道如何定价。对于大多数人来说，它将分为三个计划，而特殊情况将有两个额外的计划。
一些功能有实际可测量的成本，例如机器人、短信等。我不确定如何加价。是否应该做成单点购买？
我仍然需要构建iOS和Android应用程序，但在没有真实反馈和API构建之前不会进行。
有什么想法、反馈，如何确定价格，如何进行市场营销而不让人觉得是在营销？有什么不同的准备建议？
感谢你的反馈。
你能想到哪些最具未来感的计算接口，但目前还没有广泛应用？<p>（这与吉布森的名言“未来已经到来——只是尚未均匀分布”相呼应。）
嗨，HN，我一直在探索形式方法在机器学习/可解释性方面的各种应用，希望能让更多人关注这种方法。
我正在进行一个小型的可解释性项目，称为符号电路蒸馏。其目标是从一个微小的神经元级电路（比如OpenAI的“稀疏电路”工作中的电路）自动恢复一个简洁的Python程序，该程序实现相同的算法，并提供一个有界的形式证明，证明这两者在有限的标记域上是等价的。
大致的流程如下：
1. 从一个针对特定行为（例如，引用闭合或括号深度）提取的修剪电路图开始，该电路图来自一个变换器。
2. 将电路视为可执行函数，并训练一个小型的ReLU网络（“替代网络”），使其在有界域内的所有输入上与电路完全匹配（通常是长度为5-10的序列，使用小型标记字母表）。
3. 在常见变换器模式（计数器、开关、阈值检测器、小型状态机）的受限领域特定语言（DSL）中搜索，以合成候选的Python程序。
4. 使用基于SMT的有界等价性检查，来：
- 证明候选程序和替代网络在该域的所有输入上是一致的，或者
- 生成一个反例输入，排除该程序。
如果求解器找到证明，你将获得一个小型、可读的Python函数，以及一个机器可检查的保证，证明它在该有界域上与原始电路匹配。
我为什么要构建这个项目
机械可解释性在从大型模型中提取“简洁小电路”方面已经相当成熟，但将这些图转换为干净、可读的算法仍然非常手动。我的目标是自动化最后一步：从“这是一个稀疏电路”到“这是一个经过验证的算法，解释它的功能”，而无需手动干预。
目前的工作进展
- 任务：来自OpenAI circuit_sparsity库的引用闭合和括号深度检测。
- 在有限标记域上的精确替代拟合。
- 简单计数器、开关和小型状态机的DSL模板。
- 基于SMT的有界等价性检查：
稀疏电路 -> ReLU替代网络 -> DSL中的Python程序。
局限性和待解决的问题
- 保证是有界的：等价性仅在有限标记域（短序列和小词汇表）上得到证明。
- 目前专注于非常小的电路。扩展到更大电路和更长上下文仍需工程和研究工作。
- DSL是围绕几个模式手动设计的。我尚未学习DSL本身或在搜索中做任何非常巧妙的事情。
我希望获得的反馈
- 问题框架和保证对从事机械可解释性或形式方法的人是否有趣？
- 对下一个基准的建议：你希望看到哪些电路或行为被蒸馏？
- 对DSL设计、搜索策略和SMT设置的反馈。
欢迎对实施细节、SMT编码、与OpenAI的稀疏电路库的集成或其他任何问题进行提问。