스탠퍼드 연구진은 인과추론 이론 연구를 자동화하는 에이전트형 파이프라인 CausalSmith를 구축했습니다. 시스템은 연구 결과를 제안하고 언어 모델 검토자가 확인한 뒤, Lean 4(정리를 형식 논리로 검증하는 증명 도구)로 증명을 형식화합니다. 이어 대화형 웹페이지와 슬라이드 자료를 포함한 논문을 만듭니다. 기반 라이브러리 Causalean에는 통계와 인과추론 분야의 Lean 검증 정의·정리가 1만 5,000건 넘게 담겨 있습니다.

CausalSmith는 발견, 형식화, 발표의 세 단계로 작동합니다. 발견 단계에서 에이전트가 결과와 자연어 증명을 제안하면 다른 에이전트가 정확성과 참신성을 검토합니다. Lean이 증명을 검사하고, 별도의 감사 과정은 형식화된 명제와 논문의 가정·결론이 일치하는지 살펴 정리가 실제 주장보다 약해지는 문제를 찾습니다. 마지막 단계에서는 사람이 읽을 수 있는 논문과 대화형 페이지, 20분 분량의 발표 자료를 생성합니다.

연구진은 이 절차를 이산 교란 아래 평균 처치 효과를 추정하는 사례로 설명했습니다. Zeng 연구진이 2024년 논문에서 하한을 제시했지만, 그 하한에 도달하는 추정량이 있는지는 미해결 문제로 남았습니다. CausalSmith는 간극을 메우고 미니맥스 수렴률(최악의 경우에도 달성 가능한 최적 수렴 속도)을 달성하는 추정량을 제안했습니다. Lean 증명을 완성하기 위해 파이프라인은 Lean의 표준 수학 라이브러리인 Mathlib에 없던 무작위 계수의 집중 부등식을 증명하고 Causalean에 추가했습니다. 연구진은 사례 논문을 직접 확인했으며, 인과추론에 앞서 적용되지 않았던 증명 기법을 발견했다고 밝혔습니다.

2026년 10월 기준 연구팀은 CausalSmith를 1,732회 실행했습니다. 이 가운데 41회, 즉 2.4%가 정확하고 Lean 증명이 완성됐으며 각 실행에 설정된 검토 기준상 충분히 참신하다고 승인됐습니다. 수학적으로는 맞지만 진전이 제한적이라는 평가를 받아 1,388회는 하향 평가됐고, 제안이나 수학적 내용이 거부된 303회는 실패했습니다. 세 유형의 실행 결과는 실행 기록 저장소에 보관돼 후속 실행이 이전 시도를 참고합니다. 재사용할 수 있는 보조정리와 정리는 일반화와 검토를 거쳐 Causalean에 추가되며, 같은 문제에 대한 후속 승인 결과는 앞서 만든 집중 부등식을 다시 증명하지 않고 활용했습니다.

연구진은 Mathlib에 인과추론 자료가 거의 없어 Causalean을 만들었습니다. 문헌에서 자주 쓰이는 결과를 골라 언어 모델의 도움으로 정리하고 형식화한 뒤, 각 명제를 사람이 검토했습니다. 후속 실행도 언어 모델 검토를 거쳐 누락된 고전적 결과를 추가할 수 있습니다. 라이브러리는 인과 그래프, 잠재 결과, 구조적 인과 모형, 추정, 실험, 패널 데이터를 포함하며, 검토자는 항목이 출처와 일치하는지, 재사용 가능한지, 내용이 공허하지 않은지도 확인합니다. 프로젝트 페이지에서는 논문에 평점과 의견을 남기고, 개별 명제를 인증하며, 자연어 정의·정리를 감사된 Lean 버전과 비교할 수 있습니다. 참신성 검토와 Lean 검증을 통과한 논문에는 DOI와 인용 정보가 부여됩니다.

연구진은 2026년 10월 기준 생성된 논문 가운데 일부만 직접 검토해 전체 품질은 아직 알 수 없다고 밝혔습니다. 현재 프로젝트 페이지의 평점, 인증, 의견이 사람의 판단을 모으는 주요 수단입니다. 연구진은 더 체계적인 참신성 측정법과 언어 모델의 독창적 연구 수행 능력을 평가할 벤치마크를 향후 과제로 제시했습니다.

스탠퍼드 연구진은 인과추론 이론 연구를 자동화하는 에이전트형 파이프라인 CausalSmith를 구축했습니다. 시스템은 연구 결과를 제안하고 언어 모델 검토자가 확인한 뒤, Lean 4(정리를 형식 논리로 검증하는 증명 도구)로 증명을 형식화합니다. 이어 대화형 웹페이지와 슬라이드 자료를 포함한 논문을 만듭니다. 기반 라이브러리 Causalean에는 통계와 인과추론 분야의 Lean 검증 정의·정리가 1만 5,000건 넘게 담겨 있습니다.

CausalSmith는 발견, 형식화, 발표의 세 단계로 작동합니다. 발견 단계에서 에이전트가 결과와 자연어 증명을 제안하면 다른 에이전트가 정확성과 참신성을 검토합니다. Lean이 증명을 검사하고, 별도의 감사 과정은 형식화된 명제와 논문의 가정·결론이 일치하는지 살펴 정리가 실제 주장보다 약해지는 문제를 찾습니다. 마지막 단계에서는 사람이 읽을 수 있는 논문과 대화형 페이지, 20분 분량의 발표 자료를 생성합니다.

연구진은 이 절차를 이산 교란 아래 평균 처치 효과를 추정하는 사례로 설명했습니다. Zeng 연구진이 2024년 논문에서 하한을 제시했지만, 그 하한에 도달하는 추정량이 있는지는 미해결 문제로 남았습니다. CausalSmith는 간극을 메우고 미니맥스 수렴률(최악의 경우에도 달성 가능한 최적 수렴 속도)을 달성하는 추정량을 제안했습니다. Lean 증명을 완성하기 위해 파이프라인은 Lean의 표준 수학 라이브러리인 Mathlib에 없던 무작위 계수의 집중 부등식을 증명하고 Causalean에 추가했습니다. 연구진은 사례 논문을 직접 확인했으며, 인과추론에 앞서 적용되지 않았던 증명 기법을 발견했다고 밝혔습니다.

2026년 10월 기준 연구팀은 CausalSmith를 1,732회 실행했습니다. 이 가운데 41회, 즉 2.4%가 정확하고 Lean 증명이 완성됐으며 각 실행에 설정된 검토 기준상 충분히 참신하다고 승인됐습니다. 수학적으로는 맞지만 진전이 제한적이라는 평가를 받아 1,388회는 하향 평가됐고, 제안이나 수학적 내용이 거부된 303회는 실패했습니다. 세 유형의 실행 결과는 실행 기록 저장소에 보관돼 후속 실행이 이전 시도를 참고합니다. 재사용할 수 있는 보조정리와 정리는 일반화와 검토를 거쳐 Causalean에 추가되며, 같은 문제에 대한 후속 승인 결과는 앞서 만든 집중 부등식을 다시 증명하지 않고 활용했습니다.

연구진은 Mathlib에 인과추론 자료가 거의 없어 Causalean을 만들었습니다. 문헌에서 자주 쓰이는 결과를 골라 언어 모델의 도움으로 정리하고 형식화한 뒤, 각 명제를 사람이 검토했습니다. 후속 실행도 언어 모델 검토를 거쳐 누락된 고전적 결과를 추가할 수 있습니다. 라이브러리는 인과 그래프, 잠재 결과, 구조적 인과 모형, 추정, 실험, 패널 데이터를 포함하며, 검토자는 항목이 출처와 일치하는지, 재사용 가능한지, 내용이 공허하지 않은지도 확인합니다. 프로젝트 페이지에서는 논문에 평점과 의견을 남기고, 개별 명제를 인증하며, 자연어 정의·정리를 감사된 Lean 버전과 비교할 수 있습니다. 참신성 검토와 Lean 검증을 통과한 논문에는 DOI와 인용 정보가 부여됩니다.

연구진은 2026년 10월 기준 생성된 논문 가운데 일부만 직접 검토해 전체 품질은 아직 알 수 없다고 밝혔습니다. 현재 프로젝트 페이지의 평점, 인증, 의견이 사람의 판단을 모으는 주요 수단입니다. 연구진은 더 체계적인 참신성 측정법과 언어 모델의 독창적 연구 수행 능력을 평가할 벤치마크를 향후 과제로 제시했습니다.