Relative formalization in Isabelle/HOL of a result in inverse problems

물리학과 공학의 세계에는 역문제(inverse problems)라고 불리는 일종의 퍼즐이 존재한다. 당신이 밀봉된 불투명한 상자 밖에 서 있다고 상상해 보라. 당신은 상자 내부를 볼 수 없지만, 표면을 만지고 그 위로 흐르는 전기를 측정할 수 있다. 한 지점에 전압을 가하고 다른 지점에서 발생하는 전류를 측정함으로써, 당신은 일련의 데이터를 수집한다. 역문제는 이 외부 측정값들을 바탕으로, 숨겨진 물체의 정확한 형태와 재질 특성을 재구성할 수 있는가 하는 문제이다. 이것은 단순히 이론적인 유희가 아니다. 이는 의료 영상, 석유 탐사, 그리고 재료의 비파괴 검사의 배후에 있는 수학적 엔진이다. 문제는 서로 다른 내부 구조들이 거의 동일한 외부 신호를 만들어낼 수 있다는 점이며, 이로 인해 매우 구체적인 조건 없이는 해결책을 찾는 것이 불안정하거나 불가능해질 수 있다는 데 있다.

이러한 퍼즐을 복잡하게 만드는 한 가지 특정 유형의 재료는, 한 영역에서 다음 영역으로 넘어갈 때 전기 전도 능력이 급격히 변하는 서로 다른 영역들로 구성된 복합체이다. 만약 이 영역들이 단순한 기하학적 블록 모양이고, 각 블크 내부의 재료 특성이 예측 가능한 매끄러운 패턴을 따른다면, 수학자들은 외부 측정값이 내부 배치를 식별하기에 충분할 것이라고 오랫동안 믿어 왔다. 그러나 이 믿음을 증명하는 것은 파동과 장(field)이 영역 사이의 경계에서 어떻게 행동하는지에 대한 복잡한 방정식과 가정들의 미로를 헤쳐나가는 과정을 필요로 한다. 수십 년 동안 이러한 증명들은 인간의 직관과, 손으로 검증하기에는 너무 번거로운 어떤 깊은 수학적 진리들을 수용하는 방식에 의존해 왔다.

최-린 I. 커르스테아(Cătălin I. Cârstea)의 최근 실험은 이 오래된 문제에 대해 다른 접근 방식을 취한다. 연구자는 오직 인간의 검증에만 의존하는 대신, 절대적인 정밀도로 수학적 논리를 점검하도록 설계된 컴퓨터 시스템을 사용했다. 목표는 이러한 조각 형태의 재료들에 관한 특정한 복잡한 정리를 컴퓨터가 이해하고 검증할 수 있는 언어로 번역하는 것이었다. 형식화(formalization)라고 알려진 이 과정은 수학적 논증을 아주 작고 원자적인 단계로 분해하여, 모든 논리적 도약이 컴퓨터가 참이라고 알고 있는 규칙에 의해 정당화되는지 확인하는 과정을 포함한다. 연구자는 모든 기저 사실을 처음부터 증명하려고 시도하지 않았다. 그렇게 했다면 수년이 걸렸을 것이기 때문이다. 대신 그는 주요 결과가 다른 확립된 수학적 진리라는 토대 위에 놓이도록 구조를 구축했으며, 컴퓨터는 이를 신뢰할 수 있는 구성 요소로 취급한다.

이 연구는 유한한 수의 영역으로 나뉜 경계가 있는 3차원 물체의 표면에서 두 개의 서로 다른 내부 전도도 패턴이 정확히 동일한 전기적 측정값을 생성한다면, 그 두 패턴은 반드시 동일해야 한다는 정리에 초점을 맞추었다. 해당 물체는 유한한 수의 영역으로 나뉘어 있으며, 각 영역 내에서 재료의 특성은 다항식, 즉 매끄럽고 예측 가능한 수학적 표현식으로 기술된다. 이 정리는 영역들이 특정한, 잘 정돈된 방식으로 배치되어 있고 측정이 표면의 충분히 넓은 부분에서 이루어지는 경우에 성립한다.

이를 달기 위해, 연구자는 인공지능 도구를 사용하여 원래 논문의 밀도 높고 전문적인 언어를 컴퓨터가 요구하는 엄격한 구문으로 번역하는 데 도움을 받았다. 이것은 단순한 복사 및 붙여넣기 작업이 아니었다. 이는 의미를 보존하면서 컴퓨터와 인간이 함께 협력하며 수행하는 신중하고 반복적인 과정이었다. 심판 역할을 하는 엄격한 레퍼리로서의 컴퓨터는 증명의 모든 단계를 점검하여, 결론이 시작된 가정과 신뢰할 수 있는 수학적 사실들로부터 논리적으로 도출되는지를 확인했다. 전체 과정은 번역에서 최종 검증에 이르기까지 일주일도 채 걸리지 않았으며, 이는 전통적인 방식으로는 지나치게 비용이 많이 들고 시간이 오래 걸리는 작업이었다.

결과는, 신뢰할 수 있는 수학적 사실들이 옳다고 가정할 때, 주요 정리가 옳다는 기계 검증 증명이다. 컴퓨터는 논리가 빈틈없이 유지됨을 확인했으며, 시작된 가정으로부터 결론이 논리적으로 따라온다는 것을 확인했다. 이것이 새로운 물리 법칙을 찾아내는 의미에서의 새로운 발견을 의미하는 것은 아니다. 오히려 이는 기존 결과에 대한 새로운 수준의 확실성을 부여하는 것이다. 이 실험은 현대적인 도구들의 도움을 받으면, 수년이 아닌 며칠 만에 복잡한 수학적 주장을 검증하는 것이 가능하다는 것을 보여주며, 검증 과정을 과학 및 공학의 다른 어려운 문제들에 적용할 수 있는 일상적인 단계로 변화시킨다.

논문은 또한 이 번의 과정에서 발생하는 어려움들을 강조한다. 원래의 수학 텍xt는 인간 독자를 위해 작성되었기 때문에, 컴퓨터가 결정을 내리는 데 필요한 세부 사항을 생략하는 경우가 많다. 연구자는 컴퓨터의 버전이 인간의 버전과 정확히 일치하도록 보장해야 했으며, 이 작업에는 번역을 여러 번 확인하고 도구들을 사용하여 불일치를 찾아내는 과정이 포함되었다. 최종 출력물은 누구나 컴퓨터 시스템에 접속하여 스스로 증명을 확인할 수 있는 코드와 논리적 진술들의 모음이다. 이러한 투명성은 저자의 명성이나 동료 검토 과정에서 오는 것이 아니라, 기계의 굴하지 않는 논리로부터 오는 새로운 종류의 확신을 제공한다.

궁극적으로, 이 연구는 개념 증명(proof of concept) 역할을 한다. 이는 복잡한 수학적 연구를 형식화하는 장벽이 낮아지고 있음을 보여주며, 정교한 이론적 토대에 의존하는 분야에 더 높은 수준의 검증을 가져오는 것을 가능하게 한다. 여기서 다룬 전기 전도도에 관한 특정 정리는 하나의 예시일 뿐이지만, 여기에 사용된 방법론은 가장 어려운 수학적 논증들도 과학 실험과 같은 수준의 정밀한 조사를 받을 수 있는 미래를 암시하며, 우리 이해의 토대가 보이는 것만큼 견고함을 보장한다.