📈 economics

CausalForge: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference

CausalForge는 Lean 기반의 Causalean 라이브러리와 증명을 생성, 형식화 및 감사하여 기계가 검증한 결과의 신뢰성을 보장하는 파이프라인을 결합함으로써 인과 추론 연구를 자동화하는, 형식적으로 근거를 둔 자기 개선형 에이전트 프레임워크입니다.

원저자: Jiyuan Tan, Vasilis Syrgkanis

게시일 2026-07-27

📖 3 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Jiyuan Tan, Vasilis Syrgkanis

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

당신이 인과관계에 관한 미스터리를 풀려는 탐정이라고 상상해 보세요. 당신은 다음과 같은 질문을 던지고 싶습니다. "내가 이 약을 먹으면 나을까?" 또는 "저 비가 실제로 홍수를 일으킨 걸까?" 과학의 세계에서 이것은 **인과 추론(causal inference)**이라고 불립니다. 이것은 단순히 어떤 일이 일어나는 것을 관찰하는 것과는 다릅니다. 무언가를 바꿨을 때 어떤 일이 일어날지를 알아내는 것에 관한 것입니다. 오랫동안 과학자들은 이러한 인과관계의 이야기를 사실로 증명하기 위해 수학을 사용해 왔습니다. 하지만 수학은 어렵고, 증명 과정에서의 아주 작은 실수 하나가 전체 이야기를 거짓으로 만들 수 있습니다.

최근 컴퓨터는 **대규모 언 모델(LLM)**이라 불리는 기술을 사용하여 이야기를 쓰고 퍼즐을 푸는 데 매우 능숙해졌습니다. 이들은 거의 모든 기록된 글을 읽고 자신만의 논문, 증명, 이론을 쓸 수 있는 초지능 로봇과 같습니다. 하지만 여기에는 함정이 있습니다. 이 로봇들은 자신감 있게 말하는 데는 뛰어나지만, 자신의 작업물을 스스로 검토하는 데는 형편없다는 점입니다. 이들은 종종 사실을 지어내거나, 숫자를 날조하거나, 겉보기에는 완벽해 보이지만 실제로는 말도 안 되는 증명을 써 내려가곤 합니다. 만약 우리가 로봇에게 과학 논문을 쓰게 하고, 또 다른 로봇에게 그것을 검토하라고 시킨다면, 그들은 내용이 완전히 틀렸음에도 불구하고 서로를 향해 "응, 맞아!"라고 고개를 끄덕이며 동조할지도 모릅니다. 이는 과학에서 매우 큰 문제입니다. 왜냐하면 틀린다는 것은 잘못된 결정으로 이어질 수 있기 때문입니다.

여기서 CausalForge라는 새로운 프로젝트가 등장합니다. CausalForge는 인과 추론 분야의 연구를 수행하도록 설계된 '자기 개선형 로봇 과학자'이며, 매우 엄격한 안전망을 갖추고 있습니다. 로봇이 다른 로봇의 숙제를 검사하는 것을 그냥 믿는 대신, CausalForge는 Lean이라는 마법 같고 깨뜨릴 수 없는 수학 도구(증명 보조기)를 사용합니다. Lean은 모든 단계가 논리적으로 완벽하지 않으면 결코 정답을 인정하지 않는 매우 엄격한 선생님과 같습니다. 만약 수학이 맞지 않는다면, Lean은 "안 돼!"라고 말하며 승인을 거부합니다.

하지만 두 번째 문제가 있습니다. 수학이 완벽하더라도, 로봇이 엉뚱한 것을 증명하고 있을 수도 있다는 점입니다. 예를 들어, 로봇이 완벽한 논리로 "모든 고양이는 개다"라는 것을 증명한다고 상상해 보세요. 수학적 논리는 타당하지만, 그 주장은 터무니없습니다. CausalForge는 **문장 감사(Statement Audit)**를 추가하여 이 문제를 해결합니다. 이것은 "로봇이 원래 증명하려고 했던 것을 실제로 증명했는가?"를 확인하는 번역기와 같습니다.

그렇다면 CausalForge는 실제로 무엇을 했을까요? 팀은 두 가지 주요 부분을 구축했습니다. 첫째, 그들은 Causalean이라는 거대한 라이브러리를 만들었는데, 여기에는 인과관계에 관한 7,000개 이상의 사전 검증된 완벽한 수학적 사실들이 포함되어 있습니다. 이는 모든 도구가 제대로 작동하는지 이미 테스트를 마친 거대한 공구 상자와 같습니다. 둘째, 그들은 CausalSmith라는 로봇 파이프라인을 구축했습니다. 이 로봇은 연구 주제를 선정하고, 새로운 정리를 고안하며, Lean 언어로 증명을 작성하고, 시스템이 그 증명이 실제인지 그리고 그 주장이 수학과 일치하는지 확인하도록 할 수 있습니다.

결과는 성공과 현실적인 점검이 섞여 있었습니다. 시스템이 새로운 것을 발견하기 위해 시도한 123번의 시도 중, 9번이 완전하게 수용되었으며, 이는 새롭고 기계적으로 검증된 것이었습니다. 시스템은 기존 연구의 작은 기술적 틈새(예: 공식의 아주 작은 오류를 수정하는 것)를 찾아내는 데는 놀라울 정도로 뛰어났지만, 완전히 새로운 거대한 아이디어를 무에서 유로 창조해 달라는 요청에는 어려움을 겪었습니다. 이 논문은 우리가 아직 로봇의 창의성을 완전히 신뢰할 수는 없더라도, 엄격한 '마법 선생님'(Lean)과 세심한 '번역가'(감사)가 지켜보고 있다면, 로봇이 수학을 쓰고 검증하는 힘든 작업을 수행하는 데는 신뢰할 수 있다는 것을 보여줍니다. 이것은 모든 과학 문제를 해결하는 마법 지팡이는 아니지만, 우리의 과학적 이야기가 실제로 참임을 보장하는 강력하고 새로운 방법입니다.

기술 요약: CausalForge

문제 정의

인과 추론(causal inference) 분야의 이론적 연구를 자동화하는 데 있어 핵심적인 병목 현상은 생성된 결과물의 신뢰할 수 있는 평가에 직면해 있다는 점이다. 대규모 언어 모델(LLM)은 추측, 증명, 논문을 빠르게 생성할 수 있지만, 스스로의 정확성을 평가하는 데는 어려움을 겪는다. 실증 연구에 따르면, LLM 검토자들은 신뢰할 수 없으며, 조작된 논문을 우연한 확률에 가까운 높은 비율로 수용하거나, 올바른 정리와 틀린 정리를 구분하지 못하는 경st를 보인다.

결과를 공식화(formalization)하는 것(예: Lean 4 증명 보조 도구 활용)에만 의존하는 것은 두 가지 이유로 불충분하다:

비용: 기초부터 결과를 공식화하는 것은 노동 집약적이다. 자동화된 발견을 위해서는 매 실행마다 표준 이론을 다시 구축하지 않도록 재사용 가능하고 검증된 정리 라이브러리가 필요하다.
충실도(Faithfulness): 기계가 확인한 증명은 공식적인 문장이 가정으로부터 논리적으로 도출됨을 보장하지만, 그 공식적인 문장이 의도한 과학적 주장을 충실하게 포착했음을 보장하지는 않는다. LLM은 공허한 정의(vacuous definition)로부터 타입 체크가 통과된 증명을 만들어내거나, 모순된 가설을 가진 정리, 또는 증명되지 않은 단계를 공리(axiom)로 대체한 결과를 생성할 수 있다.

방법론: CausalForge 프레임워크

CausalForge는 인과 추론의 이론적 연구를 자동화하기 위해 설계된 자기 개선형 에이전트 프레임워크이다. 이는 기초적인 형식 라이브러리와 증명의 건전성(soundness) 및 문장의 충실도(faithfulness)를 강조하는 다단계 파이프라인을 통합한다.

핵심 구성 요소

Causalean (라이브러리):
- 그래픽 모델, 구조적 인과 모델(SCM), 잠재적 결과(potential outcomes), 식별(identification), 점근적 통계(asymptotic statistics)를 다루는 7,035개의 기계 확인 선언(machine-checked declarations)을 포함하는 기초적인 Lean 4 라이브러리이다.
- 인간의 설계와 검토 하에 LLM의 도움을 받아 구축되었으며, 에이전트가 검증된 프리미티브(예: 백도어 조정, 이중 머신러닝 추정량)를 재사용할 수 있는 검색 인터페이스를 제공한다.
- 코어 라이브러리와 파이프라인 전용 레마(lemma) 사이의 엄격한 분리를 강제하여, 라이브러리가 피드백 루프를 통해 성장할 수 있도록 한다.
CausalSmith (파이프라인):
- 발견(Discovery), 공식화(Formalization), 증명 구축(Proof Construction), **제시(Presentation)**의 4단계를 실행하는 결정론적 상태 머신이다.
- 로직 그래프(Logic Graph): 중심 산물은 노드가 문장(정의, 레마, 정리)을 나타내고 엣지가 의존성을 나타내는 로직 그래프이다. 이 그래프는 게이트가 설정된 노드(증명되지 않은 기질)와 인용된 노드(빌려온 결과)의 "임계 경로(critical path)"를 추적한다.
- 발견: 연구 주제를 선택하며(사용자가 제공하거나 문헌의 공백에서 자율적으로 선택), 자연어 결과를 제안한다.
- 공식화 및 증명: 로직 그래프를 Lean 4 선언으로 매핑하고, Causalean 검색을 통해 증명 의무를 채우며 증명을 구축한다.
- 문장 감사(Statement Audit, 핵심 혁신): 공식적인 Lean 4 선언이 의도한 자연어 주장과 논리적으로 일치하는지 확인하는 전용 "문장 일치" 게이트이다. 여기에는 다음이 포함된다:
  - "증명되지 않은 지름길"(예: sorry, admit, 숨겨진 공리) 확인.
  - "공허함(vacuity)" 탐지(정의가 True로 축소되거나 만족 불가능한 가설을 갖는 경우).
  - 역번역(back-translation)을 통한 "충실도" 보장: 의도한 주장을 Lean 형태의 가설/결론 리스트로 변환한 뒤, 이를 공식 선언과 비교하여 논리적 동등성(더 강하거나 약하지 않음)을 확인한다.
- 수렴 검토(Convergence Review): 제시 전 전체 고정 그래프에 대해 듀얼 모델 검토를 수행하여 문장의 의미가 변질되는 것을 방지한다.
자기 개선 메커니즘:
- 실행 기록(Run Record): 모든 실행(수용, 강등, 또는 실패)은 기록된다. 실패한 실행은 미래의 에이전트가 막다른 길을 반복하지 않도록 방지하며, 강등된 실행은 참신함의 목표를 정교화한다.
- 라이브러리 피드백: 실행 중 Causalean에 없는 새로운 핵심 레마가 필요한 경우, 시스템은 이를 증명하기 위해 "학습 모드"에 진입한다. 검증 및 재사용성 검토가 완료되면, 해당 레마는 향후 실행을 위해 Causalean으로 승격된다.

주요 기여

Causalean 라이브러리: 자동화된 발견을 위한 검증된 토대로서 작용하는 인과 추론 툴킷의 광범위한 기계 확인 공식화(7,035개 선언).
CausalSmith 파이프라인: 주제를 자율적으로 선택하고, 결과를 제안하며, 이를 Lean 4로 공식화 및 증명하고, 공식 문장의 충실도를 감사하는 엔드 투 엔드 시스템.
문장 감사 메커니즘: 공식적 검증과 과학적 의도 사이의 간극을 메우는 새로운 접근 방식. 로직 그래프를 노드 단위로 감사함으로써, 시스템은 커널에 의해 수용된 증명이 단순히 구문론적으로 유효한 정리가 아니라 특정 과학적 주장과 부합함을 보장한다.
실증적 평가: 기존 문헌의 기술적 공백을 메우는 9개의 수용된 결과를 포함하여 123개의 기록된 자율 연구 실행 카탈로그.

결과

시스템은 123회의 기록된 실행을 통해 평가되었다:

결과: 9건의 실행이 수용되었고, 44건은 강등되었으며(타당하지만 참신함이 부족함), 70건은 실패했다(제안 또는 수학적 유도 단계에서 거부됨).
성능 패턴: 시스템은 통계 이론, 실험법, 패널 방법 분야에서 탁월한 성능을 보였으며, 기술적 공백을 성공적으로 메웠다(예: 알려진 하한값에 상한값을 맞춤). 반면, 정확한 식별(Exact Identification), 부분 식별(Partial Identification), SCM 클러스터에서는 어려움을 겪었는데, 이 영역들은 기술적 정교화보다는 새로운 개념적 아이디어를 요구하기 때문이다. 이 영역들에서 시스템은 수학적으로는 타당하지만 알려진 구조로 환원되는 결과(예: "일반적인 Manski 스타일의 외곽 포함 관계")를 자주 생성했다.
주요 성과: 시스템은 고차원 이산 교란(high-dimensional discrete confounding) 하에서의 평균 처치 효과(ATE) 추정에 관한 미니맥스 갭(minimax gap)을 성공적으로 메웠다. 시스템은 Zeng 등[54]에 의해 확립된 알려진 상한과 하한 사이의 $\log^2$ 인자 갭을 메우는 계산 가능한 추정량을 구축했다. 이 결과는 기계로 확인되었고, 문장 충실도 감사를 거쳤으며, Lean 4 개발과 공식적으로 연결되었다.
라이브러리 성장: 피드백 루프를 통해 13개의 새로운 레마(예: Bretagnolle–Huber 친화도 경계, Fano의 부등식)가 특정 실행에서 일반 Causalean 라이브러리로 성공적으로 승격되었다.

의의 및 주장

본 논문은 CausalForge가 세 가지 별개의 질문을 분리함으로써 자동화된 이론 연구를 위한 새로운 신뢰 모델을 제공한다고 주장한다:

증명의 건전성(Proof Soundness): Lean 4 커널에 의해 보장됨.
문장의 충실도(Statement Faithfulness): 문장 감사를 통해 검증됨(공식 선언 vs 의도된 주장 비교).
과학적 유의성(Scientific Significance): 파이프라인의 참신함 등급에 의해 정보를 얻지만, 그 자체로 결정되지는 않는 인간의 판단 영역임.

저자들은 이 프레임워크가 정형 검증에 근거를 두면서도 정리의 의미에 관한 자동화의 한계를 명시적으로 인정함으로써, LLM 검토자의 불신할 수 있는 문제를 해결한다고 주장한다. 시스템은 자동화된 에이전트가 특히 기술적 공백이 잘 정의된 영역에서 기계로 확인되고 충실한 인과 정리를 생성할 수 있음을 입증한다. 그러나 본 논문은 현재 시스템이 진정으로 새로운 개념적 아이디어를 생성하는 데 한계가 있으며, LLM 기반의 참신함 및 충실도 감사의 신뢰성에 대한 추가적인 엄격한 연구가 필요함을 겸허히 밝히고 있다. 이 연구는 인간 연구자를 대체하는 것이 아니라, 인과 추론 이론의 경계를 탐구하기 위한 정형화된 기초를 가진 자기 개선형 도구를 제공하는 것을 목표로 한다.