검증 가능한 AI를 향하여: 형식적 방법의 5가지 과제

인공지능은 학습, 문제 해결, 합리적 사고와 행동 등 지능과 직관적으로 관련된 인간의 일부 기능을 포함하여 인간 지능을 모방하려는 컴퓨팅 시스템입니다. 광범위하게 해석되는 AI라는 용어는 기계 학습과 같이 밀접하게 관련된 여러 분야를 포괄합니다. AI를 많이 활용하는 시스템은 의료, 교통, 금융, 소셜 네트워크, 전자상거래, 교육 등의 분야에서 상당한 사회적 영향을 미치고 있습니다.

이렇게 사회적 영향이 커지면서 인공지능 소프트웨어의 오류, 사이버 공격, 인공지능 시스템 보안 등 일련의 위험과 우려도 함께 가져왔습니다. 따라서 AI 시스템 검증 문제, 더 나아가 신뢰할 수 있는 AI라는 주제가 연구계의 관심을 끌기 시작했습니다. "검증 가능한 AI"는 특정 수학적 요구 사항에 대해 강력하고 이상적으로 입증 가능한 정확성을 보장하는 검증 가능한 AI 시스템인 AI 시스템을 설계하기 위한 목표로 설정되었습니다. 우리는 어떻게 이 목표를 달성할 수 있습니까?

최근 "The Communications of ACM"의 리뷰 기사에서는 검증 가능한 AI가 직면한 과제를 공식 검증의 관점에서 생각해 보고 몇 가지 원칙적인 솔루션을 제시했습니다. 저자는 UC Berkeley 전기 공학 및 컴퓨터 과학과의 학과장인 S. Shankar Sastry 교수와 Sanjit A. Seshia, 그리고 Stanford University의 컴퓨터 과학 조교수인 Dorsa Sadigh입니다.

컴퓨터 과학 및 공학에서 형식적 방법에는 엄격한 수학적 사양, 설계 및 시스템 검증이 포함됩니다. 핵심적으로 형식적 방법은 증명에 관한 것입니다. 즉, 증명 의무를 형성하는 사양을 공식화하고, 이러한 의무를 이행하기 위한 시스템을 설계하고, 알고리즘 증명 검색을 통해 시스템이 실제로 해당 사양을 준수하는지 확인하는 것입니다. 사양 기반 테스트 및 시뮬레이션부터 모델 확인 및 정리 증명에 이르기까지 다양한 형식적 방법은 집적 회로의 컴퓨터 지원 설계에 일반적으로 사용되며 소프트웨어에서 버그를 찾고, 사이버 물리 시스템을 분석하고, 보안을 발견하는 데 널리 사용되었습니다. 취약점.

이 기사에서는 형식 방법의 전통적인 적용 방법을 검토하고 다음을 포함하여 AI 시스템에서 형식 방법의 5가지 고유한 과제를 지적합니다.

• 환경에 관한 언어 및 알고리즘 개발
• 복잡한 ML 구성요소 및 시스템을 추상화하고 표현합니다.
• AI 시스템 및 데이터에 대한 새로운 정식 형식 방법 및 속성을 제안합니다.
• 자동 추론을 위한 확장 가능한 컴퓨팅 엔진 개발
• 알고리즘 개발 그리고 시공에 의한 신뢰받는 설계를 위한 기술

저자는 최근 진행된 논의를 바탕으로 위의 과제를 해결하기 위한 원칙을 제안합니다. 이 기사에서는 심층 신경망과 같은 특정 유형의 AI 구성 요소나 강화 학습과 같은 특정 방법에만 초점을 맞추는 것이 아니라 더 광범위한 AI 시스템과 설계 프로세스를 다루려고 합니다. 게다가 형식적 방법은 신뢰할 수 있는 AI를 향한 하나의 경로일 뿐이므로 이 문서의 아이디어는 다른 분야의 방법을 보완하기 위한 것입니다. 이러한 관점은 안전 및 검증 문제가 더 두드러지는 자율 및 반자율 시스템에서 AI의 사용으로 인해 발생하는 문제에 대해 생각함으로써 크게 알 수 있습니다.

개요

그림 1은 형식 검증, 형식 합성 및 형식 안내 런타임 복원력을 위한 일반적인 프로세스를 보여줍니다. 공식 검증 프로세스는 세 가지 입력으로 시작됩니다.

그림 1: 검증, 합성 및 런타임 복원력을 위한 공식 접근 방식

1. 검증할 시스템 모델 S
2. 환경 모델 E
3. 검증할 속성 Φ

검증기는 예 또는 아니요 응답을 출력으로 생성합니다. 여부를 나타냅니다. S는 환경 E에서 속성 Φ를 만족합니다. 일반적으로 "아니요" 출력에는 Φ가 어떻게 위조되었는지 보여주는 시스템 실행인 오류 추적이라고도 알려진 반례가 수반됩니다. 일부 검증 도구에는 "예"라고 대답하는 정확성 증명이나 인증서도 포함되어 있습니다. 우리는 형식적 사양, 검증 또는 합성의 일부 측면을 사용하는 기술을 포함하여 형식적 방법에 대한 광범위한 관점을 취합니다. 예를 들어, 시뮬레이션 기반 하드웨어 검증 방법이나 모델 기반 소프트웨어 테스트 방법은 공식 사양이나 모델을 사용하여 시뮬레이션 또는 테스트 프로세스를 안내하기 때문에 포함됩니다.

AI 시스템에 형식 검증을 적용하려면 최소한 세 가지 입력 S, E, Φ를 공식적으로 나타낼 수 있어야 합니다. "예"라고 답할 수 있는 효율적인 의사 결정 절차가 있어야 합니다. " 앞서 설명한 /아니요" 질문입니다. 그러나 기본 설계 및 검증 문제의 복잡성을 처리하는 것은 고사하고 세 가지 입력에 대해서도 좋은 표현을 구성하는 것은 사소한 일이 아닙니다.

여기서는 반자율 주행 분야의 예를 통해 이 기사의 요점을 설명합니다. 그림 2는 AI 시스템의 예시를 보여줍니다. 즉, 기계 학습 구성 요소와 해당 환경을 갖춘 반자율 차량을 포함하는 폐쇄 루프 CPS입니다. 특히 반자율 "자아" 차량에는 전방의 물체를 감지 및 분류하고 충돌을 피하기 위해 필요할 때 브레이크를 적용하는 자동 비상 제동 시스템(AEBS)이 있다고 가정합니다. 그림 2에서 AEBS는 컨트롤러(자율 제동), 제어 대상(자율 스택의 다른 부분을 포함하는 제어 차량 하위 시스템), 센서(카메라) 및 DNN을 사용하는 인식 구성 요소로 구성됩니다. AEBS는 차량 환경과 결합되어 폐쇄 루프 CPS를 형성합니다. "셀프" 차량의 환경에는 차량 외부(다른 차량, 보행자 등)는 물론 차량 내부(예: 운전자)에 대한 에이전트와 개체가 포함됩니다. 이러한 폐쇄 루프 시스템의 안전 요구 사항은 움직이는 "자아" 차량과 도로 위의 다른 에이전트 또는 물체 사이의 안전 거리를 유지하는 특성이라는 측면에서 비공식적으로 특성화될 수 있습니다. 그러나 이러한 시스템의 사양, 모델링 및 검증에는 미묘한 차이가 많이 있습니다.

그림 2: 기계 학습 구성 요소가 포함된 폐쇄 루프 CPS의 예

먼저 반자율 차량의 환경 모델링을 고려해보세요. 환경에 얼마나 많은 에이전트(인간 및 비인간 모두)가 있는지와 같은 질문조차도 그들의 속성과 행동은 물론이고 상당한 불확실성을 겪을 수 있습니다. 둘째, AI나 ML을 활용한 인식 작업은 불가능하지는 않더라도 공식화하기가 어렵습니다. 셋째, DNN과 같은 구성 요소는 복잡한 고차원 입력 공간에서 작동하는 복잡한 고차원 개체일 수 있습니다. 따라서 검증을 다루기 쉬운 형태로라도 공식 검증 프로세스의 세 가지 입력 S, E, Φ를 생성하는 것은 매우 어렵습니다.

누군가 이 문제를 해결한다면 그림 2처럼 복잡한 AI 기반 CPS를 검증하는 것은 어려운 작업이 될 것입니다. 이러한 CPS에서는 구성적(모듈형) 접근 방식이 확장성을 위해 중요하지만 구성 사양의 어려움 등의 요인으로 인해 구현이 어려울 수 있습니다. 마지막으로, CBC(correction-by-construction) 접근 방식은 검증 가능한 AI를 약속하지만 아직 초기 단계이며 사양 및 검증의 발전에 크게 의존합니다. 그림 3은 검증 가능한 AI의 5가지 도전적인 영역을 요약합니다. 각 영역에 대해 현재 유망한 접근 방식을 노드로 표현되는 과제 극복을 위한 세 가지 원칙으로 추출합니다. 노드 사이의 가장자리는 단일 색상으로 표현되는 공통 종속성 스레드를 통해 검증 가능한 AI의 어떤 원칙이 서로 의존하는지 보여줍니다. 이러한 과제와 해당 원칙은 아래에 자세히 설명되어 있습니다.

그림 3: 검증 가능한 AI의 5가지 과제 영역 요약

환경 모델링

AI/ML 기반 시스템이 실행되는 환경은 일반적으로 자율 차량이 운영되는 다양한 도시와 같이 복잡합니다. 교통 환경. 실제로 환경의 복잡성과 불확실성에 대처하기 위해 AI/ML이 이러한 시스템에 도입되는 경우가 많습니다. 현재 ML 설계 프로세스에서는 데이터를 사용하여 환경을 암시적으로 지정하는 경우가 많습니다. 많은 AI 시스템의 목표는 선험적으로 지정된 환경을 위해 설계된 기존 시스템과 달리 작동하면서 환경을 발견하고 이해하는 것입니다. 그러나 모든 형식적 검증과 종합은 환경 모델과 관련이 있습니다. 따라서 입력 데이터에 대한 가정과 속성을 환경 모델로 해석해야 합니다. 우리는 이러한 이분법을 AI 시스템 환경 모델링을 위한 세 가지 과제로 분류하고 이러한 과제를 해결하기 위한 해당 원칙을 개발합니다.

2.1 불확실성 모델링 ​

공식 검증의 전통적인 사용에서 일반적인 접근 방식은 환경을 제한된 비결정적 프로세스 또는 "교란"으로 모델링하는 것입니다. 환경 모델링의 이러한 "과도한 근사"를 통해 추론에 매우 비효율적인 지나치게 상세한 모델을 요구하지 않고 보다 보수적으로 환경 불확실성을 포착할 수 있습니다. 그러나 AI 기반 자율성의 경우 순전히 비결정적 모델링은 허위 오류 보고서를 너무 많이 생성하여 실제로 검증 프로세스를 쓸모 없게 만들 수 있습니다. 예를 들어, 자율주행차의 주변 차량의 거동을 모델링할 때 주변 차량의 거동이 다양하므로, 순수 비결정론적 모델링을 채택하면 항상 예상치 못하게 발생하는 사고를 고려할 수 없습니다. 또한 많은 AI/ML 시스템은 환경의 데이터 또는 동작에 대한 분포 가정을 암시적으로 또는 명시적으로 수행하므로 확률적 모델링이 필요합니다. 기본 분포를 정확하게 결정하는 것이 어렵기 때문에 결과적인 확률 모델이 완벽하다고 가정할 수 없으며 모델링 프로세스의 불확실성은 모델 자체에서 특성화되어야 합니다.

확률적 공식 모델링. 이러한 문제를 해결하기 위해 우리는 확률적 모델링과 비결정적 모델링을 결합한 형식을 제안합니다. 확률 분포를 안정적으로 지정하거나 추정할 수 있는 경우 확률론적 모델링을 사용할 수 있습니다. 다른 경우에는 비결정적 모델링을 사용하여 환경 동작을 과대평가할 수 있습니다. Markov 결정 프로세스와 같은 형식론은 이미 확률론적 접근 방식과 비결정론적 접근 방식을 혼합하는 방법을 제공하지만, 확률론적 프로그래밍 패러다임과 같은 보다 풍부한 형식론이 환경을 모델링하는 데 더 표현적이고 절차적인 방법을 제공할 수 있다고 믿습니다. 우리는 많은 경우 그러한 확률적 절차를 데이터로부터 (부분적으로) 학습하거나 합성해야 할 것이라고 예측합니다. 이 시점에서 학습된 매개변수의 불확실성은 시스템의 나머지 부분에 전파되어 확률 모델로 표현되어야 합니다. 예를 들어, 볼록 마르코프 결정 프로세스는 학습된 전이 확률 값의 불확실성을 표현하고 이러한 불확실성을 설명하기 위해 검증 및 제어를 위한 알고리즘을 확장하는 방법을 제공합니다.

2.2 알 수 없는 변수​

디바이스 드라이버 검증과 같은 전통적인 형식 검증 분야에서는 시스템 S와 환경 E 사이의 인터페이스가 잘 정의되어 있으며 E는 이 인터페이스를 통해서만 S와 통신할 수 있습니다. 상호 작용합니다. AI 기반 자율성의 경우 이 인터페이스는 불완전하며 환경을 부분적으로 시끄럽게 캡처하고 S와 E 사이의 모든 상호 작용을 캡처할 수 없는 센서 및 인식 구성 요소에 의해 결정됩니다. 환경의 모든 변수(특성)는 인식은 물론이고 알려져 있습니다. 환경 변수가 알려진 제한된 시나리오에서도 특히 설계 시점에 환경 변수의 진화에 대한 정보가 뚜렷하게 부족합니다. 또한 환경 인터페이스를 나타내는 LiDAR와 같은 센서를 모델링하는 것은 중요한 기술적 과제입니다.

성찰적인 환경 모델링. 우리는 내성적 설계 및 검증 방법을 개발함으로써 이 문제를 해결할 것을 제안합니다. 즉, 사양 Φ가 충족된다는 것을 보장하기에 충분한 환경 E에 대한 가정 A를 알고리즘적으로 식별하기 위해 시스템 S에서 내성을 수행하는 것입니다. 이상적으로 A는 이러한 가정 중 가장 약한 가정이어야 하며, 설계 시 생성하고 런타임 시 사용 가능한 센서 및 기타 환경 정보 소스를 모니터링하고 가정이 위반될 때 감지를 용이하게 할 만큼 효율적이어야 합니다. 취해진다. 더욱이, 인간 조작자가 관여하는 경우 A가 이해 가능한 설명으로 변환될 수 있기를 바랄 수 있습니다. 즉, S는 왜 사양 Φ를 충족하지 못할 수 있는지 인간에게 "설명"할 수 있습니다. 좋은 센서 모델의 필요성과 함께 이러한 다양한 요구 사항을 처리하는 것은 내성적인 환경 모델링을 매우 중요한 문제로 만듭니다. 예비 작업에서는 모니터링 가능한 가설을 추출하는 것이 단순한 경우에 가능하다는 것을 보여 주지만, 이를 실용화하려면 더 많은 작업이 필요합니다.

2.3 인간 행동 시뮬레이션 ​

반자율 자동차와 같은 많은 AI 시스템에서 인간 에이전트는 환경과 시스템의 중요한 부분입니다. 인간의 인공 모델은 인간 행동의 가변성과 불확실성을 적절하게 포착하지 못합니다. 반면, 인간 행동을 모델링하기 위한 데이터 기반 접근 방식은 ML 모델에서 사용되는 기능의 표현력과 데이터 품질에 민감할 수 있습니다. 인간 AI 시스템에 대한 높은 보증을 달성하려면 현재 인간 모델링 기술의 한계를 해결하고 예측 정확성과 수렴에 대한 보증을 제공해야 합니다.

선제적인 데이터 기반 모델링. 우리는 인간 모델링에는 적극적인 데이터 기반 접근 방식이 필요하며, 수학적으로 표현된 모델 구조와 특징은 형식적인 방법에 적합하다고 믿습니다. 인간 모델링의 핵심 부분은 인간의 의도를 포착하는 것입니다. 우리는 전문 지식을 기반으로 모델의 템플릿이나 기능을 정의하고, 오프라인 학습을 사용하여 디자인 타임에 사용할 모델을 완성하고, 환경을 모니터링하고 상호 작용하여 런타임에 환경 모델을 학습하고 업데이트하는 세 가지 접근 방식을 제안합니다. 예를 들어, 연구에 따르면 인간 대상 실험을 통해 운전 시뮬레이터에서 수집한 데이터를 사용하여 자율 차량을 검증하고 제어하는 ​​데 사용할 수 있는 인간 운전자의 행동 모델을 생성할 수 있습니다. 또한, 컴퓨터 보안의 적대적 훈련 및 공격 기술은 인간 모델의 능동적 학습과 안전하지 않은 행동으로 이어지는 특정 인간 행동에 대한 모델 설계에 사용될 수 있습니다. 이러한 기술은 인간-AI ​​시스템을 위한 검증 알고리즘을 개발하는 데 도움이 될 수 있습니다.

공식 사양

공식 검증은 공식 사양, 즉 시스템이 수행해야 하는 작업에 대한 정확한 수학적 설명에 크게 의존합니다. 정형적 방법이 상당한 성공을 거둔 영역에서도 고품질의 정형 사양을 마련하는 것이 어려운 일이며, 특히 AI 시스템은 독특한 과제에 직면해 있습니다.

3.1 작업을 공식화하기 어려움 ​

그림 2의 AEBS 컨트롤러에 있는 인식 모듈은 물체를 감지하고 분류하여 차량과 보행자를 다른 개체와 구별해야 합니다. 이 모듈의 정확성을 위해서는 각 유형의 도로 사용자 및 객체에 대한 공식적인 정의가 필요하며 이는 고전적인 형식적 방법 측면에서 매우 어렵습니다. 이 문제는 딥러닝 기반 방법뿐만 아니라 이 인식 모듈의 모든 구현에 존재합니다. 자연어 처리와 같이 인식 및 의사소통과 관련된 다른 작업에서도 비슷한 문제가 발생합니다. 그렇다면 그러한 모듈에 대한 정밀도 속성을 어떻게 지정합니까? 사양 언어는 무엇이어야 합니까? 사양을 작성하는 데 어떤 도구를 사용할 수 있습니까?

종단 간/시스템 수준 사양. 위의 문제를 해결하기 위해 이 문제를 약간 변경할 수 있습니다. 형식화하기 어려운 작업을 직접 지정하기보다는 먼저 AI 시스템의 엔드투엔드 동작을 정확하게 지정하는 데 집중해야 합니다. 이 시스템 수준 사양에서 형식화하기 어려운 구성 요소의 입출력 인터페이스에 대한 제약 조건을 얻을 수 있습니다. 이러한 제약 조건은 전체 AI 시스템과 상황에 맞게 관련된 구성 요소 수준 사양의 역할을 합니다. 그림 2의 AEBS 예의 경우 이는 동작 중에 모든 객체로부터 최소 거리를 유지하는 속성 Φ의 사양을 포함하며, 이를 통해 적대적 분석에서 의미를 포착하는 DNN 입력 공간에 대한 제약 조건을 도출할 수 있습니다. 입력 공간.

3.2 정량적 사양과 부울 사양​

전통적으로 공식 사양은 주어진 시스템 동작을 "참" 또는 "거짓"으로 매핑하는 부울인 경향이 있습니다. 그러나 AI와 ML에서는 사양이 비용이나 보상을 규제하는 목적 함수로 제공되는 경우가 많습니다. 또한 여러 목표가 있을 수 있으며 그 중 일부는 함께 충족되어야 하지만 일부는 특정 상황에서 서로 균형을 맞춰야 할 수도 있습니다. 두 가지 규범적 접근 방식인 부울 접근 방식과 정량적 접근 방식을 통합하는 가장 좋은 방법은 무엇입니까? 견고성, 공정성 등 AI 구성 요소의 공통 속성을 균일하게 포착하는 형식이 있습니까?

양적 사양과 부울 사양을 혼합하세요. 부울 사양과 정량적 사양 모두 장점이 있습니다. 부울 사양은 구성하기 쉽지만 목적 함수는 최적화 기반 기술을 통해 검증 및 합성을 용이하게 하고 더 미세한 속성 만족도 세분성을 정의합니다. 이러한 격차를 해소하는 한 가지 방법은 부울 및 정량적 의미론(예: 미터법 시간 논리)이 포함된 논리를 사용하거나 RL에 대한 보상 함수와 오토마타를 결합하는 등 정량적 사양 언어로 전환하는 것입니다. 또 다른 접근 방식은 부울 및 정량적 사양을 규칙집과 같은 공통 사양 구조로 결합하여 사양을 계층 구조로 구성, 비교 및 ​​요약할 수 있는 것입니다. 연구 결과에 따르면 견고성, 공정성, 개인정보 보호, 책임성, 투명성 등 AI 시스템의 여러 속성 범주가 확인되었습니다. 연구자들은 형식적 방법과 ML의 아이디어를 의미론적 견고성과 같은 이러한 속성의 모델 변형에 연결하는 새로운 형식론을 제안하고 있습니다.

3.3 데이터 대 형식적 요구 사항 ​

"데이터는 사양이다"라는 관점은 기계 학습에서 매우 일반적입니다. 제한된 입력 세트에 대한 레이블이 지정된 "실제" 데이터가 올바른 동작에 대한 유일한 사양인 경우가 많습니다. 이는 일반적으로 가능한 모든 입력을 통과하는 올바른 동작 집합을 정의하는 논리 또는 오토마타의 형태로 제공되는 형식적 방법과는 매우 다릅니다. 데이터와 규범 사이의 격차는 특히 데이터가 제한적이거나 편향되어 있거나 비전문가로부터 나온 경우 주목할 가치가 있습니다. 디자인 타임에 사용 가능한 데이터와 아직 발견되지 않은 데이터 모두 데이터의 속성을 공식화하는 기술이 필요합니다.

사양 마이닝. 데이터와 공식 사양 사이의 격차를 해소하기 위해 우리는 소위 사양 마이닝 기술인 데이터 및 기타 관찰에서 사양을 추론하는 알고리즘을 사용할 것을 제안합니다. 이러한 접근 방식은 인식 구성 요소를 포함한 ML 구성 요소에 자주 사용될 수 있습니다. 왜냐하면 많은 경우 정확한 사양이나 사람이 읽을 수 있는 사양이 필요하지 않기 때문입니다. 또한 규범 마이닝 방법을 사용하여 데모나 여러 에이전트(인간과 AI) 간의 보다 복잡한 형태의 상호 작용에서 인간의 의도와 기타 속성을 추론할 수 있습니다.

학습 시스템 모델링

대부분의 전통적인 형식 검증 응용에서 시스템 S는 프로그램일 수도 있고 프로그래밍 언어나 하드웨어를 사용하는 프로그램일 수도 있으므로 설계 시점에 고정되어 알려져 있습니다. 회로를 설명하는 설명 언어입니다. 시스템 모델링 문제는 주로 관련 없는 세부 사항을 추상화하여 S를 보다 다루기 쉬운 크기로 줄이는 것과 관련됩니다. AI 시스템은 주로 기계 학습의 사용으로 인해 시스템 모델링에 매우 다양한 과제를 안겨줍니다.

고차원 입력 공간 ​

ML 인식 구성 요소는 일반적으로 매우 높은 차원에서 작동합니다. 입력 공간. 예를 들어, 입력 RGB 이미지는 1000 x 600 픽셀일 수 있으며, 여기에는 256개((1000x600x3)) 요소가 포함됩니다. 입력은 일반적으로 이와 같은 고차원 벡터 스트림입니다. 연구자들은 디지털 회로에서와 같이 고차원 입력 공간에 대해 형식적 방법을 사용했지만 ML 기반 인식을 위한 입력 공간의 특성은 완전히 부울이 아니며 혼합되어 있으며 이산 변수와 연속 변수를 포함합니다. .

고차원 매개변수/상태 공간 ​

심층 신경망과 같은 ML 구성요소에는 수천에서 수백만 개의 모델 매개변수와 원시 구성요소가 있습니다. 예를 들어, 그림 2에 사용된 최첨단 DNN에는 최대 6천만 개의 매개변수와 수십 개의 구성 요소 레이어가 있습니다. 이는 검증을 위한 거대한 검색 공간을 생성하며 추상화 프로세스는 매우 신중해야 합니다.

온라인 적응과 진화​

RL을 사용하는 로봇과 같은 일부 학습 시스템은 새로운 데이터와 상황에 직면하면서 진화합니다. 이러한 시스템의 경우 설계 시 검증은 시스템 동작의 향후 진화를 설명하거나 학습 시스템이 발전함에 따라 온라인으로 점진적으로 수행되어야 합니다.

컨텍스트에 따른 시스템 모델링 ​

많은 AI/ML 구성 요소의 경우 해당 사양은 컨텍스트에 의해서만 정의됩니다. 예를 들어 그림 2의 DNN 기반 시스템의 보안을 확인하려면 환경 모델링이 필요합니다. 의미상 의미 있는 속성을 확인할 수 있도록 ML 구성 요소와 해당 컨텍스트를 모델링하는 기술이 필요합니다.

최근 몇 년 동안 많은 작업이 DNN의 견고성과 입출력 속성을 검증하기 위해 효율성을 향상시키는 데 중점을 두었습니다. 그러나 이것만으로는 충분하지 않으며 다음 세 가지 측면에서도 진전이 필요합니다.

자동 추상화 및 효율적인 표현​

자동으로 생성된 시스템 추상화는 항상 형식적 방법의 핵심이었습니다. 이는 형식적 방법의 핵심입니다. 형식적 방법은 범위를 대규모 하드웨어 및 소프트웨어 시스템으로 확장하는 데 중요한 역할을 합니다. 초고차원 혼합 상태 공간과 ML 기반 시스템의 입력 공간 문제를 해결하려면 ML 모델을 형식적 분석에 더 적합한 간단한 모델로 추상화하는 효율적인 기술을 개발해야 합니다. 몇 가지 유망한 방향에는 추상적 해석을 사용하여 DNN을 분석하고, ML 구성 요소를 사용하여 사이버 물리 시스템을 제작하기 위한 추상화를 개발하고, 검증을 위한 새로운 표현(예: 별 집합)을 설계하는 것이 포함됩니다.

설명 및 원인과 효과

학습자가 데이터와 배경 지식에서 예측이 어떻게 나타나는지에 대한 설명을 예측과 함께 제공하면 학습 시스템 모델링 작업을 단순화할 수 있습니다. ML 커뮤니티에서 이미 '설명 기반 일반화'와 같은 용어를 연구하고 있어 이 아이디어는 새로운 것이 아니지만, 최근에는 학습 시스템의 출력을 설명하기 위해 논리를 사용하는 데 대한 관심이 다시 높아지고 있습니다. 설명 생성은 디자인 타임에 디자인과 사양을 디버깅하는 데 도움이 되며 런타임에 보증을 제공하는 강력한 AI 시스템을 합성하는 데 도움이 됩니다. 인과관계 및 반사실적 추론을 포함한 ML은 형식적 방법에 대한 설명을 생성하는 데도 도움이 될 수 있습니다.

의미론적 특징 공간​

ML 모델의 적대적 분석과 형식적 검증은 생성된 적대적 입력과 반례가 사용된 ML 모델의 의미 측면에서 의미론적 의미를 가질 때 더 효율적입니다. 예를 들어 DNN 객체 감지기를 분석하여 자동차 색상이나 시간의 작은 변화를 분석하는 기술은 임의로 선택한 소수의 픽셀에 노이즈를 추가하는 기술보다 더 유용합니다. 현재 대부분의 방법은 이 시점에서 부족합니다. 의미론적 적대 분석, 즉 ML 모델이 속한 시스템의 맥락에서 분석하는 것이 필요합니다. 핵심 단계는 ML 모델의 입력 공간을 정의하는 특정 기능 공간이 아니라 ML 시스템이 작동하는 환경을 모델링하는 의미론적 기능 공간을 표현하는 것입니다. 이는 구체적인 특징 공간(예: 교통 장면 이미지)의 의미상 의미 있는 부분으로 형성된 잠재 공간이 완전한 구체적인 특징 공간보다 훨씬 낮다는 직관과 일치합니다. 그림 2의 의미론적 특징 공간은 자율주행차 주변의 3차원 세계를 표현하는 저차원 공간인 반면, 특정 특징 공간은 고차원 픽셀 공간이다. 의미특징공간은 차원이 낮기 때문에 더 쉽게 검색할 수 있다. 그러나 의미론적 특징 공간의 한 지점을 구체적인 특징 공간의 한 지점으로 매핑하는 "렌더러"도 필요합니다. 차별화 가능성과 같은 렌더러의 속성을 사용하면 형식적 방법을 적용하여 의미론적 특징 공간의 목표 지향 검색을 수행하는 것이 더 쉬워집니다.

설계 및 검증을 위한 계산 엔진

하드웨어 및 소프트웨어 시스템에 대한 형식적 방법의 효율성은 기본 "계산 엔진"의 발전에 의해 주도됩니다(예: 부울 만족 가능성 해결(SAT), 만족 모듈러 이론( SMT) 및 모델 확인. AI/ML 시스템의 규모, 환경 복잡성 및 관련된 새로운 사양을 고려할 때 효율적이고 확장 가능한 교육, 테스트, 설계 및 검증을 위해서는 새로운 종류의 컴퓨팅 엔진이 필요하며, 이러한 발전을 달성하기 위해 극복해야 하는 주요 과제입니다.

5.1 데이터 세트 디자인​

데이터는 기계 학습의 기본 시작점입니다. ML 시스템의 품질을 향상하려면 학습하는 데이터의 품질을 향상해야 합니다. ML 데이터의 체계적인 선택, 설계 및 강화에 공식적인 방법이 어떻게 도움이 될 수 있습니까?

ML 데이터 생성은 하드웨어 및 소프트웨어의 테스트 생성 문제와 유사합니다. 공식적인 방법은 체계적이고 제약 조건 기반 테스트 생성에 효과적인 것으로 입증되었지만 이는 제약 조건 유형이 훨씬 더 복잡할 수 있는 인공 지능 시스템의 요구 사항과는 다릅니다. 예를 들어 복잡한 환경에서 데이터를 추출하기 위해 센서를 사용하는 경우입니다. 트래픽 상황으로) 캡처된 데이터의 "진위성"에 대한 요구 사항을 인코딩합니다. 특정 특성(예: 버그를 찾는 테스트)을 가진 데이터 항목을 생성해야 할 뿐만 아니라 배포 제약 조건을 충족하는 컬렉션도 생성해야 합니다. 데이터 생성은 효과적인 교육 및 일반화를 위해 데이터 세트 크기와 다양성 목표를 충족해야 합니다. 이러한 요구 사항에는 새로운 형식 기술 세트의 개발이 필요합니다.

정식 방법으로 통제된 무작위 배정. 데이터 세트 설계 문제에는 여러 가지 측면이 있습니다. 첫째, 응용 프로그램 의미에 따라 예제가 올바르게 구성되도록 "적법한" 입력 공간을 정의해야 합니다. 둘째, 실제 데이터에 대한 유사성 측정에 대한 제약이 필요합니다. 셋째, 학습 알고리즘이 실제 개념에 수렴된다는 보장을 얻기 위해 예제의 분포가 제한되는 경우가 많습니다.

우리는 이러한 측면이 확률론적 형식적 방법, 즉 형식적 제약 조건과 배포 요구 사항에 따라 데이터를 생성하기 위한 확률론적 알고리즘을 통해 해결될 수 있다고 믿습니다. 임의의 문자열(예)을 생성하는 제어된 즉흥 연주라는 새로운 종류의 새로운 기술이 유망합니다.

생성 방법을 정의하는 소프트 제약 조건, 우리는 이제 막 계산 복잡성과 효율적인 알고리즘 설계를 이해하기 시작했습니다. 임시변통은 제한된 무작위 샘플링, 모델 계산, 확률 프로그래밍에 기반한 생성 방법과 같은 계산 문제의 최근 발전에 의존합니다.
• 5.2 정량적 검증
• ​
전통적인 지표(상태 공간 차원, 구성 요소 수 등)를 통해 AI 시스템의 규모를 측정하는 것 외에도 구성 요소 유형이 훨씬 더 복잡할 수 있습니다. . 예를 들어, 자율 및 반자율 차량과 그 컨트롤러는 개별 및 연속 역학을 결합한 하이브리드 시스템으로 모델링되어야 하며, 환경(인간, 기타 차량)의 대표자는 확률적 프로세스로 모델링되어야 할 수도 있습니다. 마지막으로 요구 사항에는 안전성과 활성도에 대한 전통적인 부울 사양뿐만 아니라 시스템 견고성과 성능에 대한 정량적 요구 사항도 포함될 수 있지만 대부분의 기존 검증 방법은 부울 검증 질문에 답하는 것을 목표로 합니다. 이러한 격차를 해결하려면 정량적 검증을 위한 새로운 확장 가능한 엔진을 개발해야 합니다.
정량적 의미 분석. 일반적으로 AI 시스템의 복잡성과 이질성은 표준 형식 검증(부울 또는 정량적)이 결정 불가능하다는 것을 의미합니다. 예를 들어 선형 하이브리드 시스템의 상태에 도달할 수 있는지 여부를 결정하는 것조차 결정 불가능합니다. 계산 복잡성으로 인한 이러한 장애물을 극복하려면 의미론적 특징 공간에 대한 확률적 및 정량적 검증을 위한 새로운 기술을 사용하여 이 섹션의 앞부분에서 설명한 추상화 및 모델링 접근 방식을 향상해야 합니다. 부울 의미론과 정량적 의미론을 모두 갖춘 표준 형식론의 경우, 미터법 시간 논리와 같은 형식론에서 검증을 최적화로 공식화하는 것은 공식 방법의 계산 방법과 최적화 문헌의 계산 방법을 통합하는 데 중요합니다. 예를 들어 시뮬레이션 기반 시간 논리 위조에서는 효율성을 위해 의미론적 특징 공간에 적용해야 하지만 이러한 위조 기술을 사용하여 ML 구성 요소에 대한 훈련 데이터를 체계적이고 적대적으로 생성할 수도 있습니다. 확률론적 검증 기술은 의미론적 특징 공간에 대한 확률론적 프로그램을 검증하기 위해 Markov 체인 또는 MDP와 같은 전통적인 형식을 넘어서야 합니다. 마찬가지로 비용 제약을 보다 효율적으로 처리하려면 SMT 해결 작업을 확장해야 합니다. 즉, SMT 해결과 최적화 방법을 결합해야 합니다.

우리는 디자인 타임에 무엇을 보장할 수 있는지, 디자인 프로세스가 런타임 시 안전한 작동에 어떻게 기여하는지, 디자인 타임과 런타임 기술이 어떻게 효과적으로 상호 운용될 수 있는지 이해해야 합니다.

5.3 AI/ML을 위한 조합 추론 ​

공식 방법을 대규모 시스템으로 확장하려면 조합(모듈식) 추론이 필수적입니다. 구성 검증에서는 대규모 시스템(예: 프로그램)을 구성 요소(예: 프로그램)로 분할하고 각 구성 요소를 사양에 대해 검증한 다음 구성 요소 사양을 모아 시스템 수준 사양을 생성합니다. 조합 검증에 대한 일반적인 접근 방식은 가정 보장 계약을 사용하는 것입니다. 예를 들어 프로세스는 시작 상태(전제 조건)에 대해 가정하고 이는 결국 최종 상태(사후 조건)를 보장합니다. 동시 소프트웨어 및 하드웨어 시스템을 적용합니다.

그러나 이러한 패러다임은 "형식 사양" 섹션에서 설명한 인공 지능 시스템의 형식화 문제로 인해 인공 지능 시스템을 다루지 않습니다. 구성 가능 검증에는 구성 사양이 필요합니다. 즉, 구성 요소는 형식화 가능해야 합니다. 그러나 "공식 사양"에 설명된 대로 지각 구성 요소의 올바른 동작을 공식적으로 지정하는 것이 불가능할 수도 있습니다. 따라서 과제 중 하나는 완전한 조합 사양을 갖는 데 의존하지 않는 조합 추론 기술을 개발하는 것입니다. 또한 AI 시스템의 정량적, 확률적 특성으로 인해 조합 추론 이론을 정량적 시스템 및 사양으로 확장해야 합니다.

구성요소 계약을 추론합니다. AI 시스템의 조합 설계 및 분석에는 여러 측면의 진전이 필요합니다. 첫째, 이러한 시스템의 의미 공간에 대한 확률적 보장의 설계 및 검증을 위한 이론을 개발하기 위해 몇 가지 유망한 예비 작업을 구축할 필요가 있습니다. 둘째, 규범적 부담을 줄이고 조합 추론을 촉진하는 가설 보증 계약을 알고리즘적으로 생성하기 위한 새로운 귀납적 합성 기술을 고안해야 합니다. 셋째, 컴포넌트가 정확한 형식적 사양을 갖고 있지 않은 인식과 같은 경우를 처리하기 위해 시스템 수준 분석에서 컴포넌트 수준 제약 조건을 추론하고, 이러한 제약 조건을 사용하여 적대적 분석을 포함한 컴포넌트 수준 분석을 검색에 집중하는 기술을 제안합니다. 공간의 "관련"부분.

구축됨에 따라 수정되는 지능형 시스템

이상적인 세계에서는 검증이 설계 프로세스와 통합되므로 시스템이 '구축됨에 따라 수정'됩니다. 예를 들어 집적 회로에서 일반적인 RTL(레지스터 전송 수준) 설계 흐름을 가정하여 검증은 컴파일/합성 단계와 인터리브될 수 있으며 구현이 사양을 충족하는지 확인하기 위해 합성 알고리즘에 통합될 수도 있습니다. 구축 과정에서 점진적으로 수정되는 인공지능 시스템에 적합한 설계 프로세스를 설계할 수 있을까요?

6.1 ML 구성 요소의 사양 기반 설계

정식 사양이 주어지면 사양을 만족한다고 입증할 수 있는 기계 학습 구성 요소(모델)를 설계할 수 있습니까? 이 새로운 ML 구성 요소의 설계에는 (1) 데이터 세트 설계, (2) 모델 구조 합성, (3) 대표 기능 세트 생성, (4) 하이퍼파라미터 및 기타 선택 사항 합성 등 여러 측면이 있습니다. ML 알고리즘 측면 및 (5) 합성이 실패할 때 ML 모델 또는 사양의 디버깅을 자동화하는 기술입니다.

ML 구성요소의 형식적 합성. 앞서 나열된 일부 문제에 대한 솔루션이 등장하고 있습니다. 의미 손실 기능이나 인증된 견고성을 사용하여 ML 모델에 속성을 적용할 수 있으며, 이러한 기술을 신경 아키텍처 검색과 결합하여 올바르게 구성된 모델을 생성할 수 있습니다. 또 다른 접근법은 형식적 귀납적 합성, 즉 형식 사양을 만족하는 프로그램 인스턴스로부터의 합성이라는 새로운 이론을 기반으로 합니다. 형식적 귀납적 합성 문제를 해결하는 가장 일반적인 방법은 오라클 기반 접근 방식을 사용하는 것입니다. 여기서 학습자는 그림 2의 예에서와 같이 쿼리에 응답하는 오라클과 쌍을 이루고 오라클은 다음과 같은 반례를 생성하는 위조자가 될 수 있습니다. 학습 구성 요소가 어떻게 오작동하는지 보여줍니다. 시스템 수준 사양을 위반합니다. 마지막으로, ML 모델을 훈련하는 데 사용되는 알고리즘의 정확성을 보장하기 위해 증명된 정리를 사용하는 것도 수정된 ML 구성 요소를 구성하는 데 중요한 단계입니다.

6.2 기계 학습 기반 시스템 설계​

두 번째 과제는 학습 구성 요소와 비학습 구성 요소를 포함하는 전체 시스템을 설계하는 것입니다. 몇 가지 연구 질문이 제기되었습니다. ML 구성 요소의 작동을 제한할 수 있는 안전한 범위를 계산할 수 있습니까? 입력으로 받는 ML 인식 구성 요소의 한계를 극복하는 제어 또는 계획 알고리즘을 설계할 수 있습니까? 인공지능 시스템을 위한 조합 설계 이론을 고안할 수 있을까? 두 가지 ML 모델을 사용하여 두 가지 유형의 센서 데이터(예: LiDAR 및 시각적 이미지)를 감지하고 각 모델이 특정 가정 하에 사양을 충족하는 경우, 두 모델을 함께 사용하여 전반적인 시스템 안정성을 향상시킬 수 있는 조건은 무엇입니까?

이 과제에 대한 진전의 두드러진 예는 안전한 학습 기반 제어에 대한 작업입니다. 이 접근 방식은 안전 범위를 사전 계산하고 학습 알고리즘을 사용하여 해당 범위 내에서 컨트롤러를 조정하므로 도달 가능성 분석 등을 기반으로 이러한 안전 범위를 효율적으로 계산하는 기술이 필요합니다. 안전 RL 분야에서도 상당한 진전이 이루어졌습니다. .

그러나 이는 인식 및 예측을 위한 기계 학습이 제기하는 과제를 완전히 해결하지 못합니다. 예를 들어 입증된 안전한 엔드 투 엔드 심층 강화 학습은 아직 달성되지 않았습니다.

6.3 복원력 있는 AI를 위한 설계 시간 및 런타임 연결 ​

환경 모델링 섹션에서 설명한 것처럼 많은 AI 시스템은 선험적으로 지정할 수 없는 환경에서 작동하므로 항상 다음과 같은 상황이 발생합니다. 정확성을 보장할 수 없습니다. 런타임에 내결함성과 오류 복구를 구현하는 기술은 인공지능 시스템에서 중요한 역할을 합니다. 우리는 디자인 타임에 무엇을 보장할 수 있는지, 디자인 프로세스가 런타임 시 AI 시스템의 안전하고 올바른 작동에 어떻게 기여하는지, 디자인 타임과 런타임 기술이 어떻게 효과적으로 상호 운용될 수 있는지에 대한 체계적인 이해가 필요합니다.

이와 관련하여 내결함성 및 신뢰성 있는 시스템에 관한 문헌은 런타임 보증 기술을 개발하기 위한 기초를 제공합니다. 즉, 런타임 검증 및 완화 기술을 결합하는 방법을 제공합니다. 복잡하지만 쉬움 결함이 있는 모듈을 안전하고 공식적으로 검증된 백업 모듈과 결합하는 접근 방식입니다. 최근에는 디자인 타임과 런타임 보증 접근 방식을 결합한 기술을 통해 AI 및 ML 기반 구성 요소를 포함하여 검증되지 않은 구성 요소를 런타임 보증 프레임워크에 래핑하여 안전한 작동을 보장할 수 있음이 나타났습니다. 그러나 현재 이는 특정 클래스의 시스템으로 제한되거나 런타임 모니터 및 완화 전략의 수동 설계가 필요합니다. 내부 환경 모델링, 인공 지능 기반 모니터 및 안전한 대체 전략의 합성과 같은 접근 방식이 더 많이 제공될 예정입니다. 많은 일을 해야 합니다.

여기에서 논의된 건설 중인 지능형 시스템을 수정하는 설계 접근 방식은 성능 및 실시간 요구 사항을 충족하기 더 어렵게 만드는 오버헤드를 도입할 수 있습니다. 그러나 우리는 공식적인 방법이 다음과 같은 의미에서 시스템의 성능이나 에너지 효율성을 향상시키는 데 도움이 될 수 있다고 (아마도 비직관적으로) 믿습니다.

기존 성능 튜닝은 상황에 구애받지 않는 경향이 있습니다. 예를 들어 작업은 실행되는 환경과 관계없이 마감일을 준수해야 합니다. 그러나 이러한 환경이 디자인 타임에 공식적으로 특성화되고 런타임에 모니터링되며 시스템 작동이 안전한 것으로 공식적으로 검증된다면 이러한 환경에서 ML 모델은 더 높은 효율성을 위해 정확성을 교환할 수 있습니다. 이러한 절충안은 향후 연구에 유익한 영역이 될 수 있습니다.

결론

공식적 방법론 관점에서 우리는 높은 보증의 인공 지능 시스템 설계 문제를 분석했습니다. 그림 3에서 볼 수 있듯이 우리는 AI 시스템에 정형적 방법을 적용하는 데 있어 5가지 주요 과제를 식별하고 이 과제를 해결할 수 있는 5가지 과제 각각에 대해 3가지 설계 및 검증 원칙을 개발했습니다.

그림 3의 가장자리는 모니터링 가능한 가정과 환경 모델을 추출하기 위한 자체 검사 및 데이터 기반 환경 모델링에 의존하는 런타임 보장과 같은 이러한 원칙 간의 종속성을 보여줍니다. 마찬가지로, 시스템 수준 분석을 수행하려면 조합 추론 및 추상화에 참여해야 합니다. 여기서 일부 AI 구성 요소는 마이닝 사양이 필요할 수 있고 다른 구성 요소는 형식적 귀납적 합성을 통해 올바른 구조를 생성할 수 있습니다.

저자를 포함한 몇몇 연구자들은 이 기사의 원본 출판 버전에서 몇 가지 샘플 진행 상황을 제시한 2016년부터 이러한 과제에 대해 연구해 왔습니다. 우리는 이 기사에 설명된 원리를 기반으로 기술을 구현하고 자율 주행 및 항공우주 분야의 산업 규모 시스템에 적용되는 오픈 소스 도구 VerifAI 및 Scenic을 개발했습니다. 이러한 결과는 시작에 불과하며 앞으로 해야 할 일이 많이 남아 있습니다. 검증 가능한 AI는 앞으로도 계속해서 유익한 연구 분야가 될 것으로 예상됩니다.

위 내용은 검증 가능한 AI를 향하여: 형식적 방법의 5가지 과제의 상세 내용입니다. 자세한 내용은 PHP 중국어 웹사이트의 기타 관련 기사를 참조하세요!