安全人工智能的形式化方法博士

项目概览

伯明翰大学计算机科学学院提供一个“安全人工智能的形式化方法”博士研究机会，联系人为Dr Mirco Giacobbe。项目面向英国及国际申请者，属于竞争性博士资助项目，申请截止日期为2026年12月18日。研究把形式化方法、机器学习与软件工程连接起来，希望为与深度学习和神经网络交互的数字、物理及概率系统建立可形式化证明的安全保证。

项目详情

安全人工智能关注如何自动确认AI系统满足正确性规范。对于集成神经网络的系统，计算机辅助形式化验证尤其重要：神经网络难以由人直接解释，系统可能自动改变行为，而且越来越多地作用于现实世界。仅观察一些运行结果，不能覆盖所有可能情况，因此这些系统的正确性验证仍是开放的研究问题，对学术界和工业界都有意义。

项目介绍特别讨论了两个应用背景。第一，AI编程代理生成和修改软件的速度可能超过人工审查能力，使关键代码面临隐蔽错误和漏洞风险。第二，在机器人和自动驾驶中，学习得到的决策组件直接作用于物理世界，错误可能造成不可逆的后果。博士研究希望从明确的正确性或安全规范出发，发展可辅助检查这些系统的理论和工具，而不是只依赖模型在有限测试中的表现。

相关方法既包括符号技术，也包括新的机器学习方法。符号技术包括模型检测、抽象解释，以及可满足性模理论（SMT）；机器学习则可能用于支持安全AI的分析和构造。研究问题包括确保含深度学习组件的信息物理系统安全，以及确认软件、硬件中的算法组件正确，其中也包括AI生成的代码。这些是可能研究的问题，不构成仅限两种固定课题的清单。

总体目标是发展验证、综合及机器学习方法，使数字系统、物理系统和概率系统在与神经网络交互时能够获得形式化安全保证。这里的“综合”指围绕规范构造符合要求的系统或组件，与事后检验已有系统形成互补。项目横跨计算机科学理论与实践，候选人可开展学习系统形式化验证的理论和／或实验研究，具体侧重可结合研究问题形成。

博士生还可以研究理论计算机科学与机器学习之间的联系，例如逻辑、自动机如何与学习方法结合，并探索控制、机器人等科学与工程应用。项目将学生置于相关研究环境中，既需要分析数学模型与算法，也需要开发软件原型、学习验证及机器学习工具链。公开说明并未规定必须同时完成所有应用方向，也没有列出固定的年度工作包、具体硬件平台或软件产品交付数量。

申请要点

• 需要分析能力，包括数学建模、逻辑和算法设计方面的扎实基础；也需要编程能力，愿意学习验证与机器学习工具链，并能够开发软件原型。项目特别强调同时对数学和代码感兴趣。

• 邀请计算机科学、电气工程、数学、物理，或与团队研究及拟开展课题相关的其他背景申请者。学历要求为英国一等或二等一荣誉本科学位，或国际同等学历。

• 英国及国际申请者均可申请。项目属于面向全球申请者的竞争性资助遴选，不能把提交申请直接等同于获得奖学金。

• 团队希望博士群体体现社会多样性，强调机会平等，鼓励少数族裔、代表性不足群体、残障及神经多样性申请者；介绍提及可通过非全日制、分地点学习等方式支持个人情况，具体可用性需结合申请及资助安排确认。

• 申请截止2026年12月18日；联系人Dr Mirco Giacobbe。课程及申请入口为伯明翰大学计算机科学博士项目。

需要进一步确认

大学官方项目详情补充说明：全日制奖学金为三年半，竞争授予优秀申请者，覆盖符合资格的本土及国际学生学费，并提供每年£21,805免税生活津贴，标准通常在每年10月1日调整。未来入学年度的实际津贴、研究预算、正式材料清单、入学时间和具体截止时刻仍需确认。导师日常指导频率、第二导师、理论与工具开发的比例、选定应用及计算资源，也需要进一步确认。

PhD 项目深度调研报告：伯明翰安全 AI 的形式化方法

是否值得申请

这个博士要解决的，是怎样用数学证据判断 AI 系统是否满足明确规范。博士既需要逻辑和算法，也要写出可运行的验证原型，可探索 AI 生成代码、硬件或物理控制系统。大学官方项目确认招收一人，竞争性全日制三年半奖学金包含符合资格的本土及国际学生学费豁免，目前免税生活津贴为每年 £21,805。2026 年 12 月 18 日截止，具体时刻和入学日期未说明。宜先联系 Mirco Giacobbe，确认方向、材料清单和入学年度资助安排。当前官方项目；导师联系方式。

从有限测试走向可检查的保证

研究对象是包含学习组件的系统。形式化规范可以描述控制器始终避开危险状态、最终到达目标，或程序遵守某项断言。挑战是超越有限测试，判断系统是否符合规范。AI 编程代理增加代码审查负担，机器人和自动驾驶则将错误决策与物理后果连接起来。招聘范围涵盖与深度网络交互的数字、物理及概率系统。招聘所列科学问题。

博士可以发展验证、综合和机器学习方法。模型检测检查系统是否满足逻辑性质；抽象解释用可靠近似控制分析复杂度；可满足性模理论（SMT）求解涉及数学理论的逻辑约束；“综合”则围绕规范构造系统或组件。项目允许理论和／或实验研究，也可探索逻辑、自动机与学习的联系及控制、机器人应用，并非要求一个博士完成所有方向。

团队近期论文提供了一条具体切入：先学习候选证明证书，再用符号推理独立检查。神经网络训练成功本身不是证明；可靠检查才为所建模型上的性质提供保证。证书表示、规范表达力、求解器扩展性或物理抽象是否忠实，都可能形成研究问题。这些是基于论文的判断，不是已指定工作包。保证仍依赖规范、模型和假设；即使证明过程正确，也不能替错误规范担保现实世界安全。神经模型检测；连续时间证书；定量验证。

学校、学科与博士培养

项目设于英国伯明翰大学计算机科学学院，学位由伯明翰大学授予。课程通常为全日制三年、线下研究，配有导师、论文小组及定期进展审核；专项奖学金为三年半，需确认研究、写作和注册里程碑如何对应。非全日制及分地点支持不等于每位申请者都可按这些方式获得资助或符合签证要求。导师兼任 Zeroth Research 职务，也不代表本博士为企业雇佣或联合学位。博士课程。

课程公布 QS 2027 综合第 68、Complete University Guide 2027 英国计算机科学第 6；学院另说明，在 REF 2021 的 GPA 与四星研究口径中列英国第 3。年份、地区和评估范围不同，不能将这些数字当作具体形式化验证项目排名。Theory of Computation 团队将 Giacobbe 列入程序语言、验证与模型检测方向；学院有理论研讨、lab lunch 及 Midlands Graduate School 网络，大学博士培养提供个性化能力计划和研究生职业支持。具体实习、算力及第二导师尚未确认。学院与 REF；理论研究群体；博士能力发展。

导师与近期研究

学校人员页仍将 Mirco Giacobbe 标为 Lecturer，个人主页和 CV 则为 Associate Professor，CV 明确自 2025 年 2 月任该职。这是资料更新口径差异。其牛津 Research Associate 经历已于 2021 年 8 月结束，不能宣传为当前牛津任职。CV 介绍的团队及 ARIA、Amazon 相关项目支持研究网络判断，但不足以确定是哪项经费支付本奖学金。考虑到其大学及企业职责，可在面试中问清实际会议时间和日常指导人。大学人员页；个人主页；有日期的履历。

三篇论文与招聘直接衔接：

• Giacobbe、Kroening、Pal、Tautschnig，NeurIPS 2024，Neural Model Checking： 从运行轨迹学习神经排序证书，再进行逻辑检查，以验证硬件 LTL 性质；原型结合 PyTorch、EBMC、Spot、Verilator、Bitwuzla。194 项 SystemVerilog 测试体现工具实现，但 SMT 耗时、局部极小值、字级表示与跨任务泛化仍有限制，且不支持 CTL。论文与局限。
• Neustroev、Giacobbe、Lukina，AAAI 2025： 用神经超鞅证书，将概率验证推进到连续时间系统，为到达、避障、保持等要求提供概率界。分析基于给定策略、模型正则性和紧致区域假设；自动综合控制器及更丰富时序性质属于后续扩展，不能当作已全部解决。正式论文。
• Abate、Edwards、Giacobbe、Punchihewa、Roy，LMCS 2026： 结合反例引导学习与 SMT 检查，为概率程序和离散随机模型建立可靠概率界，讨论使用或不使用程序信息的证书构造方式。超出可达性的性质及网络结构、规模问题仍开放。这是 CONCUR 2023 工作的期刊扩展。期刊研究。

本次读取摘要及部分方法、假设、评估或结论，未独立检查全部证明或重跑基准。共同署名证明研究联系，不足以拆分每位作者的具体贡献。连续时间研究已有带版本的软件归档，可用于了解可复现条件和准备小例子；本次未测试其运行环境及当前依赖。软件归档。

资助与伯明翰生活

具名官方项目确认三年半全日制奖学金，竞争授予符合资格的本土及国际申请者，包含学费豁免。当前年 £21,805 为免税津贴，通常每年 10 月 1 日调整，与 2026 年 10 月生效的 UKRI 最低标准相符；实际入学及后续年度标准需确认。研究、算力与差旅额度，签证、IHS 和搬迁由谁支付，尚未明确。大学说明竞争性资助是项目之间争取奖项，得到导师兴趣或学术录取不等于获得奖学金。具名资助说明；竞争资助解释；有日期的 UKRI 参照。

课程选择中国后，2027 入学国际学费为每年 £30,780，本土参照为 £5,400。差额 £25,380 说明国际学费豁免的重要性，不能写成符合资格的获奖者必须补交。应确认书面豁免及覆盖期间，避免套用仅覆盖本土标准的其他奖项。写作／延续注册可能另有费用；一般费用页有旧年份数字，剩余责任最终须以录取和资助文件确认。课程学费；研究生费用规则。

当前官方住宿可提供一个具体参照：Jarratt Hall 列出每周 £189、研究生 50 周总价 £9,445，含水电、Wi-Fi 和物品保险。周价经过取整，应保留官方合同总价，不能简单相乘代替。它只是一个合同报价，不是全年总生活费或 2027 年房源承诺。住宿与合同。

学校研究生理财页列出基本与可变开支，但表格未注明适用学年、按 50 周计算，且保留旧行政事项，宜作为分类清单而非当期价格保证。预算应覆盖完整 52 周、饮食交通及个人／学习开支、合同结束后的住房、移民、机票和抵达储备。不能用这份未注明年份的预算与未知的未来津贴承诺结余。开支分类与资料边界。

申请条件与可迁移能力

项目明确需要数学建模、逻辑、算法设计及编程基础，愿意学习验证和 ML 工具链。邀请计算机、电气工程、数学、物理及其他相关背景，学历为一等／二等一荣誉本科或国际同等资格，并未要求入学前精通每个求解器。课程英语为 IELTS 总分 6.0、单项至少 5.5，或指定替代资格。项目背景条件；课程学历与英语。

中国申请者存在附条件审核路径，没有已核实的统一分数线。中国页面院校分组成绩表明确属于 PGT，不能直接套给本博士；中国选项的博士课程也未展示具体数字等同性。应提供学校、四年制学位及成绩，请招生确认。课程提示符合情形的国际生须在 CAS 前取得 ATAS；政府规则同时设国籍及移民身份豁免。只有中国国籍并不构成豁免，但 ATAS 是审批过程，不能改写成中国申请者禁申；须结合 offer、CAH3 及个人情况判断。中国学历说明；ATAS 规则。

通过课程在线入口申请并注明具名项目。通用广告项目指南列出学历证书、成绩单或阶段成绩，使用单位邮箱的推荐人，以及约 5,000 字符的个人陈述；页面提到两份推荐材料，部分系统说明为一至两位。研究计划的明确要求主要针对自拟课题，本项目是否另需 proposal 应向导师确认，不能照搬其他项目“上传空白计划”的规定。语言考试通常须在入学前两年以内。导师联系有助于明确要求，但不代替正式提交。广告项目申请指南。

准备时可用一个数学论证配合小型可复现原型，说明方法在哪些情况失败。这是展示能力的建议，不是新增必交作品集。技能可衔接形式化验证、EDA、可靠软件、自主系统保障及学术研究。英国 2025 年 AI assurance 路线图提出建设技能框架与职业路径，说明保障方法有政策及行业发展背景；但它没有证明具体细分岗位数量、毕业薪资或伯明翰去向，形式化验证也只是更广保障体系的一部分。英国保障技能政策。

下一步与待确认问题

申请前，确认正式材料清单、截止时刻、入学日期及个人中国学历等同性。面试时，问清优先方向、第一年基准与规范、符号检查的扩展性、日常指导，以及计算和软件支持。接受前，取得书面津贴、三年半资助与免学费起止日，核对写作费、研究差旅、签证/IHS/搬迁责任及 ATAS、CAS 顺序。

证据与来源

项目、学校与准入

• University official named PhD project
• Mirco Giacobbe university profile
• Mirco Giacobbe personal research site
• Mirco Giacobbe career CV
• Computer Science PhD,2027
• Computer Science research and REF
• Theory of Computation group
• Birmingham Doctoral Programme
• China qualifications guidance
• Apply for an advertised PhD
• Academic Technology Approval Scheme

研究与软件

• Neural Model Checking
• Neural Continuous-Time Supermartingale Certificates
• Quantitative Verification with Neural Networks
• Continuous-time certificate software artifact

资金、生活与职业

• Funding postgraduate research
• Fees for postgraduate researchers
• Money advice for postgraduates
• Jarratt Hall postgraduate accommodation
• DSIT AI assurance roadmap
• UKRI student financial support