안녕하세요? 저는 수학 교육용 게임을 개발하고자 프로그래밍을 배우고 있는 예비 창업자이고, 이름은 차불휘입니다.
정보통신산업진흥원 산하에 있는 오픈소스 소프트웨어 통합지원센터(오픈업)에서 2024 오픈소스 컨트리뷰션 아카데미(OSSCA)의 2차 체험형 프로그램을 9월부터 10월까지 운영할 예정입니다.
이번에 드디어 저도 컨트리뷰션 아카데미의 멘토로 뽑혔습니다. 저는 멘티분들에게 린 정리 증명기를 가르치면서 자연수 게임을 멘티분들과 함께 한국어로 번역할 계획입니다.
위의 링크에서도 확인하실 수 있는 제 프로젝트 'Git 활용 및 Lean'의 안내문을 아래에 옮겨 적었습니다.
깃 버전 관리 시스템과 린 정리 증명기
프로젝트 개요
- 프로젝트명: Git 활용 및 Lean
- 프로젝트 분야: 깃 심화, 정리 증명
- 활용 기술: 깃(Git), 린(Lean)
- 프로젝트 난이도: ★★★★★(매우 어려움)
활용 언어: 린
- 린을 비롯한 상호 작용 정리 증명기를 다루신 적이 없어도 괜찮습니다.
- 제가 멘티분들에게 린 정리 증명기의 이용법을 자세히 가르칠 계획입니다.
- 저장소
프로젝트 소개
린 정리 증명기
- 린(Lean): 상호 작용 정리 증명기 겸 순수 함수형 프로그래밍 언어
- 상호 작용 정리 증명기: 사람이 형식 증명을 작성하도록 돕는 컴퓨터 프로그램
- 형식 증명: 증명 검증기라는 컴퓨터 프로그램으로 검증할 수 있는 증명
- 린의 활용
- 형식 검증: 컴퓨터 프로그램이 그 명세에 맞게 동작함을 증명하기
- 수학 인공 지능의 개발: 린이 검증할 수 있는 수학 증명을 생성하는 언어 모형 만들기
- 학술 이론의 형식화: 수학·컴퓨터 과학·물리학·철학 이론을 재서술하고 검증하기
증명 지향 프로그래밍
- 증명 지향 프로그래밍: 개발자가 프로그램과 증명을 함께 설계해 프로그램 동작의 여러 측면을 수학적으로 보장하는 패러다임
- 기능 정확성: 프로그램이 입력값마다 명세에 맞는 출력값을 산출하는 성질
- 보안 성질: 프로그램이 특정 비밀을 절대로 유출하지 않는 성질
- 그 밖의 성질: 자원 이용의 한계에 관한 성질 등
- 증명 지향 프로그래밍 언어: F*, 다프니(Dafny) 등
- 라이브러리와 도구가 충분히 개발되고 나면, 린으로 증명 지향 프로그래밍을 하기가 지금보다 수월할 것임.
린의 활용 사례 1: 시더
- 시더(Cedar): 아마존 웹 서비스(AWS)에서 2023년 5월 10일에 발표한 인가 정책 언어
- 시더 개발진이 시더의 형식 모형을 린으로 작성하고, 시더의 컴포넌트들이 핵심적인 안전 및 보안 속성을 지님을 증명함.
- 러스트로 구현한 시더가 그 형식 모형과 일치함을 차등 무작위 시험으로 확인함.
- 참고 자료
린의 활용 사례 2: 샘프서트
- 샘프서트(SampCert): 차등 프라이버시를 위한 이산 가우스 샘플러
- 린과 그 수학 라이브러리 매스리브(Mathlib)를 이용해 검증한 구현물임.
- 린으로 작성한 이 구현물은 계산 가능하지 않지만, 린 코드에서 다프니 코드를 추출할 수 있음.
- 다프니-VMC: 검증된 몬테카를로 알로리듬을 위한 다프니 라이브러리
- 샘프서트 코드에서 추출한 다프니 코드가 이 라이브러리에 포함돼 있음.
- 참고 자료
린의 활용 사례 3: 구글 딥마인드의 알파푸르프
- 알파푸르프(AlphaProof): 형식 수학 추리를 위한 강화 학습 기반 시스템
- 린의 언어로 수학 진술을 증명하도록 자기 자신을 훈련함.
- 사전 훈련된 언어 모형과 알파제로(AlphaZero) 강화 학습 알고리듬을 결합함.
- 제미니(Gemini) 모형을 미세하게 조정해 자연 언어로 쓰인 문제 진술을 형식 진술로 번역함. 이로써 다양한 난이도의 대규모 형식 문제 라이브러리를 만듦.
- 참고 자료
컨트리뷰션 운영 방안
활동 목표
- 프로젝트 관리
- 깃(Git) 버전 관리 시스템으로 프로젝트 관리하기
- 깃허브(GitHub)에서 프로젝트 개발에 기여하기
- 정리 증명
- "린 4로 하는 정리 증명" 교재의 연습 문제 다 풀기
- 자연수 게임 한국어로 번역하기
첫째 주(9월 9~15일)
- "린 4로 하는 정리 증명" 교재: 1~3장 읽기, 3장 연습 문제 풀기
- 프로젝트 관리: 자신의 연습 문제 풀이를 모은 깃 저장소를 만들고 깃허브에서 공유하기
둘째 주(9월 16~22일)
- 추석 연휴: 16~18일
- "린 4로 하는 정리 증명" 교재: 4장 읽고 연습 문제 풀기
- 프로젝트 관리: 매깃(Magit) 등의 이용자 친화적인 깃 인터페이스로 커밋 이력 관리하기
셋째 주(9월 23~29일)
- "린 4로 하는 정리 증명" 교재: 5~6장 읽기, 5장 연습 문제 풀기
- 프로젝트 관리: 오메가T를 이용해 프로젝트 번역하기
- 자연수 게임: 튜토리얼·덧셈 세계 번역하기
넷째 주(9월 30일~10월 6일)
- "린 4로 하는 정리 증명" 교재: 7~8장 읽고 연습 문제 풀기
- 프로젝트 관리: 연습 삼아 풀 요청하기(PR)
- 자연수 게임: 곱셈·거듭제곱 세계 번역하기
다섯째 주(10월 7~13일)
- "린 4로 하는 정리 증명" 교재: 9~11장 읽기
- 프로젝트 관리: 연습 삼아 풀 요청 병합하기
- 자연수 게임: 함의·알고리듬 세계 번역하기
여섯째 주(10월 14~20일)
- "린 4로 하는 정리 증명" 교재: 12장 읽기
- 프로젝트 관리: 린 웹 게임 관리자에게 풀 요청하기
- 자연수 게임: 상급 덧셈·부등식 세계 번역하기
남은 5일(10월 21~25일)
- "린 4로 하는 정리 증명" 교재: 복습하기
- 프로젝트 관리: 자신이 만든 저장소 정돈하기
- 자연수 게임: 상급 곱셈 세계 번역하기
학습 모임
- 매주 최소 2회, 매회 최소 2시간 진행할 듯합니다.
- 아마 대면 모임에서는 주로 제가 멘토분들에게 기술 지원을 할 듯합니다.
"린 4로 하는 정리 증명" 교재의 난이도
- 6주 동안 "린 4로 하는 정리 증명" 교재를 완독하고 모든 연습 문제를 푸신 멘티분은 저보다 학습 속도가 7배 이상 빠릅니다.
- 제가 다른 자료를 참고하면서 이 교재를 찬찬히 읽었다는 점을 감안하면, 멘티분들이 저보다 적어도 3배 빨리 이 교재를 읽고 연습 문제를 풀어내실 수 있을 듯합니다.
- 멘티분들이 이 교재를 7장까지 읽고 연습 문제를 다 푸시기만 해도 이 체험형 프로젝트는 성공한 셈입니다.
린에 관한 첨언
- 제가 멘티분들에게 가르칠 다음 개념은 린의 이용법을 이해하는 데 꼭 필요합니다.
- 명제 논리: 논리 연결어(부정, 논리곱, 논리합, 함의, 동등)
- 술어 논리: 양화사(보편 양화사, 존재 양화사)
- 자연수 게임
- 수학적 귀납법에 대한 배경지식이 필요합니다.
- 한국어로 번역할 텍스트가 그리 많지는 않습니다.
멘토 소개: 차불휘(Bulhwi Cha)
- 2024년 6~7월: 시네레라 GG 인피니티 문서 개정 기여
- 2024년 1~6월: 린 배터리 라이브러리 개발 기여
- 2023년 4~8월
- 매스리브 포팅 기여
- 린 표준 라이브러리 개발 기여