- 人工智能虽然其提供了广泛的信息，却缺乏解决复杂问题所需的深入、结构化的推理能力，同时还存幻觉的局限。形式逻辑和相关数学工具为 AGI 的逻辑推理能力提供了必要的理论基础和技术支撑。
- Harmonic AI 正在开发数学超级智能，它的第一个模型 Aristotle（亚里士多德）不仅能理解和解决自然语言描述的国际奥赛数学问题，还能提供严格的数学证明。
- Harmonic 的领导者是 86年生的英年才俊 Vlad Tenev。他以创办免佣金的互联网券商应用 Robinhood 闻名，Robinhood 21 年上市时市值达到 320 亿美元。Vlad 有很强的数学背景，本科毕业于 Stanford，还曾攻读 UCLA 的数学博士学位。
在通用人工智能（AGI）的研究领域中，数学推理能力被视为一项核心技能，远远超出了简单的计算范畴。数学推理能力不仅是人类智慧的根基，也是我们解决复杂问题、推动创新和理解世界的关键工具。对于 AGI 系统而言，具备数学推理能力意味着它不仅仅是一个高效的计算工具，更代表了一种能够进行抽象思考、概念化和创造性思维的高级智能形式。这种能力的实现将标志着 AI 向真正的智能体迈进了一大步。Harmonic 的创立正是为了应对当前 AI 在数学推理和解决复杂数学问题上的不足。数学是所有科学发现的基础，通过将数学作为模型的基本组成部分，Harmonic 希望创建一个能够精确定义和对齐共同真理的工具，从而加速科学和工程领域的进步。通过专注于数学能力，AI 系统可以在其他领域展示出卓越的推理能力。
Harmonic 的第一个模型是 Aristotle（亚里士多德）。Aristotle 能将自然语言描述的数学问题，转换为一种专门证明数学命题的计算机编程语言 Lean 进行验证。这意味着 Aristotle 的解决方案是经过严格数学证明的，而不仅仅是给出一个答案。下图来源于 2001 年国际数学奥林匹克竞赛（IMO）的第 6 题，这是一个相当高级的数学问题，需要运用数论和代数的知识来解决。Aristotle 使用反证法得出矛盾从而证明原命题成立，并且使用了 Lean 的语法和 tactics 来严格地表达每一个推理步骤。
（图源：Harmonic AI ）
Harmonic 表示，Aristotle 生成的 Lean 代码并不总是完美的。但通过不断尝试，它可以学会验证一个解决方案，就像一个人反复尝试解决问题一样。基准测试方面，Aristotle 在领先的形式化数学基准 MiniF2F 上获得了 90%的得分，展示了该模型具有高精度解决复杂数学问题的能力。与 Aristotle 一同比较的还有国内幻方公司的 Deepseek-Prover，在 MiniF2F 得到了 60%的成绩。03 彻底改变软件工程领域，代码验证更加高效、可靠。据公司描述，Harmonic 的应用场景集中在高精度和可靠性的软件领域。如航空航天中用于设计和验证复杂系统，以确保在极端条件下的安全性和有效性；在计算机芯片设计中优化流程，提高效率并减少错误；在工业系统中，通过高可靠性算法优化自动化和控制系统，确保生产稳定性和安全性；在医疗技术中，提升数据分析和诊断精度，开发更准确的诊断工具和治疗方案，辅助医生决策。此外，公司还提到 Harmonic 的技术还可以推动 AI 研究本身的发展，通过创建更强大的系统，这些系统能够生成自己的合成数据以增强知识和学习能力。（Harmonic AI 两位联创 Vlad Tenev，Tudor Achim）Vlad Tenev 和出生于 1987 年，是美籍保加利亚裔。在学术方面，Vlad 展现出对数学的浓厚兴趣，他先是在斯坦福大学获得了学士学位，随后前往加州大学洛杉矶分校攻读博士学位。尽管最终没有完成博士课程，但他在斯坦福结识了未来的创业伙伴，并于2013 年共同创立了 Robinhood。Robinhood 是一个互联网券商应用，通过零佣金交易和“游戏化投资”，吸引了大量年轻投资者。Robinhood 的流行称得上改变了一代美国人的投资方式。2021 年 7 月，Robinhood 以 320 亿美元的惊人估值上市。另一位联创 Tudor 在 19 岁时从 CMU 获得计算机科学学士学位。辅修数学。后来，他在斯坦福大学攻读计算机科学博士学位，主攻理论机器学习和高维推断。职业方面，Tudor 最早于 Quora 带领机器学习团队，后在自动驾驶公司 Helm.ai 担任 CTO。2024 年 9 月 23 日，Harmonic 宣布完成 7500 万美元的 A 轮融资，估值为 3.25 亿美元。该轮融资由红杉资本（Sequoia Capital）领投。
了解更多AI资讯，可以加入我们的交流群一起沟通讨论~
文章来源： Z Potentials
