Z Highlights

• 人工智能虽然其提供了广泛的信息，却缺乏解决复杂问题所需的深入、结构化的推理能力，同时还存幻觉的局限。形式逻辑和相关数学工具为 AGI 的逻辑推理能力提供了必要的理论基础和技术支撑。

• Harmonic AI 正在开发数学超级智能，它的第一个模型 Aristotle（亚里士多德）不仅能理解和解决自然语言描述的国际奥赛数学问题，还能提供严格的数学证明。

• Harmonic 的领导者是 86年生的英年才俊 Vlad Tenev。他以创办免佣金的互联网券商应用 Robinhood 闻名，Robinhood 21 年上市时市值达到 320 亿美元。Vlad 有很强的数学背景，本科毕业于 Stanford，还曾攻读 UCLA 的数学博士学位。

01 数学推理是人工智能下一个重大飞跃

强人工智能的一个核心挑战是强数学基础。

在通用人工智能（AGI）的研究领域中，数学推理能力被视为一项核心技能，远远超出了简单的计算范畴。数学推理能力不仅是人类智慧的根基，也是我们解决复杂问题、推动创新和理解世界的关键工具。

对于 AGI 系统而言，具备数学推理能力意味着它不仅仅是一个高效的计算工具，更代表了一种能够进行抽象思考、概念化和创造性思维的高级智能形式。这种能力的实现将标志着 AI 向真正的智能体迈进了一大步。

Harmonic 的创立正是为了应对当前 AI 在数学推理和解决复杂数学问题上的不足。数学是所有科学发现的基础，通过将数学作为模型的基本组成部分，Harmonic 希望创建一个能够精确定义和对齐共同真理的工具，从而加速科学和工程领域的进步。通过专注于数学能力，AI 系统可以在其他领域展示出卓越的推理能力。

02 第一个模型已接近国际数学奥赛选手

Harmonic 的第一个模型是 Aristotle（亚里士多德）。

Aristotle 能将自然语言描述的数学问题，转换为一种专门证明数学命题的计算机编程语言 Lean 进行验证。这意味着 Aristotle 的解决方案是经过严格数学证明的，而不仅仅是给出一个答案。

下图来源于 2001 年国际数学奥林匹克竞赛（IMO）的第 6 题，这是一个相当高级的数学问题，需要运用数论和代数的知识来解决。Aristotle 使用反证法得出矛盾从而证明原命题成立，并且使用了 Lean 的语法和 tactics 来严格地表达每一个推理步骤。

（图源：Harmonic AI ）

Harmonic 表示，Aristotle 生成的 Lean 代码并不总是完美的。但通过不断尝试，它可以学会验证一个解决方案，就像一个人反复尝试解决问题一样。

基准测试方面，Aristotle 在领先的形式化数学基准 MiniF2F 上获得了 90%的得分，展示了该模型具有高精度解决复杂数学问题的能力。与 Aristotle 一同比较的还有国内幻方公司的 Deepseek-Prover，在 MiniF2F 得到了 60%的成绩。

（图源：Harmonic AI）

03 彻底改变软件工程领域，代码验证更加高效、可靠。

据公司描述，Harmonic 的应用场景集中在高精度和可靠性的软件领域。

如航空航天中用于设计和验证复杂系统，以确保在极端条件下的安全性和有效性；在计算机芯片设计中优化流程，提高效率并减少错误；在工业系统中，通过高可靠性算法优化自动化和控制系统，确保生产稳定性和安全性；在医疗技术中，提升数据分析和诊断精度，开发更准确的诊断工具和治疗方案，辅助医生决策。此外，公司还提到 Harmonic 的技术还可以推动 AI 研究本身的发展，通过创建更强大的系统，这些系统能够生成自己的合成数据以增强知识和学习能力。

04 金融业的百亿大鳄，追梦数学理想

（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）领投。

References:

https://github.com/harmonic-ai/datasets

https://harmonic.fun/news#blog-post-1-link

https://www.nytimes.com/2024/09/23/technology/ai-chatbots-chatgpt-math.html?smid=url-share

https://www.sequoiacap.com/podcast/training-data-harmonic/

https://www.indexventures.com/perspectives/solving-the-ai-reasoning-gap-how-harmonic-is-building-mathematical-superintelligence/

文章来自微信公众号 “Z Potentials”，作者“Z Potentials”