可解释软件系统博士：随机与动力系统的认证式验证

项目概览

TUD 德累斯顿工业大学计算机学院理论计算机科学研究所、计算机科学代数与逻辑基础教席招聘研究助理／博士研究人员。岗位属于SFB/Transregio 248“Foundations of Perspicuous Software Systems”，研究随机系统和动力系统的可认证验证算法，以及可解释性与可行动性的形式化方法。联系人为Christel Baier教授。工作语言为英语，计划2027年1月1日开始，合同至2030年12月31日，岗位设置以经费可用为前提。

项目详情

认证式验证关心的不只是工具给出的概率值或安全结论，还包括能由独立检查器核验的证据。可解释性进一步追问哪些系统条件和行为影响结果；可行动性关注使用者能够改变什么。这三类问题相关，但不能把“已有验证结论”等同于“已为不同用户提供有用解释”，也不能把模型中的证明直接当成真实系统准确性的证明。

博士的主要任务是研究并开发面向随机系统与动力系统的认证式验证算法，以及用于解释与行动选择的形式化方法。理论基础涉及验证、自动机与逻辑，也与概率、优化和复杂性分析相连。可以讨论证书规模和检查成本、多目标保证与解释质量、不同策略假设下的因果解释等切入点；这些是已有论文提示的研究问题，不是招聘指定每人必须完成的题目。招聘没有指定必用编程语言、证明器、软件产品、模型类别或首年基准，需由具体课题确定。

TRR248针对未来信息物理系统建立可理解软件的科学基础，研究覆盖系统行为的解释理论，以及适合不同用户群体的视觉和语言解释方法。项目让验证、分析、系统构造与解释形成共同研究背景；本岗仍需有可识别的个人博士贡献，不能只按共享工具维护任务理解。

学校、学科与培养：TUD是招聘大学和拟开展博士培养的单位，合作网络包括其他大学和研究机构，不表示共同授位。获得工作合同与博士学术接收是两道程序，需导师同意、博士委员会接收、指导协议及适用的学历认定。学院区分不同学位路径；Ph.D.路径获接收后3个月内需提供注册证明，其他路径注册为自愿且受鼓励。个人学位名称、境外学历等值及可能的补充考核须确认，四年拟聘期不是自动入学或保证毕业。

岗位支持包括协作研究环境、灵活工时、职业发展与继续教育、健康和体育项目、优惠公共交通工作票（含Deutschlandticket选择），以及VBL公共部门员工补充养老计划。每年30天年假以每周5天工作为口径。学校重视多样性与家庭友好，鼓励女性申请；同等资质下，残疾及德国SGB IX等同身份申请者优先。

申请要点

要求计算机科学或相关学科大学学位、扎实理论计算机基础、很好的数学基础、有条理地独立推进项目并与参与者沟通，以及优秀英语书面和口头能力。验证、自动机和逻辑背景受到优先考虑；良好编程技能及实验工作兴趣为desirable，不能全部升级为一律必备。学位说明列Master和应用科学大学Diplom，最终学历资格仍须由招聘及博士接收程序判断，未列统一英语考试分数或国籍排除条件。

按个人资格适用E13 TV-L；工时比例、具体工资档次、净薪及单独费用安排未列明，不能据薪级直接算到手金额。拟聘至2030年12月31日仍附资源可用条件；已有研究网络资料仅列至2026年的资助期，需确认后续落实，不能由此认定岗位已取消。

截止2026年10月30日，以大学中央收件到件戳或TUD邮件服务器时间戳为准；未公布精确钟点和时区。提交详细申请及常规材料，包括动机信、CV和学历证书，优先经TUD SecureMail合为1份PDF发至professur-alg@tu-dresden.de，也可邮寄至TU Dresden, Chair of Algebraic and Logical Foundations of Computer Science, Prof. Dr. Christel Baier, Helmholtzstr.10, 01069 Dresden, Germany。纸质材料只交副本，学校不退还；面试费用不予报销。岗位官方入口；安全邮件入口。

需要进一步确认

申请前落实工时比例、经费条件与个人博士接收路径；面试讨论模型范围、第一年问题、导师反馈和证明／实现工作的分配；接受前确认合同、薪资依据、注册与住房及许可时程。当前受理状态和门户操作未在此次编辑中重新核验，不应仅凭未来截止日推定仍可递交。

TUD 德累斯顿工业大学：认证式验证、解释与可行动性

项目价值与关键条件

这个岗位连接3个问题：验证结论凭什么可信，系统行为怎样解释，以及解释能否帮助使用者作出改变。核心是随机与动力系统的认证式算法和形式化方法，适合以数学定义、证明和算法实现开展研究的方向。岗位拟2027年1月1日至2030年12月31日聘用，按个人资格适用E13 TV-L，但资源可用条件、工时比例和个人博士路径仍须落实。官方招聘

已有招聘资料列截止2026年10月30日，以中央收件到件戳或TUD邮件服务器时间戳为准，没有另列精确钟点及时区。未来截止日不等于已确认当前门户仍受理；应在递交前确认实际渠道。论文和网络背景有助于判断方向，经费条件则必须落实到个人合同。

研究问题与博士工作

随机系统的行为可能取决于概率和策略，动力系统又涉及随时间演化的状态。岗位要求为这两类系统研究并开发认证式验证算法，同时用形式化方法处理解释与可行动性。可以先区分各层成果，而不是把它们统称为“让软件可解释”：

工作层次	要回答的问题	有意义的博士成果及边界
可认证验证	概率值或安全结论为何成立，能否独立检查？	明确定义的证书／见证、适用模型及正确性论证；检查器仍依赖模型与规约
可解释性	哪些条件或路径影响结果，解释对谁有用？	给解释规定形式语义，并比较质量、规模或检查成本；不是只有可视化展示
可行动性	使用者可以改变什么，结论在何种策略假设下有效？	清楚限定可改变的条件及结果，不能把特定策略假设推广为任意系统保证

表中成果标准是依据岗位与已有论文提出的分析框架，不是额外指定的实验清单。教研组研究反应式系统、随机分析与综合；招聘未指定编程语言、定理证明器或交付产品。第一年采用有限／无限状态、连续／离散模型，以及何种基准，应与导师确定。官方招聘；代数与逻辑基础教席

有价值的贡献可以结合严格定义、适用范围内的正确性与完备性论证、复杂性分析及明确基线的原型实验。三篇论文分别提示证书压缩、多目标解释质量和策略假设下因果解释等问题，具体独立创新点仍须讨论。证书证明的是模型与规约之间的关系，模型是否准确反映部署系统需要另行判断。

TRR248把分析、构造与解释贯穿系统设计、运行和检查，探索覆盖行为多方面、适合不同用户的视觉与语言解释方法。本岗既有协作框架，也需保留可完成的个人研究问题；工具维护、实验合作及计算资源安排尚未明确。研究网络框架

学校、学科与培养

岗位所在单位是 TUD 德累斯顿工业大学计算机学院、理论计算机科学研究所、计算机代数与逻辑基础教研组。TUD 是招聘大学和拟开展博士培养的单位。TRR248 网络还包括萨尔大学、MPI-SWS、CISPA 等机构；参与研究网络不代表这些机构共同授予学位，也不能据此推定双学位。TRR248 Center for Perspicuous Computing

学校公布的 QS 世界大学排名 2027 中，TUD 综合排名为 185；同一校方报道引用 QS 学科排名 2026 工程与技术第 94。两项都不能直接说明计算机或形式化方法的学科位置。现有资料未明确适用的计算机学科具体名次。对这个理论方向，教研组的研究积累及 2024—2025 年论文更能帮助判断匹配度。TUD report on QS World University Rankings2027

拿到工作合同与获准读博是两道程序。学院要求合适且成绩良好至优秀的博士入学学历及研究论文，需要导师同意、博士委员会接收，并签署指导协议。境外学历须接受等值认定，可能要提供经认证的文件及英语或德语译文。学院区分不同博士路径：走 Ph.D. 路径者需在获接收后 3 个月内提供注册证明；其他路径的注册为自愿且受鼓励。最终学位名称、适用路径、注册及可能的补充考核，应按个人学历确认。四年的拟聘期不能直接当作保证毕业的学制。学校Graduate Academy另提供免费的通用能力课程、科研诚信培训、导师交流与职业支持。Faculty of Computer Science doctoral admission and procedure Graduate Academy qualification and career support

导师与研究条件

Christel Baier 是招聘联系的教授，也是自 2006 年起负责该教研组的学者，研究涵盖概率模型检测、逻辑与无限状态系统。个人主页和学校论文目录显示她持续参与这些方向，但不能据此推断指导频率、学生完成率或本岗位的具体导师分工。需要确认日常技术反馈由谁负责，是否有第二导师，以及证明和实现工作的时间如何安排。Christel Baier official academic profile Christel Baier institutional publication list

近年的三篇论文能帮助判断课题内容：

• 《Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes》，Baier、Chau、Klüppelholz，QEST+FORMATS 2024，作者预印本于 2025 年修订。研究从线性规划表述中构造可检查的证书与见证，覆盖多目标可达性、不变性和平均收益等问题，并给出概念验证实现。它与岗位的认证式算法直接相连，也引出证书规模和检查成本的问题。不能把原型结果直接视为新课题模型的扩展性保证。Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes
• 《Foundations of probability-raising causality in Markov decision processes》，Baier、Piribauer、Ziemek，Logical Methods in Computer Science，20(1)，2024 年第 4 篇。论文以提高结果发生概率来定义因果关系，从状态集合推广到正规路径性质，并研究判定、存在性及按召回率、覆盖率、f-score 寻优的复杂性。这项工作为解释赋予明确的形式化语义；判断因果关系时，仍以给定模型为前提。Foundations of probability-raising causality in Markov decision processes
• 《Formal Quality Measures for Predictors in Markov Decision Processes》，Baier、Klüppelholz、Piribauer、Ziemek，AAAI 2025，39(25)，26760—26768。论文对无记忆策略下的预测质量取平均，也考察预测器在多少策略下构成提高结果概率的原因。它连接预测与解释质量。无记忆策略的假设不能直接推广到任意依赖历史的控制，也不能等同于真实机器学习系统的预测准确率。Formal Quality Measures for Predictors in Markov Decision Processes

这些结论受所引预印本、学校记录与出版方摘要的范围约束，不代表已复现实验或逐项完成证明与代码审计。三篇论文说明方向匹配；新博士题目的独立创新点还需与导师讨论。

领域前景与职业去向

形式化方法已有明确工业应用。Amazon 的 ICSE 2025 论文介绍了用 Dafny 编写、编译为 Java 的授权引擎，该系统于 2024 年部署，验证过程也使用差分测试和影子测试。其 2025 年秋季自动推理研究征集涉及模型检测、程序逻辑、分布式协议和随机算法。这些材料能说明工业界持续关注相关方法，但不能用来推算当前岗位数量或 TUD 毕业生就业率，也不代表这个博士有对应企业合作。2025 年征集已经结束。Formally verified cloud-scale authorization Amazon Automated Reasoning research priorities,Fall2025

博士训练可积累证明、概率推理、算法设计和验证工具能力，适用方向包括研究岗位、安全与可靠性软件，以及需要形式化保证的软件工程。若希望拓宽工业选择，需要能解释证明的假设，并把方法落到可维护代码和现实基准。纯理论方向可选择的岗位通常更集中，博士学历本身也不能替代生产软件经验。现有资料不能给出工资溢价、就业率或当前招聘数量。

资助、费用与生活条件

这是雇佣岗位。招聘注明按个人条件适用 E13 TV-L，拟聘期为 2027 年 1 月 1 日至 2030 年 12 月 31 日，适用德国科研固定期限合同制度 WissZeitVG。工时比例、工资档次、税后收入及单独的费用承担方案未公布。经费条件需要书面确认，因为已有TRR248资料仅介绍至2026年的第二资助期，现有材料未独立确认2027—2030年续资。这是需要核实的资金条件，不能据此认定招聘已取消。岗位提供按每周工作 5 天计算的每年 30 天年假、补充养老计划及弹性工时；面试费用不报销。TUD official vacancy13027: Research Associate/PhD Student/PostDoc TRR248 Center for Perspicuous Computing Graduate Academy: financing doctoral studies

TUD 的 2026—2027 年国际交流资料给出的学生生活预算约为每月 900 欧元，其中住宿约每月 230—500 欧元，学期缴费约350 欧元，含交通。它只能用作生活成本参照，不能当作受雇博士的实际支出。应确认所选注册路径是否缴纳学期费用，个人是否能申请学生宿舍，并另查私人租房、押金、水电及保险税费。Studentenwerk 住宿要申请，也受资格与房源限制。尚无工时比例和税后工资，不能据此承诺结余。TUD2026–2027 factsheet: living costs Studentenwerk Dresden accommodation

背景要求、国内申请资格与提交方式

官方必备条件：计算机或相关学科大学学位，扎实的理论计算机基础，很好的数学基础，能够有条理地独立推进项目，并具备协作沟通和优秀的英语书面、口头表达能力。官方优先或理想条件：验证、自动机理论和逻辑背景；良好的编程能力与实验任务兴趣属于理想条件。招聘没有要求申请者具备全部优先方向，也没有指定语言、德语能力或英语考试分数。博士入学的学历要求仍需单独满足。

准备建议：用一个证明或算法项目说明假设、复杂性和你的实际贡献，并解释如何检验实现。再选一篇团队论文，提出一个范围清楚的问题，比单列软件名称更有帮助。这些是展示能力的建议，不是额外准入条件。如果主要兴趣是应用机器学习，又不喜欢数学证明，日常研究可能并不合适。

国内申请者原则上可以申请，但有条件。TUD 提供国际雇员支持，学院有境外学历认定流程；德国官方也说明，第三国博士在研究机构劳动合同下开展论文工作，可按研究居留路径办理。岗位未列出国籍排除条件。个人仍需通过学历认定、雇佣和适用的签证或居留审核；纯全日制学位项目与雇佣博士的居留路径不同，应让学校人事和 Welcome Center 确认分类。最终能否录用、入学和获批签证，仍以个人审核结果为准。TUD: international employees and researchers DRESDEN-concept Welcome Center German federal information: research residence and doctoral candidates

申请截止为 2026 年 10 月 30 日，须提交通常所需材料，合为一份 PDF，优先通过 TUD SecureMail 发至 professur-alg@tu-dresden.de。以大学中央收件服务的到件戳或 TUD 邮件服务器时间戳为准。邮寄可寄至 Prof. Dr. Christel Baier，教研组地址 Helmholtzstr.10，01069 Dresden，Germany。可以准备动机信、简历、学历和成绩证明作为常规材料；官方招聘没有另定研究计划或推荐人数。提交时仍应按最新官方说明操作。TUD official vacancy13027: Research Associate/PhD Student/PostDoc

下一步与待确认问题

申请前先问清工时比例、经费条件和续资进展，并确认个人学历适用哪条博士路径。材料可以同步准备；精确税后收入应在工资条件确定后核算。

面试时重点讨论第一年的数学问题、模型范围和相对近年论文的创新点。再确认日常与第二导师、实现及工具维护任务、基准和计算资源，以及拟证结论或扩展方案不成立时如何调整研究。

接受前应取得书面合同及工资依据，明确资助比例、期限与续聘条件，确认论文时间和教学或项目任务如何分配，并核实注册、住房及抵达费用。签证办理时间也要与计划的 1 月入职衔接。

证据与来源

核心机构与培养

• TUD official vacancy13027: Research Associate/PhD Student/PostDoc
• TUD Chair of Algebraic and Logical Foundations
• TRR248 Center for Perspicuous Computing
• Perspicuous computing research framework
• Faculty of Computer Science doctoral admission and procedure
• TUD report on QS World University Rankings2027
• TUD: international employees and researchers
• DRESDEN-concept Welcome Center
• Graduate Academy qualification and career support

导师与论文

• Christel Baier official academic profile
• Christel Baier institutional publication list
• Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes
• Foundations of probability-raising causality in Markov decision processes
• Formal Quality Measures for Predictors in Markov Decision Processes

资助、成本与职业

• TUD2026–2027 factsheet: living costs
• Graduate Academy: financing doctoral studies
• Studentenwerk Dresden accommodation
• Formally verified cloud-scale authorization
• Amazon Automated Reasoning research priorities,Fall2025
• German federal information: research residence and doctoral candidates