24小时热榜

我们都听说过裁员；那么人们在面对近期就业市场的变化时，实际的生活经历是什么样的呢？

快速概述一下，因为帖子内容较长：我在OpenAI从2017年到2020年进行机器人操作研究，当时的桌面设置成本大约是现在的10倍，并且需要一个团队来运行。这个项目是我在测试一个人是否能够在同类问题上进行有意义的工作：从物理和软件设置开始。 我有几个决策尚未确定，非常希望能得到一些反对意见或反馈： - 单臂与双臂（我选择了单臂是出于成本和空间考虑，虽然这排除了像折叠布料这样的任务） - 目前不校准相机的外部参数和内部参数 - 从零开始的策略选择RGB与RGB-D（ACT / Diffusion Policy） 还有一个我更有信心但预计会有分歧的决定：不基于ROS 2 / LeRobot，而是自己编写一个堆栈。乐意分享我的理由。

在Cajal（YC W26），我们很高兴地分享Talos（<a href="https://github.com/cajal-technologies/talos" rel="nofollow">https://github.com/cajal-technologies/talos</a>），这是一个用于在Lean中对WebAssembly模块进行形式验证的开源框架。 人工智能现在正在编写大量推向生产环境的代码。随着代码生成成本的降低，验证成为了瓶颈。我们相信未来每一款软件都应附带一份数学证明，证明其功能符合作者的意图——通过这种方式，消除许多类型的漏洞。Talos正是这一目标的基础之一。 Talos提供了一个针对二进制级推理优化的Wasm解释器，以及一个用于证明程序属性的最弱前置条件演算层。由于我们直接对WebAssembly进行推理，任何具有Wasm后端的语言都在我们的考虑范围内：Rust、C++、Go、C、Swift、Kotlin、Zig、C#等多种语言。 为了实现这一目标，我们使用Lean：一种编程语言和定理证明器，它允许您在一个系统中编写软件并数学证明其正确性。这使得Talos既可以作为可执行的解释器，又可以作为Lean进行推理的形式对象。Lean还与现代AI证明工具集成，通过证明搜索和直接评估自动完成目标。 要查看Talos的实际应用，可以查看对Stein的GCD算法的证明，该算法在流行的Rust库num-integer中实现：<a href="https://github.com/cajal-technologies/talos/blob/main/programs/lean/Project/NumInteger/Spec.lean#L562-L588" rel="nofollow">https://github.com/cajal-technologies/talos/blob/main/programs/lean/Project/NumInteger/Spec.lean#L562-L588</a>。 我们的路线图： - 首先通过官方W3C测试套件实现全面的Wasm覆盖，然后再针对SpecTec（正式的Wasm规范）进行验证。 - 任意crate验证——任何编译为Wasm的Rust crate都应在考虑范围内。 - 构建我们的证明库codelib，以使验证日益复杂的程序变得可行。 我们非常希望听到社区对Talos的反馈以及对当前形式验证状态的评论。欢迎贡献！