LLM의 발전으로 수학 분야에서 많은 돌파구가 마련되고 있는 가운데, 연구진은 응용 과학의 한 분야인 Causal Inference 연구를 자동화하기 위한 에이전트 파이프라인 'CausalSmith'를 선보였습니다. CausalSmith는 아이디어를 제안하는 Discovery, Lean 4 언어로 수식을 검증하는 Formalization, 그리고 결과물을 논문 형태로 만드는 Presentation의 3단계 과정을 거칩니다. 특히 Causalean이라는 전용 Lean 4 라이브러리를 구축하여 연구의 정확성을 높이고, 검증된 결과를 재사용할 수 있는 구조를 갖추고 있습니다. 현재까지 1,700회 이상의 실행을 통해 실제 연구에 적용 가능한 유의미한 결과를 도출하며 그 가능성을 보여주고 있습니다.