点击“第二步”即表示您知悉并同意本网站将在您的设备上运行开源内核漏洞利用程序。若运行成功，该程序可能会执行以下操作：在 Firefox 的私有数据存储中创建临时文件；向 /bin/su 和 /data/local/tmp/su 写入文件；修改您的设备壁纸；进行可能影响设备稳定性的系统级更改。 此内核漏洞利用程序处于实验阶段，可能不稳定。它可能导致意外行为、系统崩溃、数据损坏或永久性数据丢失。在继续之前，您应该：备份所有重要数据；明确此操作可能会对您的设备进行系统级修改；仅在您拥有或已获得明确测试许可的设备上进行操作；并对可能发生的任何损坏、不稳定或数据丢失承担全部责任。除非您完全理解相关风险，否则请勿继续。 我已了解相关风险，并同意在此设备上运行该漏洞利用程序。
每日HackerNews RSS
Leanstral 1.5 是一个用于 Lean 4 证明工程的全新开源（Apache-2.0）模型。它拥有 119B 总参数（6B 激活参数），在形式化验证领域展现出顶尖性能，且成本仅为同类竞争模型的一小部分。
该模型在各项主要基准测试中表现卓越：在 miniF2F 上达到满分（100%），在 FATE-H/X 上创下新纪录，并解决了 PutnamBench 中的 587/672 道难题。值得注意的是，它实现了极高的成本效益——平均每道题仅需约 4 美元，远低于其他方案数百美元的成本。Leanstral 1.5 展现了强大的测试时扩展能力，在高达 400 万个 token 的推理预算下仍能保持稳定的推理性能。
除数学领域外，Leanstral 1.5 还能验证复杂的代码属性并发现现实世界的漏洞。它成功验证了 AVL 树的 O(log n) 复杂度，并在开源 Rust 代码库中发现了 11 个真实存在的漏洞，其中包括此前未被报告的边界情况。
Leanstral 1.5 经过严谨的三阶段训练过程（包括多轮证明环境和代码代理工作流），现已通过 Hugging Face 和免费 API 接口开放使用。它针对“Mistral Vibe”进行了优化，使开发人员能够将形式化验证无缝集成到现有的代码库和工作流程中。
这篇 Hacker News 的讨论围绕 **Leanstral 1.5** 的发布展开，这是一个专为形式化验证和定理证明而设计的模型。
讨论的主要议题包括：
* **效率与前沿模型的对比：** 许多用户称赞 Mistral 专注于开发高质量、高效率的专业模型。尽管它们可能无法与庞大的“前沿”模型竞争，但由于具有高性价比、可本地运行以及性能可预测等优势，它们在 OCR 或代码验证等特定任务中极具价值。
* **形式化验证的实用性：** 用户探讨了 Lean（一种函数式编程语言及定理证明器）在增强软件可靠性方面的潜力。虽然一些批评者认为发布中列举的错误检测示例过于基础，但支持者指出，其核心价值在于确保形式化正确性，而不仅仅是发现简单的漏洞。
* **市场策略：** 讨论中围绕 Mistral 的利基市场方法究竟是可持续的商业模式，还是陷入了“商品化陷阱”展开了热烈辩论。
* **社区反馈：** 讨论还涉及了自我推广的伦理问题，用户就如何在不引发“垃圾信息”担忧的情况下有效地分享开发工具提供了建议。
请启用 JavaScript 和 Cookie 以继续。
抱歉。
十七世纪时，阿姆斯特丹巨大的财富和工业增长，使得城市面临严重的火灾风险。起初，该市使用抽水机进行灭火，但随着一家大型制糖厂和一家世界知名的印刷厂被彻底烧毁，事实证明这些设备并不足以应对灾情。
多才多艺的画家兼发明家扬·范·德·海登（Jan van der Heyden）改变了这一局面。他运用“系统分析”的方法，开创了更先进的消防技术，包括柔性皮革吸水软管，以及用于保持连续高压水流的空气室。
除了硬件之外，范·德·海登还全面改革了城市的应急基础设施。他建立了一个协调一致的响应网络，包括警报系统、各区消防队，以及针对快速响应的经济奖励机制。到1682年，这种将技术创新与城市管理相结合的综合策略，大幅降低了火灾造成的损失。范·德·海登的改革使阿姆斯特丹从一个易受灾难侵袭的城市，转变为欧洲最具防火韧性且组织最为严密的城市之一，为系统化的城市危机管理树立了早期标杆。
对不起。
弥散损失抵消了小型语言模型中的嵌入凝聚现象 Dispersion loss counteracts embedding condensation in small language models
14 天前
本文提出了“嵌入坍缩”（embedding condensation）这一概念，即较小语言模型中的词嵌入会坍缩至一个狭窄的锥形子空间，从而限制了其表达能力。观察结果证实，这种现象在小模型中比在大模型中更为显著，存在于各种数据集，且源于模型初始化阶段。关键在于，作者证明了利用大模型进行知识蒸馏无法缓解这一坍缩问题。
为解决该问题，作者引入了“离散损失”（dispersion loss）。该训练目标旨在通过鼓励嵌入在单位超球面上分布开来，从而抵消坍缩。通过促进均匀的角离散，该技术使小模型能够获得更接近大模型的高质量潜在表征。实验结果表明，在训练中加入离散损失可有效缓解嵌入坍缩，为在不增加参数规模的前提下缩小小型与大型语言模型之间的性能差距提供了有效路径。作者总结认为，模型的优异性能不仅源于其规模，还源于其潜在信息的结构化组织方式。
抱歉。
Steam Controller Auto-Charge 是一款开源 Web 应用程序，可自动将 Steam 控制器导航至其磁吸充电底座上。该系统利用头顶摄像头，结合用于 Lucas-Kanade 光流跟踪的 OpenCV.js 以及基于浏览器内 Rust/WASM 的 CNN（卷积神经网络）进行目标检测。 该应用通过 WebHID API 与控制器通信，利用其内部的线性谐振执行器（LRA）产生 70Hz 的触觉脉冲，从而将设备“震动”至底座。为确保平稳的对接过程，系统采用了“近距离缓行”模式，当控制器处于目标 150 像素范围内时，会降低触觉强度。此外，该应用还会拦截特定的控制器报告，以实时监控电池状态和电压。 该项目使用 Vue 3 构建，具有跨平台特性，仅需 Nix 包管理器和基于 Chromium 的浏览器即可运行。它提供了一种无缝的自动化体验，并可在需要时进行手动跟踪覆盖。本项目灵感源自 Very Lazy Pixel，为家庭自动化领域中计算机视觉和硬件遥测技术的应用提供了一个复杂的实现方案。
抱歉。
参天大树能轻而易举地将水分输送到顶端的枝叶。 Giant trees have no trouble pumping water to top branches: new research
14 天前
发表在《科学》杂志上的一项新研究对一个长期存在的理论提出了挑战，即高大的热带树木由于难以将水分输送到最高枝叶，而天生更容易受到干旱的影响。
通过研究马来西亚婆罗洲的巨型龙脑香科树木（其中一些高度超过 80 米），研究人员发现这些树木已经进化出了复杂的液压适应能力。其中包括加宽靠近树干底部的输水导管，以及使叶片能够承受显著的水分压力。这些调整使树木能够完全补偿高度带来的影响，确保其内部的水分系统无论长到多高都能保持高效运行。
研究关键发现，与高度相关的生长并不会增加树木对干旱的敏感性。这反驳了现有的气候变化模型，该模型曾预测最高、碳密度最大的树木在干旱时期面临的风险最大。由于这些巨树储存了全球一半以上的地上森林碳，这一发现对于准确预测热带生态系统将如何应对气候变暖至关重要。研究人员强调，这些发现有力地支持了保护这些具有韧性且生态上至关重要的森林的必要性。
埃克塞特大学的最新研究表明，参天大树能够成功将水分输送到最高的枝头，这一发现引发了 Hacker News 用户对其中生物学机制的热烈讨论。
文章指出树木克服重力运送水分的物理挑战，而评论区则深入探讨了其确切的物理原理。一些人指出，由于大气压和潜在的空穴现象，“抽吸”作用存在局限性，并强调树木更多是依赖复杂的毛细作用和内聚力-张力理论，而非传统的机械泵送。另一些人则补充了其他机制，如叶片直接从空气中吸收雾气，以及共生苔藓在维持水分方面的作用。
讨论很快演变为跨学科的推测，许多计算机科学家表达了对植物学的新兴趣。参与者探讨了“计算植物学”，以及人工智能和基因工程在理解甚至突破植物生物学极限方面的潜力。归根结底，这篇讨论帖提醒人们，自然界中那些令人敬畏且常被误解的机制依然存在；用户在感叹历史上的环境破坏之余，也赞叹了世界上最高大树木的生命韧性。
这篇文章剥离了晦涩的术语，揭示了数字技术的根本原理，从而为现代计算的“魔法”解密。文中指出，我们流畅的设备背后是一套复杂的抽象层，每一层都凝聚了人类的智慧。
这一过程始于物理学：利用电流驱动开关（晶体管），进而组合成逻辑门。这些逻辑门实现了二进制运算、数据存储及指令执行。以此为起点，文章梳理了计算技术的发展脉络：
* **硬件**：晶体管如何演变为通过“取指-译码-执行”周期来运行指令的处理器。
* **软件**：编程语言（从汇编到 Python）如何将人类逻辑转化为机器可读的代码。
* **系统**：操作系统如何管理多任务和内存，以及网络如何实现全球互联。
文章最终认为，软件素养已不再仅仅是计算机科学家的专属，而是驾驭数字优先世界的生存技能。通过掌握这些思维模型，我们能够更安全地使用技术、高效排除故障，并利用人工智能构建工具，从而确保自己是技术的主人，而非被动的从属者。
**Nerdle** 源于伦敦交通堵塞时的一次闲聊，是由数据科学家 Richard Mann 和他的孩子们共同打造的数学版“Wordle”游戏。自迅速走红以来，它不仅吸引了从比尔·盖茨到 Stormzy 等各界名流，更成为了那些比起词汇更钟情于逻辑与算术的玩家们的必备游戏。 **游戏体验：** Nerdle 提供了一种基于逻辑推理的益智体验，既有挑战性又不失公平。凭借简洁的设计、针对移动端优化的自定义键盘，以及详尽的历史游戏存档，它堪称绝佳的每日大脑锻炼工具。尽管玩法几乎无可挑剔，但用户体验却因那则阻挡在玩家与首个猜题步骤之间的侵入式全屏隐私声明而大打折扣。 **结论：** 虽然 Nerdle 本质上是 Wordle 的模仿之作，但它凭借独特的个性和“数学友好型”魅力脱颖而出。它在适度、非侵入式的广告与统计数据、联赛及慈善支持等深层功能之间取得了平衡。在 DLE 评测框架中获得 **84/102** 分的 Nerdle，是一个精致、易上手且充满温情的项目，它证明了一个由家庭成员共同构思的简单创意，也能演变成风靡全球的数字经典。
抱歉。
2026年4月，Anthropic宣布其最新的内部模型（Claude Mythos Preview）具备了自主发现并利用网络安全漏洞的能力。此后，Anthropic和OpenAI均致力于利用前沿模型来加固关键软件，以防恶意行为者利用同类模型进行破坏。研究表明，在这些公告发布后，常见漏洞与披露（CVE）的数量显著激增。与Mythos Preview发布前的月度纪录相比，6月份高危及严重漏洞的数量增加了3.5倍以上。
Anthropic 发布 “Claude Mythos” 预览版后，严重软件漏洞激增，这在 Hacker News 上引发了激烈讨论。一些人认为漏洞披露数量（CVE）的增加是积极的结果，因为它暴露了遗留代码库中长期存在的安全缺陷；而另一些人则担心，随着研究人员和恶意行为者利用人工智能实现漏洞发现自动化，可能会进入一个“混乱”时期。
讨论的重点包括：
* **人工智能的优势：** 许多专家认为，Mythos 及类似的人工智能模型客观上提高了漏洞研究的速度和效率，迫使维护者面对大量积压的隐蔽漏洞。
* **运营挑战：** 参与 “Glasswing 项目” 的安全工程师强调，人工智能生成的报告通常需要严格验证，因为不一致的“利用”方式可能导致误报，并使开发人员感到疲惫。
* **广泛的行业影响：** 对于人工智能究竟是在识别旧漏洞，还是在通过编写代码的同时引入了质量更低的新漏洞，评论者们看法不一。
* **伦理担忧：** 关于 Anthropic 的限制性访问政策，各方存在严重分歧。一些人认为，不向开源社区提供此类工具，会使小型维护者更容易受到国家级黑客的攻击。