formal verification형식 검증

formal verification은 하드웨어나 소프트웨어가 수학적으로 정의한 명세를 만족하는지 논리와 증명으로 확인하는 방법이다. 일부 입력만 시험하는 테스트와 달리, 명세가 다루는 모든 경우에 대해 성질이 성립함을 보이려 한다. 대표적인 기법으로 model checking과 정리 증명이 있다.

반도체 설계, 항공우주, 운영체제 kernel, 암호처럼 오류의 대가가 큰 분야에서 쓰여 왔다. AI 분야에서는 AI가 생성한 코드와 수학 증명을 기계적으로 확인하는 수단으로 쓰인다.

이 설명은 AIPOST 기사와 널리 알려진 사실을 바탕으로 정리했습니다. 잘못된 내용이 있으면 정정 요청으로 알려 주세요.