Formal Method by Agents

音频围绕形式化方法在程序生成与汽车设计中的应用、大语言模型的局限性、体育策略分析以及超级智能时代人类角色等内容展开讨论，内容如下：

• 形式化方法与程序生成
• 形式化思维链确保程序正确
• 运用 refinement calculus 作为形式化的思维链，能产生 100% 正确的程序，如解决平方根问题，通过 separational composition law、assignment law 和 integration law 等可保证程序代码的正确性。
• 相关成果已发表在去年和凌云合作的 poco paper 中，但复杂程序或系统设计生成可能面临新挑战。
• 大语言模型在程序生成中的不足
• 让大语言模型生成平方根程序时，GPT5 和 Gemini3 都出现错误，原因是其长思维链不正式，各环节间缺乏形式化连接和保证。
• 目前大语言模型在解决复杂问题上还不够擅长，不过结合研究有望生成自动的大语言模型 agent。
• 形式化方法在汽车设计中的应用
• 特斯拉设计缺陷案例
• 特斯拉汽车水传感器检测到车辆浸入水中时，未触发车门解锁，导致车内人员被困淹死，这是设计失误。
• 大语言模型给出的改进建议多聚焦于用户界面，未抓住关键的传感器触发车门锁状态问题，而形式化方法可解决此问题。
• 小米汽车安全问题
• 小米汽车在高速行驶遇障碍物时，仅给用户 3 秒手动控制时间，碰撞后车门仍处于锁定状态，导致车内人员被烧死。
• 应在碰撞传感器检测到重大撞击时，同时触发气囊弹出和车门解锁，以保障人员安全。
• 体育策略分析
• 大语言模型在体育策略中的不足：大语言模型为费德勒提供的打败纳达尔的策略全错，如建议多用反手削球，而纳达尔擅长处理上旋球，此策略会让费德勒更吃力。
• 概率模型助力体育策略
• 运用概率模型分析，建议费德勒多打反手直线球，其提高 2% 赢球几率可增加 5%。费德勒听从建议，2017 年反手直线球提高 3%，24 次全部打败纳达尔。
• 为无名小将 Muelman 提供概率监督报告，助其 2018 年首次打败费德勒。还为小德分析对阵费德勒的策略，助其 3：0 战胜对手。
• 对郑钦文比赛进行分析，助其在意大利公开赛首次打败萨门。
• 超级智能时代人类角色
• 玩家角色：许多人将成为玩家，参与体育、电子竞技、音乐、舞蹈等娱乐活动。
• 探索者角色：当麻烦成本变大时，人们会因好奇心成为探索者和旅行者，在玩乐和探索中产生新想法。
• 共创者角色：与 AI 共同创造新系统和新世界。
• 守门人角色：人类需成为守门人，确保 AI 的安全、可靠、对齐和鲁棒性，防止 AI 完全控制。