Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar

이 논문은 Isabelle/HOL 에서의 절차적 'apply-style' 증명 스크립트를 가독성과 견고성이 높은 선언적 Isar 증명 형식으로 자동 변환하는 'Apply2Isar' 도구를 제안하고, Isabelle 공식 증명 아카이브의 대규모 벤치마크를 통해 그 유효성을 검증합니다.

핵심

이 논문은 **이사벨 (Isabelle/HOL)**이라는 수학적 증명 도구를 사용하는 사람들을 위해 만든 **'Apply2Isar'**라는 도구에 대해 설명합니다.

이걸 쉽게 비유해서 설명해 드릴게요.

🏗️ 비유: "임시 가설 (Apply-Style)" vs "완성된 건축도면 (Structured Isar)"

수학 증명을 작성할 때, 두 가지 방식이 있습니다.

1. Apply-Style (적용 스타일):

   • 비유: "일단 저 벽을 치고, 그다음 창문 내고, 문 붙여보자!"라고 즉흥적으로 건물을 짓는 방식입니다.
   • 특징: 빠르게 아이디어를 테스트하고 실험하기 좋습니다. 하지만 건물이 완성된 후, "어? 이 기둥이 왜 여기 있지? 이 벽을 치면 저기 문이 무너지는데?"라고 뒤늦게 문제를 발견하기 쉽습니다. 수정하기도 매우 어렵습니다.
   • 문제점: 나중에 누군가 (또는 미래의 본인) 가 이 증명을 다시 읽으면, "도대체 왜 이렇게 했지?"라고 혼란을 겪습니다.

2. Structured Isar (구조화된 Isar):

   • 비유: "1 층은 거실, 2 층은 침실, 3 층은 다락방"이라고 명확한 도면을 그려가며 짓는 방식입니다.
   • 특징: 처음부터 끝까지 논리가 명확하게 드러납니다. 나중에 수정할 때도 "2 층 침실만 고치면 되네"라고 쉽게 파악할 수 있습니다.
   • 장점: 읽기 쉽고, 튼튼하며, 유지보수가 쉽습니다.

🚀 Apply2Isar 가 하는 일: "임시 건물을 명품 아파트로 자동 리모델링"

문제는 많은 수학자들이 **빠른 실험을 위해 '일시적 스타일 (Apply-Style)'**로 증명을 먼저 작성한다는 점입니다. 하지만 나중에 이걸 **명품 아파트 (Isar)**로 바꾸려면, 모든 벽을 하나하나 뜯어내어 다시 쌓아야 하는 엄청난 수고를 해야 합니다.

여기서 Apply2Isar가 등장합니다!

• 역할: 사용자가 작성한 "임시 가설 (Apply-Style)" 증명 코드를 받아서, 자동으로 "명품 아파트 도면 (Structured Isar)"으로 바꿔주는 자동 리모델링 로봇입니다.
• 작동 원리:
  1. 로봇이 사용자의 증명 과정을 다시 실행 (재연) 해봅니다.
  2. 각 단계에서 "지금 어떤 상태인가?"를 기록합니다.
  3. 그 기록을 바탕으로, 논리가 명확하게 드러나는 새로운 도면 (Isar 코드) 을 뒤집어서 작성합니다.

🛠️ 로봇이 겪는 어려움 (기술적 난제들)

이 로봇은 단순히 코드를 복사하는 게 아니라, 논리의 흐름을 이해해야 하므로 몇 가지 까다로운 상황을 맞닥뜨립니다.

• 한 번에 여러 문제 해결하기: 어떤 명령은 한 번에 10 개의 문제를 해결합니다. 로봇은 "어떤 명령이 어떤 문제를 해결했는지" 정확히 구분해서 도면에 적어야 합니다. (마치 "이 벽은 거실과 주방을 동시에 지었다"고 적는 것 같습니다.)
• 이름 충돌: 증명 과정에서 변수 이름이 겹치는 경우가 있습니다. 로봇은 "이름이 같은 두 사람이 다른 사람인데, 혼동하지 않도록 이름을 바꿔줘야겠다"라고 판단합니다.
• 미완성된 증명: 때로는 "이건 나중에 해결할게 (Sorry)"라고 미루는 부분이 있을 수 있습니다. 로봇은 이 부분도 잘 처리해서 전체 구조를 유지합니다.

📊 결과: 얼마나 잘 작동할까?

저자들은 이 도구를 **이사벨의 공식 증명 자료집 (AFP)**에 있는 수천 개의 증명 코드로 테스트했습니다.

• 성공률: 테스트한 증명의 **95%~99%**에서 완벽하거나 거의 완벽하게 변환에 성공했습니다.
• 의미: 수학자들은 이제 "일단 빠르게 증명해놓고, Apply2Isar 로 깔끔하게 정리하자!"라고 생각할 수 있게 되었습니다.

💡 결론

이 논문은 "빠르게 아이디어를 구현하는 것 (Apply-Style)"과 "오래 두고 읽기 좋은 코드를 만드는 것 (Isar)"이라는 두 마리 토끼를 모두 잡을 수 있는 방법을 제시합니다.

마치 요리사가 실험실에서는 재료를 대충 섞어보지만 (Apply-Style), 최종 메뉴판에는 **정갈하게 정리된 레시피 (Isar)**를 올리는 것과 같습니다. Apply2Isar 는 그 정갈한 레시피를 자동으로 만들어주는 비서 역할을 합니다.

이 도구를 통해 수학 증명 코드는 더 읽기 쉬워지고, 수정하기 편해지며, 더 튼튼해질 것입니다.

기술 요약

1. 문제 정의 (Problem)

Isabelle/HOL 증명 도구는 두 가지 주요 스타일을 지원합니다:

• Apply-style (절차적 증명): apply 명령어를 사용하여 증명 상태를 역방향으로 조작하는 스크립트 방식입니다. 탐색 속도가 빠르고 복잡한 증명을 작성하기 쉽지만, 증명의 중간 상태를 명시적으로 보여주지 않아 가독성이 낮고, 증명 단계가 변경될 경우 (예: 규칙 순서 변경) 증명이 깨지기 쉽습니다 (Fragile).
• Structured Isar (선언적 증명): 중간 목표와 논리적 흐름을 명시적으로 서술하는 방식입니다. 가독성이 높고, 구조가 고정되어 있어 유지보수가 용이하며, Isabelle 공식 아카이브 (AFP) 에서 선호되는 방식입니다.

핵심 문제: 많은 사용자는 빠른 탐색을 위해 Apply-style 스크립트를 작성하지만, 이를 Isar 로 변환하려면 수동으로 각 단계의 중간 목표와 명령어를 복사하여 재작성해야 하는 번거로움이 있습니다. 이 수동 과정은 시간 소모가 크고 오류가 발생하기 쉽습니다.

2. 방법론 (Methodology)

저자들은 Apply2Isar라는 도구를 개발하여 Apply-style 스크립트를 자동으로 Isar 증명 코드로 변환합니다. 주요 구현 전략은 다음과 같습니다.

• 증명 재연 (Proof Replay): Apply2Isar 는 입력된 Apply 스크립트를 Isabelle/ML 환경에서 실제로 실행 (replay) 하여 각 메서드 적용 후의 **중간 증명 상태 (goals)**를 기록합니다.
• 역방향 변환 (Reverse Construction): Isar 는 주로 순방향 추론 (forward reasoning) 에 적합하므로, 기록된 증명 상태를 역순으로 처리하여 Isar 코드를 생성합니다.
• 사실 (Fact) 연결: 생성된 Isar 증명에서 각 단계는 by (fact h)와 같은 명령어를 사용하여 이전 단계에서 증명된 사실을 다음 단계의 입력으로 연결합니다.
• AST 기반 파싱: 입력 스크립트를 커스텀 AST(추상 구문 트리) 로 파싱하고, 이를 Isar 요소로 변환하는 두 번째 AST 로 재구성한 후 문자열로 출력합니다.

주요 기술적 도전 과제 및 해결 방안:

1. 다중 목표 처리 (Multiple Goals): auto나 simp_all 같은 명령어는 여러 목표를 동시에 변경합니다. 이를 처리하기 위해 'smart_goals' 옵션을 도입하여 변경된 목표만 명시하거나, 모든 목표를 나열하는 방식을 선택적으로 지원합니다.
2. 증명 흐름 복잡성: subgoal, supply, using, unfolding 등의 명령어는 증명 흐름을 비선형적으로 만듭니다. Apply2Isar 는 subgoal 블록을 증명 블록의 최상위로 이동시키거나, note 명령어를 사용하여 사실을 명시적으로 정의함으로써 논리적 순서를 보장합니다.
3. 변수 가림 (Shadowing): subgoal 명령어는 메타 양화 변수를 skolemize 하는데, 이때 기존 변수 이름과 충돌할 수 있습니다. 이를 해결하기 위해 subgoal_fix_fresh 옵션을 통해 변수 이름을 자동으로 새로 생성하거나, 사용자가 수동 개입할 수 있도록 합니다.
4. 스케마틱 변수 (Schematic Variables): Apply 스크립트에서 미해결 변수 (schematic variables) 가 포함된 경우, Isar 의 have 명령어로 직접 변환할 수 없습니다. 이 경우 해당 구간은 Apply-style 스크립트 형태로 유지하거나 (partial translation), sorry 명령어로 처리하여 증명을 부분적으로 완성합니다.
5. 타입 정보 손실 방지: 증명 상태 간에 타입 정보가 손실될 수 있으므로, print_types 옵션을 통해 필요한 경우 타입 어노테이션을 자동으로 추가합니다.

3. 주요 기여 (Key Contributions)

• 자동 변환 도구 개발: Isabelle/HOL 사용자를 위해 Apply-style 스크립트를 Isar 로 자동 변환하는 첫 번째 도구인 Apply2Isar 를 구현 및 공개했습니다.
• 가독성과 견고성 향상: 변환된 증명은 기계적으로 생성되었음에도 불구하고, Isar 의 선언적 특성을 활용하여 증명의 구조와 논리적 흐름을 명확히 보여줍니다. 이는 증명 유지보수성을 크게 향상시킵니다.
• 포괄적인 명령어 지원: Table 1 에 나열된 바와 같이 apply, by, subgoal, unfolding, using 등 Isabelle 의 주요 절차적 명령어들을 광범위하게 지원합니다.
• 부분 변환 (Partial Translation) 전략: 완전히 변환할 수 없는 경우 (예: 복잡한 스케마틱 변수) 에는 해당 부분을 Apply-style 로 유지하거나 sorry 로 처리하여 전체 증명의 구조를 보존하는 유연한 전략을 제시합니다.

4. 평가 결과 (Results)

저자들은 Isabelle 의 공식 아카이브 (AFP) 에 있는 5 개의 주요 엔트리 (Group-Ring-Module, AutoCorres2 등) 에서 4,461 개의 Apply-style 증명을 대상으로 도구를 평가했습니다.

• 성공률: 전체 테스트 케이스의 **95%~99%**에서 완전 또는 부분 변환에 성공했습니다.
• 성공/실패 분석:
  • 성공 (Successes): 대부분의 증명이 성공적으로 Isar 로 변환되었습니다.
  • 부분 변환 (Partial Translations): 스케마틱 변수가 포함된 경우 등 일부 단계가 Apply-style 로 남았으나, 전체 구조는 Isar 를 따랐습니다.
  • 실패 (Fails): 실패의 주된 원인은 Isabelle 의 용어 (term) 출력 및 재파싱 메커니즘의 불일치 (custom syntax 사용 시 등) 였으며, 이는 도구 자체의 한계라기보다 Isabelle 내부의 문제였습니다. 타임아웃은 드물게 발생했습니다.
• 성능: 30 초 타임아웃 제한 하에서 대부분의 증명을 처리했으며, 350 개 이상의 명령어로 구성된 긴 증명도 성공적으로 변환했습니다.

5. 의의 및 결론 (Significance & Conclusion)

• 실용성: Apply2Isar 는 기존 증명을 Isar 로 리팩토링하는 데 드는 막대한 수동 작업을 제거하여, Isabelle/HOL 생태계의 증명 품질과 유지보수성을 높이는 데 기여합니다.
• 확장성: 이 도구는 LLM 기반의 Isabelle Assistant 와 같은 최신 도구와 비교할 때, **결정론적 (deterministic)**이고 로컬 환경에서 실행 가능하다는 장점이 있습니다.
• 미래 작업: 스케마틱 변수 처리 개선, 커스텀 명령어 지원, 그리고 'Deautomation'(자동화된 증명을 더 단순한 단계로 분해) 기술과의 통합 등을 통해 도구의 기능을 확장할 계획입니다.

요약하자면, Apply2Isar 는 Isabelle 사용자들이 절차적 스크립트의 유연함과 선언적 Isar 의 견고함을 모두 누릴 수 있게 해주는 필수적인 자동화 도구로, Isabelle/HOL 증명 개발의 효율성을 크게 증진시켰습니다.