Zhiheng Zhang（张智恒）

Zhiheng Zhang（张智恒）

I am an interdisciplinary researcher primarily focusing on causal inference.

CAUSAL Lab 开源研究项目申请问卷与入组考核

CAUSAL LAB · OPEN-SOURCE RESEARCH

开源研究项目申请问卷与入组考核

本页介绍 Causal Foundation Model / Causal ATLAS 和 DesignInfer：design-based inference 的 Lean 形式化 两个开源研究方向。考核重点是能否把一个研究问题做成可运行、可复现、可检查的小型项目；篇幅、模型规模和代码量本身不是评价标准。

负责人：张智恒 单位：上海财经大学统计与数据科学学院 · CAUSAL Lab 版本：2026-09-20
使用方式：请填写并提交申请考核问卷。
Track A统计 + 机器学习Python / R

Causal Foundation Model

围绕因果表格模型，完成一个处理多来源实验与观测数据的小型原型，并用它进行效果评估、跨环境迁移和后续实验选择。需要说明任务定义、比较基线、验证方法和失效情形。

Track B形式化数学Lean 4

DesignInfer

选择 design-based inference 中的一项定义、引理或定理，将其形式化为可复用的 Lean API，并提交通过内核检查的证明，同时说明依赖关系和资料来源。

一、考核目的与流程

本问卷用于了解申请人与项目是否合适，也让申请人提前了解实际工作内容。提交的材料只用于评估和后续讨论；未经沟通，不会直接并入项目。

二、第一部分：开源项目申请问卷

请用中文或英文简要回答以下问题：

基本信息姓名、学校/单位、院系与专业、年级、所在城市、邮箱、个人主页或 GitHub。申请博士生、硕士生、科研助理还是研究实习？
可投入时间预计开始时间、持续周期、每周稳定投入小时数；未来六个月已知的课程、考试、实习或其他冲突是什么？
方向选择选择 Track A 或 Track B。你为什么对它感兴趣？它与你未来两年的学习或研究目标如何连接？
代表性工作最多列两项最能说明能力的项目。分别写清问题、你本人完成的部分、可核验产出，以及他人/AI 的实质贡献。
基础能力说明你在概率统计、线性代数、优化、因果推断、机器学习、软件工程或形式化证明方面的基础。
协作方式你希望独立负责、结对协作还是参与较大模块？
希望我们了解的其他信息可以是特殊经历、资源限制、无障碍需求，或你希望在讨论中重点了解的问题。

三、第二部分：方向考核

共同原则。请选择一个范围较小、能够独立完成的个人 project。可以使用生成式 AI、开源库和公开数据，但需要保留关键使用记录、核验输出，并能解释每一项核心设计。本考核评估的是申请人本人的兴趣、判断和能力，不要求申请人无偿完成一个完整产品或大规模研究工程。

Track A：Mini Causal Foundation Model / Causal ATLAS

任务：构建一个最小的 evidence-to-estimation & decision 原型。在公开或合成数据上，把多来源/多环境证据组织为统一任务，比较至少三种候选处理、模型、提示词或策略，输出效应或价值的估计、排序、不确定性与下一步实验建议。

A1. 最小输入与输出

  • 至少两个数据来源或环境；允许使用“合成数据 + 公开数据”。
  • 明确数据、treatment、outcome、context、estimand / policy value、识别假设与可能的偏差来源。
  • 输出可以包括：候选方案排序、效应/价值估计、不确定性、在何种条件下应 abstain，以及一个具有明确预算的 bridge experiment / next experiment 建议。
  • 不要求训练大参数模型。可以采用预训练表格模型、元学习模型、检索/路由模块或简单共享骨干；需要说明它为何可以作为“跨任务/跨环境”原型，而不是单一数据集拟合器。

A2. 必须包含的系统模块

模块最低要求要回答的问题
Problem / Evidence Card统一记录 treatment、outcome、context、source、design、assumption、ground truth 可用性。不同实验和观测证据何时可比较？
Task Generator生成或切分不少于三类任务/环境，并固定训练、验证、测试边界。模型是否只记住一个数据集？
Baselines一个仅预测相关性的 baseline、一个标准因果/统计 baseline、你的方法。方法相对基线的改进来自什么？
Verifier检查 estimand、输入范围、重叠性/支持集、数值稳定性与结果一致性。何时不应相信输出？
Uncertainty / Abstention提供区间、校准、集合预测或可解释的拒答规则。系统能否识别自己不可靠的判断？
Bridge Planner在固定预算下选择下一项最有价值的实验或采样动作。有限的在线数据预算应如何分配？

A3. 三层评测与失效实验

  1. Solver fidelity：在有真值的任务上检查效应、排序或策略价值是否正确。
  2. Transfer / open benchmark：在未见环境、分布漂移或 schema 变化下评估泛化，并与 baseline 比较。
  3. Decision quality：评估 bridge experiment 是否以更少预算降低决策错误、不确定性或 regret。

至少构造一种失效情形，例如严重 overlap 破坏、未观测混杂、错误 proxy、干扰、sim-to-real 偏移或 treatment 语义错配。检查系统能否报警或拒答；如果不能，需要解释原因。

Track B：DesignInfer 的 Lean 形式化

任务：从 design-based inference 中选择一组相互关联的定义、引理和定理，完成规范化定义、依赖图和 Lean 4 实现，并给出资料来源及通过内核检查的证明。

B1. 推荐题目（任选一项）

  1. 完全随机化下差均值估计量的设计无偏性：有限总体、固定潜在结果和已知处理组规模。
  2. 概率空间的构造与经验过程：明确抽样空间、对称性与边界条件。
  3. 置换统计量或随机化检验的基本不变性/有限样本有效性：拓展到因果推断与实验设计。
  4. 其他题目可以自选。

B2. 必须包含的研究对象

  • Definition RFC：解释对象、索引、有限性、随机机制、估计量与符号约定；比较至少两个可能定义，并说明最终选择。
  • Statement fidelity：并列给出原始自然语言/数学命题、规范化命题和 Lean statement；逐项映射假设，不得偷换量词、增加隐含条件或弱化结论。
  • Dependency DAG：列出所需的 Mathlib/Statlib 结果、项目内定义、辅助引理和最终定理。
  • 边界测试：提供至少一个小规模可计算实例，以及一个说明某项假设不可删除的反例或失败尝试。
  • Problem Card：记录来源、假设、已知情形、形式化状态、尝试记录、阻塞点和可继续的开放问题。
如果 Lean 代码无法在锁定版本的环境中编译，或证明依赖占位符或新增公理，则视为未完成。如果发现原命题有误，可以提交经过验证的反例和修改建议，但必须清楚区分“原命题”“修订命题”和“已证明内容”。

四、统一功能与研究要求

  1. 任务规划：开始前提交工作分解，完成后对照原计划复盘。
  2. 真实执行：实验、数据处理、编译与测试必须实际运行；仅在文字中声称“已经运行”不算完成。
  3. 状态记录：保留关键输入、版本、命令、输出、错误、修复和决策理由，使过程可追溯。
  4. 独立验证：不能把“程序没有报错”当作正确性证明；应提供基线、单元测试、真值检查、反例、审查或其他独立验证依据。
  5. 停止条件：明确时间和算力预算、成功条件、未解决项及停止原因。
  6. 可复现性：锁定依赖和随机种子（如适用），提供一个从安装到生成主要结果的主命令。
  7. 最小化：只提交支持研究结论的必要组件。界面美化、复杂框架和无关功能不会自动加分。

五、提交材料

材料具体要求
申请问卷回答第二部分之前先提交第一部分。
完整代码Git 仓库或压缩包；包含源代码、配置、依赖锁定、测试和必要的最小数据。不要提交密钥或受限数据。
README环境、安装、目录结构、输入输出、主命令、预计运行时间、硬件需求、许可证与已知限制。
技术报告不超过 6 页。包括问题、假设、方法、基线、结果、失败案例、限制与下一步；正文不要复制运行日志。
运行记录至少一次从干净环境开始的完整记录。Track A 包括实验指标和生成物；Track B 包括 Lean/Lake 版本与完整构建结果。
AI 使用说明AI_USE.md：列出使用的模型/工具、日期、用途、关键 prompt 或 agent 任务、采纳内容、人工核验和被否决的建议。普通补全无需逐字记录。
来源与许可SOURCES.md 或报告附录：数据、论文、代码与图片来源；注明许可证、改动和直接复用范围。

建议压缩包命名：Name_University_CTFM.zip 或 Name_University_DesignInfer.zip。如使用 Git 仓库，请提交固定 commit 链接。

六、评价标准

以下情况不进入评分：伪造结果或日志；抄袭/洗稿；直接复制完整项目只改名称或少量提示词；提交自己无法解释的主要代码或数学论述；隐瞒他人/AI 的实质贡献；泄露密钥、个人数据或未授权材料；Lean 证明使用占位符或通过改变命题规避任务。

七、允许与禁止事项

允许并鼓励

  • 使用公开数据、合成数据、开源库、预训练模型和形式化证明工具。
  • 使用生成式 AI 辅助阅读、编码、调试、证明搜索和写作。
  • 缩小题目、报告失败、提交负结果或经验证的反例。
  • 在 README 中说明资源限制，并提供资源要求较低的复现方法。
  • 在遇到命题或数据问题时尽早提出。

禁止

  • 伪造实验、编译、工具调用、引用或人工审查记录。
  • 提交未理解、不能担保正确性的 AI 生成内容。
  • 未经许可公开内部材料、未发布想法或合作方数据。
  • 把 API Key、密码、Cookie 或个人敏感信息提交到仓库。
  • 用界面或宣传包装代替问题定义、验证和可复现证据。

八、提交方式

请发送至 zhangzhiheng@mail.shufe.edu.cn。邮件标题建议为：

[CAUSAL Open-source Project Application] 姓名 - CTFM / DesignInfer - 学校

正文请包含：申请身份、选择方向、问卷链接、固定 commit/压缩包链接、可复现主命令和你希望优先讨论的一个问题。完成期限以邀请邮件为准；如遇不可控延迟，请在截止前说明当前状态、已完成产出和新的预计时间。

九、常见问题

一定要有因果推断或 Lean 经验吗？

不一定。数学或统计基础扎实、编程能力较强且愿意快速学习的同学也可以申请。没有相关经验的申请人，可以在完成基础入门后使用大模型辅助学习。

必须用深度模型或 Agent 框架吗？

不需要。对新手而言，一个过程透明、基线充分的轻量原型，往往比难以解释的大模型更有价值。

Lean 题太难，能只写数学证明吗？

不能作为完成 Track B 的替代。可以先提交数学证明和形式化计划请求讨论，但正式考核必须包含内核检查通过的 Lean 代码，或经核验的反例与问题报告。

可以和别人合作完成吗？

可以讨论或使用公开社区资源，但考核默认评估个人能力。必须逐项说明他人贡献；技术讨论中需要独立解释自己提交的部分。

十、参考文献

Track A：Causal Foundation Model / Causal ATLAS

论文

  1. Noah Hollmann, Samuel Müller, Lennart Purucker, Arjun Krishnakumar, Max Körfer, Shi Bin Hoo, Robin Tibor Schirrmeister, and Frank Hutter. (2025). Accurate predictions on small data with a tabular foundation model. Nature, 637, 319–326. DOI: 10.1038/s41586-024-08328-6.
    DOI / 论文
  2. Vahid Balazadeh, Hamidreza Kamkari, Valentin Thomas, Benson Li, Junwei Ma, Jesse C. Cresswell, and Rahul G. Krishnan. (2025). CausalPFN: Amortized Causal Effect Estimation via In-Context Learning. arXiv:2506.07918 [cs.LG], version 2, revised 27 October 2025. DOI: 10.48550/arXiv.2506.07918.
    arXivDOI代码
  3. Jiaqi Zhang, Joel Jennings, Agrin Hilmkil, Nick Pawlowski, Cheng Zhang, and Chao Ma. (2023). Towards Causal Foundation Model: on Duality between Causal Inference and Attention. arXiv:2310.00809 [cs.LG], version 3, revised 3 June 2024. DOI: 10.48550/arXiv.2310.00809.
    arXivDOI

相关 Workshop：Foundation Models for Structured Data 中的因果研究

  1. CausalTab: Pretraining Across Causal Environments for Tabular Causal Discovery.
    Zi-Rong Li, Si-Yang Liu, Tian-Zuo Wang, and Han-Jia Ye.
  2. Synthetic Causal Priors for In-Context Time-Series Classification.
    Hao-Run Cai and Han-Jia Ye.
  3. Foundation Models for Partial Causal Identification.
    Alexis Bellot and Anish Dhir.
  4. Towards Continuous-time Causal Foundation Models.
    Dennis Thumm, Ruben Wiedemann, and Ying Chen.
  5. Causal Foundation Models Perform Better without Post-treatment Variables.
    Junha Ham, Deokgyu Kim, Doeun Kim, Serjin Kim, and Sanghack Lee.
  6. Inducing Causal Order through Tabular In-Context Learning.
    Sascha Xu, Sarah Mameche, and Jilles Vreeken.
  7. FairOpt-PFN: Amortized Counterfactual Fairness with Optimal Fair Targets.
    Enes Hasani, Jake Robertson, and Frank Hutter.
  8. Where Computation Lives Inside TabPFN: Causal Localisation of Attention Head Function.
    Atharva Gupta, Dhruv Kumar, Murari Mandal, and Saurabh Deshpande.
  9. A Causal Foundation Model for Structure and Outcome Prediction.
    Max Zhu, Martino Mansoldo, Chinghao Wang, and Stefan Groha.
  10. Causal Foundation Models with Continuous Treatments.
    Christopher Stith, Medha Barath, Vahid Balazadeh, Jesse Cresswell, and Rahul G. Krishnan.
  11. Causal Foundation Models for Time Series based on Prior-Data fitted Networks.
    Dennis Thumm, Arik Reuter, Jake Robertson, Shi Bin Hoo, Adrian Weller, Frank Hutter, Ying Chen, and Bernhard Schölkopf.
  12. Implicit Reward Alignment For Training Causally-Coherent Tabular Data Generators.
    Matea Gjika, Giuseppe Iannone, Luca Sfragara, Pavithra Harsha, and Georgia Perakis.
  13. A Causal DAG Prior for Synthetic Time-Series Classification Datasets.
    Franco Martino ORourke, Ana Trisovic, and Dimitris Bertsimas.
  14. SCBench: A Testbed for Causal Inference with Time Series Panel Data.
    Megan Richards, Saeyoung Rho, and Kyunghyun Cho.
  15. DataSynK: Causal-Symbolic EHR Synthesis for Tabular Foundation Models in Low-Resource Settings.
    Eduarda Chagas, Roberta Viola, Juarez Monteiro, Francisco Galuppo Azevedo, Saulo F. Saturnino, and Adriano Veloso.
  16. Bayesian Tabular Few-shot Learning with Causal Information.
    Ole Ossen, Jake Robertson, Arik Reuter, Magnus Bühler, Lennart Purucker, and Frank Hutter.

Track B：DesignInfer / Lean 形式化验证

  1. 会议论文 / Lean 软件库 Yuanhe Zhang, Jason D. Lee, and Fanghui Liu. (2026). AI4SLT: Empirical Processes in Lean 4 for Formal Statistical Learning Theory. In Forty-third International Conference on Machine Learning (ICML 2026). arXiv:2602.02285. DOI: 10.48550/arXiv.2602.02285.
    ICML / OpenReviewarXiv 摘要PDFDOILean 4 代码
  2. Lean 软件库 Shuangping Li and Peng Zhang (maintainers). Language Generation in the Limit: A Lean Library and Paper Map. Lean 4 software repository, continuous development; accessed 18 August 2026. Apache-2.0 license.
    GitHub 仓库
  3. 开源实验室 Marin Contributors. Marin: Developing Models Together, Openly. Open-source foundation-model laboratory and experiment platform; accessed 18 August 2026.
    项目主页GitHub 仓库
  4. Lean 项目模板 Self-Evolving. Lean Workspace: A Shared Workspace Where Human Teams and AI Agents Collaborate to Write Proofs Together. Lean 4 project template, continuous development; accessed 18 August 2026.
    GitHub 模板文档
  5. 讲义 / 预印本 Fang Han. (2024). An Introduction to Permutation Processes (version 0.5). arXiv:2407.09664 [math.ST], 193 pages. DOI: 10.48550/arXiv.2407.09664.
    arXiv 摘要PDFDOI
  6. 社区与统计库 Lean Prover Community / Statlib Contributors. Statlib community channel and library resources. Community discussion and Lean 4 library resources; accessed 18 August 2026.
    Statlib Zulip 频道Statlib 项目主页Statlib GitHub