农食效率系统中供应链模型的定量验证：保障效率、公平与可持续性

项目概览

本博士项目将开发一个形式化验证框架，用于应对复杂多智能体系统中的可持续性挑战。多智能体系统刻画自主行动者之间的互动，这些行动者可以是个人、组织或数字实体，其决策往往涉及不确定性、激励和权衡。尽管这类系统是现代社会技术系统的核心，现有工具仍难以对可持续和公平结果是否能够实现提供严格保证。本研究将把形式化验证与博弈论推理结合起来，评估公平性、效率、韧性和环境影响等关键性质。项目的目标不是单纯优化供应链效率，而是用可证明的方法分析不同主体在冲突目标下能否形成公平且可持续的策略。

项目详情

框架将应用于农食供应链。农食供应链关系到全球粮食安全，但也面临浪费、排放和公平性等紧迫挑战。项目会把供应链中的利益相关方建模为相互作用的智能体，识别在什么条件下存在可持续且公平的策略，并评估这些策略面对扰动时的韧性。实际案例研究可能包括有机食品供应链，用于真实世界验证，重点关注浪费、低效率和透明度不足等风险。

研究将基于交替时序逻辑、关于信息透明度定量验证的前期工作，以及围绕责任进行战略推理的相关工作，把这些方法拓展到多智能体系统中的可持续性、公平性和韧性问题。博士生将学习和使用时序逻辑、概率验证、博弈论推理以及验证工具，并把这些工具应用到较真实的案例研究中。项目还包含可持续科学和风险评估方面的跨学科训练，可为学生未来进入计算、可信 AI 和可持续农食系统交叉领域的学术或跨行业职业发展做准备。候选人若具备逻辑、模型检测、概率系统、算法博弈论或程序验证基础，将更容易切入项目方法部分。

申请要点

项目为面向全球学生的已资助博士项目。候选人应具有计算机科学、数学或相关领域学位，并具备扎实的计算机科学和/或数学背景，尤其重视形式化方法和逻辑基础，同时需要良好编程能力。该项目不向来自阿富汗、喀麦隆、缅甸、苏丹或伊朗的研究人员开放。导师团队包括 Chunyan Mu（chunyan.mu@abdn.ac.uk）、Brian Logan（Brian.logan@abdn.ac.uk）和 Adewale Adenuga（a.adenuga@qub.ac.uk）。咨询联系人为 Chunyan Mu，邮箱 chunyan.mu@abdn.ac.uk。申请截止时间为英国时间 2026 年 10 月 16 日星期五中午 12:00。整体上，适合能把数学逻辑、计算机科学理论和可持续供应链应用结合起来的申请人。

需要进一步确认

建议申请前确认资助是否覆盖国际学生全额学费、生活津贴金额、注册院校与实际培养地点、SUSTAIN 博士培养中心的课程和跨校安排、是否需要 ATAS 或其他安全审查，以及项目使用的具体验证工具和案例数据来源。对中国申请人而言，项目列明的国籍限制不包括中国，且表述为面向全球学生；但仍需向联系人确认国际名额、签证支持和形式化方法背景要求是否满足。

PhD 项目深度调研报告：农食供应链模型的定量验证

申请判断

建议：有吸引力，但需要核实匹配度。 这是一个形式化方法色彩很强的可信 AI 博士项目。当前官方 A2227 项目页面计划把农食供应链表示为相互作用的策略型智能体，形式化描述效率、公平、韧性、透明度和环境影响等性质，再开发算法，在不确定性下检验这些性质是否成立。核心方法包括概率模型检验与博弈论推理，有机农业供应链可能成为实践案例。

项目的技术基础可信。Chunyan Mu 近年的工作覆盖概率策略逻辑、定量可观测性、因果责任和多智能体系统中的偏差验证。Adewale Adenuga 的专长包括农业与环境经济学、农场决策、资源效率和政策评估。Aberdeen 还拥有长期开展多智能体系统研究的团队、学校层面的科研计算支持，以及成熟的开源验证工具生态。

申请前最需要查清的是，形式证明如何转化为经得起经验检验的供应链结论。验证器可以证明某个数学模型满足某项性质，却无法自行证明模型准确覆盖真实食品供应链中的物流、激励、信息不对称、排放和分配后果。当前项目页面没有给出产业伙伴、数据集、数据所有者、访问协议、案例规模或验证方案。公开说明也发生过变化：现页面只列 Chunyan Mu 和 Adewale Adenuga，历史 A2227 页面则曾列出不同的导师与产业配置。因此，Brian Logan、Louise Manning、Marks & Spencer 及其他可能参与者，在 SUSTAIN 提供当前书面说明前都应视为尚未确认。

本轮招生信息仍然有效。招生项目页面显示，A2227 对应 2027 年 10 月入学，申请截止时间为 2026 年 10 月 16 日星期五英国时间中午 12 点。项目未标注“Home Students Only”。受限国家包括 Afghanistan、Cameroon、Myanmar、Sudan 和 Iran，中国不在其中，所以中国申请者原则上可以申请。不过，SUSTAIN 申请指南同时执行 UKRI 的 30% 国际学生上限，并提醒并非所有情况下都能提供 CAS 担保。符合资格不等于一定能获得面向国际学生的资助名额。

研究方向与领域前景

可发展的研究切入点

• 建立供应链建模 ontology，区分物理流、合同、信息、排放、安全事件与策略选择。
• 形式化多种相互竞争的公平定义，包括结果、机会、负担分配和程序透明，并说明它们在哪些场景下产生不同判断。
• 用多目标可持续性质、costs 和 partial observability 扩展概率策略逻辑或责任感知逻辑。
• 开发组合式或基于抽象的算法，在保留相关性质的同时控制状态空间增长。
• 结合参数合成与敏感性分析，把稳健保证和只在狭窄估计范围内成立的结论区分开。
• 比较形式化验证与离散事件仿真或 agent-based simulation，记录两类方法的结论差异。
• 用伙伴数据、专家意见和留出的冲击情景验证模型假设，不能只检查内部一致性。
• 建立可审计的证据链，把案例数据与假设一直连到模型参数、性质、反例和策略建议。

项目必须避免把“模型已经验证”写成“真实供应链已经验证”。有说服力的论文应明确限定每项保证所依赖的形式体系、智能体行为假设、数据周期、不确定范围，以及结论失效的条件。

领域进展

形式化验证能提供预测分析通常不给出的东西：把待检验性质写成明确的数学命题，并在模型范围内严格判断它是否成立。应用到农食供应链后，它可以揭示单一效率目标遮蔽的权衡。例如，某个策略可能减少浪费，却把成本或风险转移给小供应商；提高透明度有助于问责，也可能暴露商业敏感信息；增强韧性所需的冗余又可能推高排放或价格。

这类保证始终有条件。智能体、行动、信息集、激励、概率分布和时序性质都需要事先设定。真实供应链还存在缺失数据、策略性报告、延迟效应、价格与监管变化、议价能力差异和罕见冲击。过度简化这些因素，模型检验可能会对错误的问题给出正确答案。

可扩展性也是清楚的边界。企业、产品、时间步、隐藏信息和连续变量一旦增加，就可能发生状态空间爆炸。博士研究或许需要组合式验证、抽象、对称性约简、参数化模型检验、统计模型检验，或明确限制场景规模。较有价值的成果不仅要说明某项性质是否满足，还应给出结论对不确定参数和建模假设的敏感程度。

职业与行业前景

这套训练可通向形式化方法、安全或安保 assurance、可信 AI、运筹学、供应链分析、可持续性 assurance 和学术研究。英国 operational researcher 职业说明把数学与计算背景对应到政府和产业中的建模与组织决策支持。high-integrity software engineer 职业标准也明确包含数学分析、算法、model-based techniques 和验证工具，应用场景包括安全关键系统。

最可迁移的成果会是一套可复现的验证流程，配有清楚的规格、可扩展算法、反例、参数敏感性和外部验证。即使产业案例数据受保密限制，学生仍应争取发布通用模型、合成 benchmark 或工具扩展，以说明方法能超越单个合作案例。

学校、学科与培养

SUSTAIN 是一个为期四年的 UKRI AI Centre for Doctoral Training，由 Aberdeen、Lincoln、Queen’s Belfast 和 Strathclyde 共同参与。项目概览介绍了 cohort training、与产业相连的真实项目，以及横跨计算、数据、农业、食品系统和负责任创新的训练。这种结构与本项目很匹配：形式化方法必须足够深入，同时也需要农业经济学与伙伴参与，避免“公平”或“可持续”只停留在符号定义上。

牵头学校是苏格兰的 University of Aberdeen。Aberdeen 2040 战略把 Data and Artificial Intelligence、Environment and Biodiversity 都列为学校重点。与项目更直接相关的是，Agents at Aberdeen长期研究自主智能体、多智能体系统、知识表示、韧性、可靠性和协调。这一研究环境比综合排名更能说明项目是否有技术支撑。作为外部参照，QS 学校页面把 Aberdeen 列在 2027 World University Rankings 第 288 位。

SUSTAIN 说明，学生通常在项目牵头学校学习，所有项目都会有外部伙伴参与。但当前 A2227 页面没有说明伙伴身份。申请者应确认博士期间是否全程在 Aberdeen，是否包括 Queen’s Belfast 或产业机构的驻留，以及相关差旅、安全数据访问和伙伴指导是否已有预算。

导师与团队评估

导师研究方向

Chunyan Mu 的 Aberdeen 主页显示，她是 Computing Science 的 Senior Lecturer，也是 Agents at Aberdeen 成员。她近期的研究与项目高度吻合，涉及定量验证、信息不透明与可观测性、策略逻辑、概率多智能体系统、因果责任，以及偏差的形式化推理。项目的技术主线延续了她正在开展的论文工作，并非临时转向形式化方法。

Adewale Adenuga 的 Queen’s 主页显示，他是一名农业经济学者，研究覆盖农场与家庭经济、资源利用效率、可持续农食系统、行为经济学和定量政策评估。Gibson Institute则提供更广的土地、食品与农村政策环境。Adenuga 的作用很关键，因为公平、韧性和可持续性需要转化为符合领域实际的变量、情景和权衡关系。

目前官方页面只确认 Chunyan Mu 和 Adewale Adenuga。Brian Logan 仍是 Aberdeen 的教授，也是相关论文作者，但没有出现在当前项目页面上。现阶段可确认的正式导师只有两位，其他导师分工仍需书面核实。

近期代表性论文

• 2025 年论文“Probabilistic Strategy Logic with Degrees of Observability”在概率策略逻辑中加入量化时序性质对智能体可观察程度的算子，并证明相应模型检验问题可判定。它为随机供应链交互中的透明度推理提供直接基础。局限在于领域落地：逻辑本身无法决定哪些行为应当可见，也无法说明真实证据如何生成状态转移概率。

• 2025 年论文“Responsibility-aware Strategic Reasoning in Probabilistic Multi-Agent Systems”提出 PATL+R，并合成在期望因果责任与 reward 之间权衡的策略。这可用于分析哪一类主体应为浪费、不安全操作或不公平分配负责。不过，责任度量与 reward function 仍是可能引发利益相关者争议的建模选择。

• 2026 年 AAMAS 论文“Reasoning about Bias in Multi-Agent Systems Verification”通过属性干扰定义偏差，在 Alternating-time Temporal Logic 中加入偏差算子，并给出模型检验程序。它提供了一种公平性的形式化处理方式，但 trace-equivalence fairness 未必能覆盖真实食品供应链中的分配公平、议价能力或程序正义。

• 2026 年 IJCAI-ECAI 论文“Counterfactual Reasoning for Causal Responsibility Attribution in Probabilistic Multi-Agent Systems”把系统建模为 concurrent stochastic games，用 Shapley values 分配责任，并通过 Nash equilibrium 推理稳定策略。这些方法适合研究供应链中的责任分配，但大规模网络的计算可扩展性和经验解释仍未解决。

实验条件、设备与协作环境

Agents at Aberdeen是最直接的学术环境。项目还可使用 PRISM。该工具是成熟的开源概率模型检验器，支持 Markov chains、Markov decision processes、partially observable models、时序逻辑、costs 与 rewards。PRISM-games把这一工具栈扩展到竞争与合作型 stochastic multi-player games，并支持策略合成。现有工具足以说明方法可实施，但博士工作可能仍需开发新的性质语言、领域编码或可扩展算法，不能只运行已有示例。

Aberdeen 的数字科研与数据管理服务包括 HPC、定制科研咨询、数据管理计划支持、Data Safe Haven 和 SafePod。这说明学校具备基础设施，但不代表 A2227 已获得专用算力。形式化模型检验可能遇到严重的状态空间增长，申请者应询问预期模型规模、计算配额、内存需求、工具开发支持，以及选择精确验证、符号验证、统计验证或抽象方法的依据。

产业与验证资源目前更不清楚。SUSTAIN 表示项目与外部伙伴共同设计，旧版 A2227 曾列出 Marks & Spencer；现页面既未列公司，也没有数据说明。因此，目前无法确认学生会得到交易数据、物流事件、排放估算、供应商属性、专家访谈、仿真输入，还是只有一个风格化案例。这个差别会直接改变论文范围和成果可复现性。

资助、申请与生活成本

SUSTAIN 博士资助方案称，项目支付全部博士学费，按 UKRI 标准提供免税生活津贴，并提供每年 £3,000、合计最高 £12,000 的 Research Training Support Grant，另有 outreach、summer schools 和科研活动支持。UKRI 当前 training-grant 指南给出的 2026/27 最低生活津贴是 £21,805，fee level 为 £5,238。2027/28 津贴尚未确认，因此 £21,805 只能作为背景参考，不能视为最终 offer 金额。

海外学费差仍未闭环。SUSTAIN 表示支付全部学费，而 UKRI 面向受资助学生的说明指出，UKRI 最多按 home-fee rate 出资；如果学校不补足差额，国际学生可能需要承担一部分。中国申请者应要求书面确认 A2227 会覆盖 Aberdeen 完整的海外研究学费，学生无需补缴。

申请分两个阶段：先提交在线表格，再通过电子邮件发送 CV、成绩单和国际申请者所需材料。一般最低要求是相关专业一等或 2:1 本科学位，或 merit 等级的 MSc；非英语母语者通常需要 IELTS equivalent 6.5。匿名申请回答需要说明所选项目、团队和 host institution。推荐信在面试后才会索取，入围申请者还要做 presentation，考察专业知识、沟通和产业知识。

当前英国 Student visa 资金要求在伦敦以外是每月 £1,171，最多计算九个月。这只是签证资金证明下限，不等于 Aberdeen 的实际生活预算。申请者还需分别估算房租、水电、饮食、签证、immigration health surcharge、差旅、计算设备和家属成本，并确认伙伴驻留、安全数据环境或产业差旅是否另有预算，而非全部从每年 £3,000 的 RTSG 中支付。

申请适配度与准备重点

更适合

• 逻辑、概率、算法和编程基础较强的计算机或数学申请者。
• 对时序或策略逻辑、概率模型检验、stochastic games 和多智能体系统感兴趣的形式化方法申请者。
• 愿意从优化或仿真转向显式性质验证的运筹学申请者。
• 能与农业经济学者和产业利益相关者合作，共同定义公平与可持续等有争议概念的申请者。
• 清楚数学保证受假设、数据质量和验证证据约束的申请者。

需要谨慎

• 主要目标是训练常规机器学习预测模型的人。项目的学术中心是规格描述与验证。
• 不愿处理证明、逻辑或算法复杂度的人。
• 希望入学第一月就有一套确定且整洁的商业数据的人。现有公开资料没有承诺这样的数据。
• 预期所有伙伴数据、模型文件和代码都能直接公开，而不需要协商的人。
• 偏好单一学科，不愿协调计算定义与经济、伦理、运营解释的人。

值得补强的能力与材料

适合提前准备的内容包括时序逻辑、模型检验、Markov chains 与 decision processes、stochastic games、博弈论、算法、复杂度分析和严谨编程。PRISM 或同类工具经验会很有帮助。Python、Java 或 C++ 可用于数据准备、实验和工具扩展，但当前官方页面没有指定编程语言。

有说服力的作品集可以选择一个小型多智能体分配或物流问题，精确定义性质、实现模型、生成反例或合成策略、测试可扩展性，并指出哪些假设缺乏经验支撑。可复现文件、版本控制和简短的敏感性分析，比通用图像分类演示更贴近这个项目。

下一步与待确认问题

首要科学风险是抽象模型的有效性。“公平”“透明”“韧性”和“可持续”没有天然唯一的形式定义。不同参与者可能分别重视分配、程序、信息访问、成本、食品安全和排放。项目需要记录定义、阈值和权重的选择过程，最好让伙伴专家和受影响利益相关者参与，而不能只由研究人员决定。

数据与 IP 也可能限制研究。Aberdeen Research Data Management Policy要求规划访问、许可、安全处理、存储和第三方权利。IP, Equity and Revenue Sharing Policy规定，postgraduate research students 注册时把 IP 转让给学校，但可在导师同意下申请 opt out；第三方协议也可能影响所有权。申请者应确认背景数据权利、代码与形式模型的归属、发表审查期、开源权限，以及哪些内容能进入论文。

公开团队信息的不一致同样重要。当前官方项目只列 Mu 和 Adenuga，较早的版本及收集材料则出现过其他人员和产业伙伴。这可能只是项目正常调整，但会改变可获得的专长和数据路径。最终 offer 应以书面形式明确正式导师、伙伴和预期访问资源。

以下按申请进程安排沟通。具体提交要求仍以项目的正式申请说明为准。

提交申请前

• 奖学金是否覆盖完整海外学费？在 30% 国际学生上限下，Aberdeen 能否为中国申请者签发 CAS？

联系导师或面试时

• 2027 cohort 正式任命了哪些导师？Brian Logan 是否承担明确角色？
• 项目开始时会提供哪种供应链模型、数据集和案例规模？
• 公平、可持续、透明和韧性将怎样定义、质询并确定优先级？
• 会使用或扩展哪些验证工具？如何处理状态空间爆炸和不确定参数？
• 哪些证据用于验证抽象模型：留出的事件、专家意见、仿真、真实决策，还是几者结合？
• 背景数据、代码、形式模型、算法和派生结果分别归谁？学生可以发表或发布哪些内容？
• Mu 与 Adenuga 如何分工？两位导师与学生共同开会的频率是多少？
• 项目承诺多少算力、安全环境和专业软件支持？
• 保密条款或伙伴审查期是否可能延迟论文章节、会议论文或代码发布？
• 论文预期产出是新逻辑、模型检验算法、工具扩展、经验证的领域框架，还是其中明确的组合？
• 主要案例会选择哪条有机食品或其他供应链？它为何具有代表性？

接受录取前

• 当前外部伙伴是谁？合同已承诺哪些数据、人员时间和验证机会？
• offer 中会列出怎样的 2027/28 津贴金额、发放周期和搬迁支持？

证据与来源

项目、培养、资助与资格

• 当前官方 A2227 项目页面
• SUSTAIN 招生项目
• SUSTAIN 申请指南
• SUSTAIN 博士资助方案
• SUSTAIN 项目概览
• UKRI training-grant 指南
• UKRI 受资助学生支持说明

学校、导师、方法与资源

• Aberdeen 2040 战略
• University of Aberdeen QS 页面
• Chunyan Mu 研究主页
• Adewale Adenuga 研究主页
• Agents at Aberdeen
• Gibson Institute for Land, Food and Environment
• Aberdeen 数字科研与数据管理服务
• PRISM 概率模型检验器
• PRISM-games
• 历史 SUSTAIN A2227 页面

论文、职业、成本与治理

• Probabilistic Strategy Logic with Degrees of Observability
• Responsibility-aware Strategic Reasoning in Probabilistic Multi-Agent Systems
• Reasoning about Bias in Multi-Agent Systems Verification
• Counterfactual Reasoning for Causal Responsibility Attribution
• Operational researcher 职业说明
• High-integrity software engineer 职业标准
• Student visa 资金要求
• University of Aberdeen Research Data Management Policy
• University of Aberdeen IP, Equity and Revenue Sharing Policy