CausalForge, AI가 인과 추론 명제를 만들고 Lean으로 증명

연구진이 인과 추론 연구의 주제 선정부터 정리 제안·형식화·증명·설명까지 수행하고 Lean으로 확인하는 자동화 프레임워크 CausalForge를 공개했다.

무엇이 공개됐나

CausalForge는 인과 추론 연구를 단순한 자연어 생성이 아니라 형식 검증 가능한 과정으로 만들려는 연구 프레임워크입니다. 에이전트가 연구 주제를 고르고 새 결과를 제안한 뒤, Lean 코드로 명제를 형식화하고 증명을 시도합니다.

핵심 구성

  • 기반 라이브러리 Causalean에는 논문 기준 7,035개의 기계 검증 선언이 포함됩니다.
  • CausalSmith 모듈이 주제 선택, 결과 제안, 형식화, 증명과 설명 생성을 연결합니다.
  • statement audit는 형식 정리가 자연어로 주장한 내용과 실제로 일치하는지 다시 대조합니다.
  • 저자들은 코드, 라이브러리와 실행 기록을 공개했다고 밝혔습니다.

왜 중요한가

과학용 AI가 그럴듯한 문장을 만드는 데서 벗어나, 결과의 정확한 조건과 논리적 연결을 기계가 확인할 수 있게 하는 접근입니다. 특히 인과 추론처럼 가정 하나가 결론을 크게 바꾸는 분야에서 재현성과 감사 가능성을 높일 수 있습니다.

확인할 한계

이 논문은 2026년 7월 공개된 사전 논문이며 동료 평가가 완료된 결과가 아닙니다. 형식 증명은 작성된 명제의 논리적 타당성을 확인하지만, 그 명제가 현실의 올바른 질문인지 또는 가정이 타당한지까지 자동으로 보장하지는 않습니다.

공식 출처