- 형식 증명: 컴퓨터 프로그램이 검사할 수 있는 방식으로 구성된 증명.
- 증명 검사기: 형식 증명을 검사하는 컴퓨터 프로그램.
- 상호 작용 정리 증명기: 사람이 형식 증명을 작성하도록 돕는 컴퓨터 프로그램. 보통 증명 검사기의 역할도 겸함. 증명 보조기라고도 함.
- 대표적인 증명 보조기: 린(Lean), 코크(Coq), 아그다(Agda), 이저벨(Isabelle) 등.
- 프로그램 검증: 컴퓨터 프로그램이 그 명세에 맞게 동작함을 증명하기.
- 수학 인공 지능의 개발: 수학 정리의 형식 증명을 생성하는 언어 모형 만들기.
- 학술 이론의 형식화: 수학·컴퓨터 과학·물리학·철학 이론을 재서술하고 검증하기.
- 증명 지향 프로그래밍: 개발자가 프로그램과 증명을 함께 설계해 프로그램 동작의
여러 측면을 수학적으로 보장하는 패러다임.
- 기능 정확성: 프로그램이 입력값마다 명세에 맞는 출력값을 산출하는 성질.
- 보안 성질: 프로그램이 특정 비밀을 절대로 유출하지 않는 성질.
- 그 밖의 성질: 자원 이용의 한계에 관한 성질 등.
- 증명 지향 프로그래밍 언어: F*, 다프니(Dafny) 등.
- F*: 이용자가 정의한 부작용을 지원하는 의존형 프로그래밍 언어 겸 증명 보조기.
- 다프니: C#, 자바, 자바스크립트, 고(Go), 파이선 등의 언어로 컴파일이 되는 명령형 프로그래밍 언어.
- 형식 수학 추리를 위한 강화 학습 기반 시스템.
- 린의 언어로 수학 진술을 증명하도록 자기 자신을 훈련함.
- 사전 훈련된 언어 모형과 알파제로(AlphaZero) 강화 학습 알고리듬을 결합함.
- 제미니(Gemini) 모형을 미세하게 조정해 자연 언어로 쓰인 문제 진술을 형식 진술로 번역함. 이로써 다양한 난이도의 대규모 형식 문제 라이브러리를 만듦.
- 알파지오메트리(AlphaGeometry) 2 기하학 문제 해결 시스템과 알파푸르프가 2024년 국제 수학 올림피아드(IMO)의 여섯 문제 가운데 넷을 풂.
- 스마트 계약과 그 명세 및 구현을 다프니 언어로 작성하면, 그 스마트 계약을 검증할 수 있음.
- 임의 재진입성은 스마트 계약에서 발생하는 버그와 공격의 주요 근원인데, 저자들은 본 논문에서 임의 재진입성에 대한 추리 방법을 제안함.
- 저자들이 작성한 다프니 코드는 설리디티 등의 언어로 작성한 스마트 계약으로 적정하게 옮길 수 있음.
- 설리디티(Solidity)는 이더리움(이시리엄) 탈중앙화 블록체인에서 작동하는 스마트 계약을 개발하기 위한 정적 유형 프로그래밍 언어임.
- 참고 자료
- 마이크로소프트 연구소, 카네기 멜런 대학, INRIA, MSR-INRIA 협력 센터를 포함한 여러 기관의 연구원과 엔지니어가 F* 증명 보조기를 활용해, 2016년부터 HTTPS 생태계의 여러 구성 요소를 형식적으로 검증함.
- 에베레스트 소프트웨어는 리눅스 커널, 윈도 커널, 마이크로소프트 애저(Azure), 모질라 파이어폭스 등의 여러 시스템에 배치됨.
- TLS-1.3 레코드 계층과 그 암호 알고리듬의 참조 구현물을 구축하고 검증함.
- QUIC, 시그널(Signal), DICE 같은 새로운 보안 프로토콜의 검증된 구현물을 만듦.