이론적 연구를 자동화하는 것은 후보 결과의 생성뿐만 아니라, 그 결과에 대한 신뢰할 수 있는 평가에 의해서도 제약을 받습니다. 일반적인 접근 방식은 대규모 언어 모델 (LLM) 리뷰어를 통해 연구 루프를 닫는 것입니다. 그러나 이러한 리뷰어들은 경험적으로 여전히 신뢰할 수 없습니다. 이들은 조작된 논문을 수락하거나, 우연에 가까운 확률로 이를 탐지할 수 있습니다 (Bad Scientist, 2025). 우리는 Lean 증명 보조 도구 (proof assistant)에 기반을 둔 인과 추론 (causal inference) 분야의 자동화된 이론 연구를 위한 프레임워크인 CausalForge를 제시합니다. CausalForge는 인간의 설계 및 검토 하에 언어 모델의 도움을 받아 개발된 7,035개의 기계 검증된 선언 (machine-checked declarations)을 포함하는 인과 추론을 위한 기초 Lean 라이브러리인 Causalean과, 연구 주제를 선택하고, 결과를 제안하며, 문장을 형식화하고, 증명을 구성하며, 결과물을 인간의 검토를 위해 제시하는 자기 개선형 에이전트 파이프라인인 CausalSmith를 결합합니다. 기계 검증된 증명은 형식적 문장이 가정으로부터 도출된다는 것만을 확립할 뿐, 그 문장이 의도된 과학적 주장을 충실히 포착한다는 것을 보장하지 않기 때문에, 이 파이프라인은 커널 검증 (kernel verification)을 각 형식적 정리를 그것이 표현하고자 하는 비형식적 주장과 비교하는 문장 감사 (statement audit)로 보강합니다. 우리는 완료된 자율 연구 실행에 의해 생성된 결과물을 사용하여 시스템을 평가합니다. 소스 코드, 형식 라이브러리 및 실행 기록은 https://github.com/Jiyuan-Tan/CausalForge 에서 확인할 수 있습니다.