Not Letting Proofs Die: xLaDe, a Lean 4 Ecosystem Framework

현대 수학과 소프트웨어 공학의 세계에는 증명과 프로그램을 컴퓨터가 절대적인 정확성을 검사할 수 있는 방식으로 작성하려는 움직임이 커지고 있습니다. 복잡한 논증에서 실수를 찾아내기 위해 인간의 눈에 의존하는 대신, 연구자들은 증명 보조기라고 불리는 특화된 소프트웨어 도구를 사용합니다. 이 프로그램들은 엄격한 편집자 역할을 수행하며, 결과가 의심의 여지 없이 참임을 보장하기 위해 모든 개별 논리 단계를 검증합니다. Lean 4와 같은 시스템은 이러한 작업을 위해 인기를 얻었으며, 대규모 팀이 검증된 수학 및 보안 소프트웨어의 방대한 라이브러리를 구축할 수 있도록 해줍니다. 그러나 이러한 도구들은 끊임없이 업데이트되고 개선됩니다. 하나의 설계도로 지은 집이 내일 건설 규칙이 바뀐다고 해서 무너지지 않을 수도 있는 것처럼, 오늘 완벽하게 작동하는 수학적 증명이라도 소프트웨어 버전이 바뀌면 내일 실행되지 않을 수 있습니다. 이는 과학의 장기적인 역사에 문제를 일으킵니다. 만약 도구가 너무 빠르게 진화한다면, 오늘 수행된 작업은 미래에 재현하거나 이해하는 것이 불가능해질 수 있기 때문입니다.

안드라 프라데시 중앙 대학교의 연구팀은 소프트웨어의 변화를 막는 것이 아니라, 그 주변에 보호 계층을 구축함으로써 이 과제를 해결하는 새로운 방법을 제안했습니다. 그들은 자신들의 창조물을 xLaDe, 즉 '실험적 Lean 4 고급 개발 생태계(Experimental Lean 4 Advanced Development Ecosystem)'라고 부릅니다. xLaDe는 기존의 Lean 소프트웨어를 고정시키거나 동일하게 유지하도록 강요하는 대신, 기존 도구 위에 위치하는 정교한 기록 및 관리 시스템 역할을 합니다. 이 시스템의 목표는 핵심 소프트웨어를 견고하고 변경 불가능한 토대로 취급하면서, 그 상단의 표면 위에서 연구자들이 자유롭게 실험할 수 있도록 하는 것입니다. 이 프레임워크는 증명이 실행된 구체적인 방식—사용된 특정 소프트웨어 버전, 종속성, 그리고 환경의 정확한 조건—을 포착하도록 설계되어, 설령 기반이 되는 도구들이 변하더라도 몇 년 후에 작업을 재구성할 수 있도록 합니다.

xLaDe의 핵심 아이디어는 시스템의 신뢰할 수 있는 심장부와 그 주변에서 일어나는 실험적 작업 사이의 엄격한 분리입니다. 연구자들은 Lean 소프트웨어 자체를 불변의 인프라로 취급하며, 이는 실험에 의해 결코 수정될 수 없음을 의미합니다. 대신, xLaDe는 외부 프로젝트의 소스 코드를 건드리지 않고 그 주변을 감싸는 도구 세트인 오케스트레이션 레이어로 작동합니다. 이러한 접근 방식은 과학자들이 수학적 증명의 무결성을 위협하지 않으면서도 새로운 아이디어를 테스트하고, 워크플로우를 변경하며, 작업 조직의 다양한 방식을 시도할 수 있게 해줍니다. 만약 실험이 잘못되거나 폐기되어야 할 경우, 그것은 흔적을 남기거나 프로젝트의 안정적인 부분에 영향을 주지 않고 깔끔하게 제거될 수 있습니다. 이러한 가역성은 연구자들이 자신의 작업을 영구적으로 망가뜨릴 걱정 없이 새로운 시도를 할 수 있도록 독려하는 데 매우 중요합니다.

이 시스템을 사용 가능하게 만들기 위해, 연구팀은 사용자를 위한 주요 인터페이스 역할을 하는 명령줄 도구를 구축했습니다. 이 도구는 다양한 필요를 충족하기 위해 서로 다른 '모드'의 운영을 관리합니다. 초보자에게 부드러운 안내를 제공하는 온보딩 모드, 연구자가 새로운 워크플로우와 정책을 테스트할 수 있는 실험 모드, 그리고 신뢰할 수 있는 장기적 사용을 위해 상황을 고정하는 안정 모드가 있습니다. 안정 모드에서는 아무것도 예기치 않게 변경되지 않도록 엄격한 규칙을 적용하여 연구 결과를 보존하는 데 이상적입니다. 또한 이 도구는 실험이 실행된 시간과 관련된 특정 소프트웨어 버전과 같은 메타데이터를 자동으로 기록하여 상세한 감사 추적(audit trail)을 생성합니다. 이를 통해 미래에 누군가가 이 작업을 살펴볼 때, 어떻게 수행되었는지 정확히 알 수 있고 재현하는 데 필요한 정보를 가질 수 있도록 보장합니다.

연구진은 이 프레워크가 실제로 작동하는지 확인하기 위해 두 가지 구체적인 실험으로 테스트를 진행했습니다. 첫 번째 테스트에서는 연구를 위해 특별히 제작된 작고 독립적인 프로젝트를 xLaDe 시스템 안에 담았습니다. 그들은 원본 코드를 단 한 줄도 변경하지 않고 프레임워크를 통해 프로젝트의 빌드 프로세스를 실행했습니다. 시스템은 증명을 성공적으로 컴파일하고 결과를 기록했으며, 이는 프레임워크 자체가 프로젝트를 완전히 분리된 상태로 유지하면서 외부 프로젝트를 관리할 수 있음을 입증했습니다. 두 번째로 더 엄격한 테스트에서는 팀 외부의 인물이 만든 Lean 4에 대한 완전히 독립적인 교육 과정을 동일한 방식으로 적용했습니다. 이 프로젝트는 xLaDe와 이전에 아무런 관계가 없었습니다. 프레임워크는 해당 과정의 파일이나 Lean 소프트웨어를 수정하지 않고도 과정을 통합하고, 빌드 프로세스를 실행하며, 정상 작동을 검증했습니다. 이러한 결과는 이 시스템이 보편적인 래퍼(wrapper)로서 기능하여, 다양한 프로젝트가 공통된 규칙 아래에서 관리되고 재현될 수 있음을 시사합니다.

보안과 신뢰는 xLaDe 설계의 중심입니다. 연구진은 컴퓨터가 해킹당하거나 코드에 접근 권한이 있는 악의적인 내부자가 있는 것과 같은 모든 가능한 위협을 방어할 수는 없다는 점을 인정합니다. 대신, 그들은 투명성과 검증에 집중합니다. 시스템은 코드를 호스팅하기 위해 여러 미러(mirrors)를 사용하여, 한 웹사이트가 다운되더라도 프로젝트에 계속 접근할 수 있도록 합니다. 또한 암호화 키와 체크섬(checksums)을 공개하는데, 이는 사용자가 다운로드한 파일이 저자가 의도한 것과 정확히 일치하는지 확인할 수 있게 해주는 디지털 지문입니다. 이 보안 모델의 핵심은 핵심 Lean 소프트웨어를 수정하려는 모든 시도를 자동으로 감지하는 것입니다. 만약 스크립트나 사용자가 변경 불가능한 토대를 변경하려고 시도하면, 시스템은 위반을 감지하고 프로세스를 중단하여 실험적 도구에 의해 수학적 증명의 무결성이 결코 훼손되지 않도록 보장합니다.

논문은 xLaDe가 아직 실험적인 프로젝트이며 완성된 솔루션은 아니지만, 형식 검증(formal verification)의 미래를 향한 유망한 경로를 제공한다고 결론짓습니다. 이 시스템은 오래된 코드가 새로운 도구와 강제로 호환되도록 만드는 하위 호환성 문제를 해결하겠다고 주장하지 않습니다. 대신, 코드가 작성된 맥락을 보존한다는 다른 해결책을 제시합니다. 환경을 기록하고 실험을 일급 연구 산물(first-class research artifacts)로 취급함으로써, 이 프레임워크는 커뮤니티가 확신을 가지고 과거의 결과들을 다시 살펴볼 수 있게 해줍니다. 저자들은 자신들의 작업이 생태계 연구를 수행하기 위한 방법론임을 강조하며, 아이디어를 테스트하고, 실패를 기록하며, 성공적인 도구를 공유할 수 있는 구조화된 방식을 제공한다고 말합니다. 이러한 접근 방식을 통해, 그들은 증명 보조기의 급격한 진화가 그 위에 구축된 가치 있는 작업들을 잃게 되는 대가로 이어지지 않는 지속 가능한 환경을 만들고자 합니다.