New paradigm of software by AI. nondeterminism problem in safety critical system(AI에 의한 소프트웨어의 새로운 패러다임. safety critical system에서의 nondeterminism문제)


한글버전은 아래로.Korean version is below.

When I studied the formal specification at the time of my Ph.D., I considered the deterministic nature of the system to be very important in terms of predictability and testability of the system. I do not think anyone would ever want to put a system into a system that does not know where to go.

A system based on AI can not perform an exhaustive test by default. However, in an exceptional situation that has not been tested, the system can not know what to do.

Therefore, the test will inevitably reach its limit.

So what should you do?

Formal verification is required. The most important thing when formal verification was done is the accuracy and sufficiency of the specification. It is not easy to judge whether or not you have written this formally. Well, even if it is better than test.

You should verify on the line considering both formal verification and testing. The most important thing here is that you have to define the safety attributes formally and the run-time verifier should continue monitoring whether the attributes are maintained. This is not a test. And it will be impossible for all situations to be tested, and a separate supervisor should be software in a way that defines the boundary of the system’s behavior space and makes it behave in it.

In the old days, everything was checked as it was intended. In the meantime, the developer has created a fatalistic system. He knows everything about what to do in 10 seconds. But AI will not be able to manage it in the future.

The problem also comes down to how AI will not be dominated in the future. It may be a concern at this point, but it will not be a distant future for such concerns to come true.

The IEEE is doing some interesting work on this. I think we should be interested in the future.

Ethically Aligned Design: Prioritizing Wellbeing for Artificial Intelligence and Autonomous Systems

박사과정때 Formal specification에 대해 연구했을때, 시스템의 예측 가능성과 테스트 가능성의 관점에서 시스템의 deterministic한 속성은 매우 중요하다고 생각했다. 어디로 튈지 모르는 시스템을 만들어놓고, 그 시스템에 자기의 목숨을 걸고 싶은 사람은 없을거라 생각한다.

AI에 의한 시스템은 기본적으로 test에 의해 exhaustive test를 수행하지 못한다. 그러나 미처 시험하지 않은 예외적 상황에서 시스템이 어떤 행동을 할 지 알 수 없다.

그러므로, test는 불가피하게도 한계를 맞이할 수 밖에 없을 것이다.

그러면 무엇을 해야 할 것인가?

formal verification을 해야 한다. formal verification을 수행했을 당시 가장 중요한 것은 specification의 정확성과 충분성이다. 과연 이 정도로 formal하게 기술했느냐를 판단하는 것이 쉽지 않다. 뭐, 그렇긴 하더라도 test보다야 낫다.

formal verification과 test의 양쪽을 다 고려해서 run-time verification을 해야 한다. 여기서 가장 중요한 것은 safety에 의한 속성을 잘 정의해야 하고, 그 속성이 유지되는지를 run-time verifier는 모니터링을 계속해야 할 것이다. 이것은 시험이 아니다. 그리고 모든 상황을 고려한 시험은 이제 불가능하게 될 것이고, 별도의 supervisor가 시스템의 행동 space의 boundary를 정하고 그 안에서 행동하도록 하는 방식의 소프트웨어가 되어야 할 것이다.

예전에는 모든 것을 의도한대로 일일이 다 점검했다. 그동안 개발자는 운명론적인 시스템을 만들어서 1초 뒤에, 10초 뒤에 어떤 일을 할 지에 대해서 모든 것을 알 수 있었다. 하지만 AI에 의해 앞으로 그런 방식의 관리는 불가능하게 될 것이다.

이 문제는 또한 향후 AI를 어떻게 감시해야 AI의 지배를 받지 않게 될 것인가하고도 맞닿아 있다. 현재 시점에서는 우려일 수 있으나, 그런 우려가 현실이 되는 것은 그리 먼 미래가 아닐 것이다.

IEEE에서 이와 관련된 흥미로운 작업을 하고 있다. 앞으로 관심을 가져야 할 것이라 생각한다.

Ethically Aligned Design: Prioritizing Wellbeing for Artificial Intelligence and Autonomous Systems

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s