CausalSmith：用于因果推理自动化研究的正式基础、自我改进的代理框架

自动化理论研究需要生成候选结果并对其进行可靠评估。模型在第一个阶段不断变得更好，而第二个阶段仍然很困难。一种常见的方法是要求一个 大语言模型 (LLM) 审查另一个人发表的内容，但这样的审稿人在经验上是不可靠的：他们可能会接受捏造的论文，并以接近偶然的概率抓住捏造的论文~\citep{badscientist2025}。我们提出了 \textsc{CausalSmith}，这是一个基于精益证明助手的因果推理自动化理论研究框架，其中证明由程序检查，而不是由裁判阅读。 \textsc{CausalSmith} 依赖于 \textsc{Causalean}，这是一个用于因果推理的基础精益库，包含 8,179 个经过机器检查的定义和定理，是在人工设计和审查下通过语言模型辅助开发的。围绕它，我们建立了一个自我改进的代理管道，用于选择研究主题、提出结果、形式化陈述、构建证明并呈现结果工件以供人工检查。此外，该管道将精益验证与语句审计结合起来，将每个正式定理与其背后的非正式主张进行比较。我们使用完成的自主研究运行产生的工件来评估系统。源代码、正式库和运行记录可在 https://github.com/Jiyuan-Tan/CausalSmith 获取。