Get up-to-date information at: https://luma.com/6fx4hphm
Address:
모두의연구소 강남캠퍼스
2층 라운지
Seoul, South Korea
[리벨리온x모두의연구소] AI for Science/Engineering 연례 정기 세미나 2026
세미나 안내
최근 인공지능은 글을 쓰고 번역하는 것을 넘어, 수학 문제를 이해하고 증명을 찾아가는 영역까지 빠르게 발전하고 있습니다.
이번 강연에서는 이러한 변화의 중심에 있는 2가지 핵심 개념을 소개합니다:
'자동 형식화(Autoformalization)'와
'자동 정리 증명(Automated Theorem Proving, ATP)'
수학자들은 증명이 올바른지 컴퓨터로 확인하기 위해 '증명 보조기(Proof Assistant)'라는 도구를 사용합니다.
하지만 이를 활용하려면 우리가 평소 사용하는 자연스러운 수학 문장을 컴퓨터가 정확하게 이해할 수 있는 형식 언어로 다시 작성해야 합니다. 이 과정은 숙련된 수학자에게도 쉽지 않으며 상당한 시간과 노력이 필요합니다.
'자동 형식화'는 이러한 과정을 인공지능을 이용해 자동화하는 기술입니다.
즉, 사람이 작성한 수학적 명제와 증명을 컴퓨터가 검증할 수 있는 형식으로 변환하는 것입니다. 아직 복잡한 수학적 내용을 완벽하게 변환하기에는 한계가 있지만, 최근 대규모 언어 모델을 활용한 연구에서 빠른…
Hosted by 모두의연구소 커뮤니티, SungTay & 이영빈
세미나 안내
최근 인공지능은 글을 쓰고 번역하는 것을 넘어, 수학 문제를 이해하고 증명을 찾아가는 영역까지 빠르게 발전하고 있습니다.
이번 강연에서는 이러한 변화의 중심에 있는 2가지 핵심 개념을 소개합니다:
'자동 형식화(Autoformalization)'와
'자동 정리 증명(Automated Theorem Proving, ATP)'
수학자들은 증명이 올바른지 컴퓨터로 확인하기 위해 '증명 보조기(Proof Assistant)'라는 도구를 사용합니다.
하지만 이를 활용하려면 우리가 평소 사용하는 자연스러운 수학 문장을 컴퓨터가 정확하게 이해할 수 있는 형식 언어로 다시 작성해야 합니다. 이 과정은 숙련된 수학자에게도 쉽지 않으며 상당한 시간과 노력이 필요합니다.
'자동 형식화'는 이러한 과정을 인공지능을 이용해 자동화하는 기술입니다.
즉, 사람이 작성한 수학적 명제와 증명을 컴퓨터가 검증할 수 있는 형식으로 변환하는 것입니다. 아직 복잡한 수학적 내용을 완벽하게 변환하기에는 한계가 있지만, 최근 대규모 언어 모델을 활용한 연구에서 빠른…
Hosted by 모두의연구소 커뮤니티, SungTay & 이영빈