Robinhood创始人再创业研发超级数学AI,已接近国际数学奥赛选手,红杉领投近亿美金

AITNT-国内领先的一站式人工智能新闻资讯网站
# 热门搜索 #
AITNT-国内领先的一站式人工智能新闻资讯网站 搜索
Robinhood创始人再创业研发超级数学AI,已接近国际数学奥赛选手,红杉领投近亿美金
5079点击    2024-11-22 14:01

Robinhood创始人再创业研发超级数学AI,已接近国际数学奥赛选手,红杉领投近亿美金


Z Highlights


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


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


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


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


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


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


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


Robinhood创始人再创业研发超级数学AI,已接近国际数学奥赛选手,红杉领投近亿美金


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


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


Harmonic 的第一个模型是 Aristotle(亚里士多德)。


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


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


Robinhood创始人再创业研发超级数学AI,已接近国际数学奥赛选手,红杉领投近亿美金


Robinhood创始人再创业研发超级数学AI,已接近国际数学奥赛选手,红杉领投近亿美金


(图源:Harmonic AI )


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


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


Robinhood创始人再创业研发超级数学AI,已接近国际数学奥赛选手,红杉领投近亿美金

(图源:Harmonic AI)


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


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


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


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


Robinhood创始人再创业研发超级数学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)领投。


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”


Robinhood创始人再创业研发超级数学AI,已接近国际数学奥赛选手,红杉领投近亿美金

AITNT-国内领先的一站式人工智能新闻资讯网站
AITNT资源拓展
根据文章内容,系统为您匹配了更有价值的资源信息。内容由AI生成,仅供参考
1
智能体

【开源免费】AutoGPT是一个允许用户创建和运行智能体的(AI Agents)项目。用户创建的智能体能够自动执行各种任务,从而让AI有步骤的去解决实际问题。

项目地址:https://github.com/Significant-Gravitas/AutoGPT


【开源免费】MetaGPT是一个“软件开发公司”的智能体项目,只需要输入一句话的老板需求,MetaGPT即可输出用户故事 / 竞品分析 / 需求 / 数据结构 / APIs / 文件等软件开发的相关内容。MetaGPT内置了各种AI角色,包括产品经理 / 架构师 / 项目经理 / 工程师,MetaGPT提供了一个精心调配的软件公司研发全过程的SOP。

项目地址:https://github.com/geekan/MetaGPT/blob/main/docs/README_CN.md