CAUSAL LAB · OPEN-SOURCE RESEARCH
开源研究项目申请问卷与入组考核
面向 Causal Foundation Model / Causal ATLAS 与 DesignInfer：design-based inference 的 Lean 形式化 两个开源研究方向。考核关注能否把研究问题转化为可运行、可复现、可审查的研究对象，无需堆砌篇幅、模型规模或代码行数。
使用方式。请提交本申请考核问卷；
Causal Foundation Model
围绕因果表格模型，构建从多源实验与观测证据到评估、迁移和下一步实验决策的最小原型。给出可信的任务定义、基线、验证和失效分析。
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. 三层评测与失效实验
- Solver fidelity：在有真值的任务上检查效应、排序或策略价值是否正确。
- Transfer / open benchmark：在未见环境、分布漂移或 schema 变化下评估泛化，并与 baseline 比较。
- Decision quality：评估 bridge experiment 是否以更少预算降低决策错误、不确定性或 regret。
至少主动构造一种失效情形，例如严重 overlap 破坏、未观测混杂、错误 proxy、干扰、sim-to-real 偏移或 treatment 语义错配。展示系统是否能报警/拒答；若不能，解释原因。
Track B：DesignInfer 的 Lean 形式化
任务：从 design-based inference 中选一个定义-引理-定理的最小闭环，给出来源、规范化定义、依赖图、Lean 4 实现与内核检查通过的证明。
B1. 推荐题目（任选一项）
- 完全随机化下差均值估计量的设计无偏性：有限总体、固定潜在结果和已知处理组规模。
- 不放回抽样的有限总体均值/方差恒等式：明确抽样空间、对称性与边界条件。
- 置换统计量或随机化检验的基本不变性/有限样本有效性：难度较高，需提前控制命题范围。
- 其他题目可以自选
B2. 必须包含的研究对象
- Definition RFC：解释对象、索引、有限性、随机机制、估计量与符号约定；比较至少两个可能定义，并说明最终选择。
- Statement fidelity：并列给出原始自然语言/数学命题、规范化命题和 Lean statement；逐项映射假设，不得偷换量词、增加隐含条件或弱化结论。
- Dependency DAG：列出所需的 Mathlib/Statlib 结果、项目内定义、辅助引理和最终定理。
- 边界测试：提供至少一个小规模可计算实例，以及一个说明某项假设不可删除的反例或失败尝试。
- Problem Card：记录来源、假设、已知情形、形式化状态、尝试记录、阻塞点和可继续的开放问题。
若 Lean 代码不能在锁定版本的环境中编译，或证明依赖占位符/新增公理，视为未完成。若发现原命题有误，可以提交经验证的反例和修订建议，但必须清楚区分“原命题”“修订命题”和“已证明内容”。
四、统一功能与研究要求
- 任务规划：提交开始前的工作分解，以及完成后对原计划的复盘。
- 真实执行：实验、数据处理、编译与测试必须真实运行；只在文字中模拟“已经运行”不算完成。
- 状态记录：保留关键输入、版本、命令、输出、错误、修复和决策理由，使过程可追溯。
- 独立验证：不能把“程序没有报错”当作正确性证明；应有基线、单元测试、真值检查、反例、审查或等价的独立信号。
- 终止条件：明确时间/算力预算、成功条件、未解决项和停止原因。
- 可复现性：锁定依赖和随机种子（如适用），提供从安装到生成主要结果的一条主命令。
- 最小化：只提交支持研究结论的必要组件。界面美化、复杂框架和无关功能不会自动加分。
五、提交材料
| 材料 | 具体要求 |
|---|---|
| 申请问卷 | 回答第二部分之前先提交第一部分。 |
| 完整代码 | 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
论文
- 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.
- 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.
- 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.
参考相关Workshop：Foundation Models for Structured Data 中的因果相关工作
- CausalTab: Pretraining Across Causal Environments for Tabular Causal Discovery.
- Synthetic Causal Priors for In-Context Time-Series Classification.
- Foundation Models for Partial Causal Identification.
- Towards Continuous-time Causal Foundation Models.
- Causal Foundation Models Perform Better without Post-treatment Variables.
- Inducing Causal Order through Tabular In-Context Learning.
- FairOpt-PFN: Amortized Counterfactual Fairness with Optimal Fair Targets.
- Where Computation Lives Inside TabPFN: Causal Localisation of Attention Head Function.
- A Causal Foundation Model for Structure and Outcome Prediction.
- Causal Foundation Models with Continuous Treatments.
- Causal Foundation Models for Time Series based on Prior-Data fitted Networks.
- Implicit Reward Alignment For Training Causally-Coherent Tabular Data Generators.
- A Causal DAG Prior for Synthetic Time-Series Classification Datasets.
- SCBench: A Testbed for Causal Inference with Time Series Panel Data.
- DataSynK: Causal-Symbolic EHR Synthesis for Tabular Foundation Models in Low-Resource Settings.
- Bayesian Tabular Few-shot Learning with Causal Information.
Track B：DesignInfer / Lean 形式化验证
- 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.
- 开源实验室 Marin Contributors. Marin: Developing Models Together, Openly. Open-source foundation-model laboratory and experiment platform; accessed 18 August 2026.
- 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.
- 讲义 / 预印本 Fang Han. (2024). An Introduction to Permutation Processes (version 0.5). arXiv:2407.09664 [math.ST], 193 pages. DOI: 10.48550/arXiv.2407.09664.
- 社区与统计库 Lean Prover Community / Statlib Contributors. Statlib community channel and library resources. Community discussion and Lean 4 library resources; accessed 18 August 2026.