Automated conjecturing with \emph{TxGraffiti}

"TxGraffiti 를 통한 자동 추측"의 기술적 요약

문제 제기
본 논문은 수학적 대상 (특히 그래프) 의 수치적 불변량 간의 수학적으로 유용하고, 중복되지 않으며, 해석 가능한 부등식을 생성하는 자동 추측의 과제를 다룹니다. 자동 증명기는 성숙한 분야이지만, 자동 추측 생성은 역사적으로 "지나치게 많은 진술" 문제에 직면해 왔습니다. 즉, 체계적인 열거가 데이터베이스상으로는 참이지만 사소하거나 중복된 방대한 수의 진술을 생성한다는 문제입니다. 목표는 이러한 진술들을 필터링하여 진정한 새로운 정보 (정보성) 를 제공하며 인간의 검토와 증명이 가능한 것들을 식별하는 것입니다.

방법론
본 논문은 유한한 버전 관리 스냅샷 테이블에서 작동하는 휴리스틱 및 최적화 기반 시스템인 TxGraffiti(텍사스 그래피티) 를 소개합니다. 이전 시스템인 Graffiti 와 Graffiti.pc 가 검색 중에 불변량을 동적으로 계산하는 것과 달리, TxGraffiti 는 증거 기반을 정적 산물 (artifact) 로 취급합니다.

추측 파이프라인은 다음 단계들로 구성됩니다:

1. 데이터 큐레이션 (스냅샷 테이블):

   • 행은 대상 (그래프) 을, 열은 사전 계산된 수치적 불변량 (예: 독립수 $\alpha$, 매칭수 $\mu$) 과 불리언 술어 (예: "연결되어 있다", "정규이다") 를 나타내는 테이블이 구성됩니다.
   • 큐레이션 전략은 무작위성보다 커버리지를 우선시하며, 특히 극단적 구성, 등식 증인 (sharp cases), 그리고 반례를 포함하여 테이블이 진단적으로 풍부하도록 합니다.

2. 최적화를 통한 후보 생성:

   • 선택된 목표 불변량 $\alpha$와 불리언 술어 $P$(가설) 에 대해, 시스템은 $\alpha \le mx + b$ 또는 $\alpha \ge mx + b$ 형태의 아핀 경계를 탐색합니다. 여기서 $x$는 예측자 불변량입니다.
   • 복잡한 표현 트리를 열거하는 대신, TxGraffiti 는 단순한 매개변수 가설 클래스 (단변수 아핀 경계) 를 고정하고 **선형 계획법 (LP)**을 풀어 계수를 적합시킵니다.
   • 상한선 LP: $P$를 만족하는 모든 행에 대해 $\alpha_i \le mx_i + b$를 조건으로 총 슬랙 $\sum (mx_i + b - \alpha_i)$을 최소화합니다.
   • 하한선 LP: $\alpha_i \ge mx_i + b$를 조건으로 총 슬랙을 최대화하거나 (또는 음의 슬랙을 최소화합니다).
   • 시스템은 파생 열 (예: $n-\mu$, $\Delta^2$) 로 스키마를 확장하여 다변량 경계와 비선형 관계도 지원하지만, 기본 웹 인터페이스는 해석 가능성을 위해 단일 예측자 모델을 우선시합니다.

3. 필터링 (정적 달마티안 휴리스틱):

   • 중복성을 관리하기 위해 TxGraffiti 는 정적 달마티안 휴리스틱을 사용합니다.
   • 터치 수 (Touch Number): 스냅샷에서 부등식이 등식으로 성립하는 (sharp instances) 대상의 개수로 정의됩니다.
   • 선택 논리: 후보들은 터치 수에 따라 정렬됩니다. 후보는 이전에 승인된 대표자들의 sharp 집합으로 아직 커버되지 않은 적어도 하나의 대상에 터치하면 "대표"로 승인됩니다. 만약 후보의 sharp 집합이 승인된 대표자의 것과 동일하다면, 동일한 등식 궤적의 다른 구문 형태인 "별칭 (alias)"으로 유지됩니다. 새로운 sharp 인스턴스를 추가하지 않는 후보는 폐기됩니다.

주요 기여

• 시스템 아키텍처: TxGraffiti 는 대화형 웹 애플리케이션과 오픈 소스 Python 패키지 (txgraffiti) 로 제공되는 모듈식 시스템으로 제시됩니다. 이는 불변량 계산과 추측 생성을 분리하여 고정된 데이터셋에 대한 빠른 반복을 가능하게 합니다.
• 최적화 기반 적합: 본 논문은 공식 생성 및 테스트를 기반으로 하는 문법 기반 열거에서, 특정 예측자에 대한 가장 엄격한 경계를 찾기 위해 LP 를 푸는 최적화 기반 적합으로 패러다임을 전환합니다. 이를 통해 생성된 후보들은 구성상 "테이블-참 (table-true)"이 되며 엄격함 측면에서 최적화됩니다.
• 정적 달마티안 필터링: 고정된 스냅샷에 대한 달마티안 휴리스틱의 적응은, 높은 "터치"(많은 sharp 증인) 를 가진 경계를 우선시하면서 중복성을 제거하는 단일 패시 결정론적 필터링 프로세스를 가능하게 합니다.
• 해석 가능성: 가설 클래스를 단순한 아핀 템플릿으로 제한하고 계수를 유리수화함으로써, 시스템은 간결하고 인간이 읽을 수 있는 추측을 생성합니다.

결과
본 논문은 여러 예시를 통해 시스템의 유효성을 입증합니다:

• 워크플로우 설명: 총 지배수 $\gamma_t$를 사용하여, 시스템은 $\Delta(G) \le 3$인 그래프에 대해 $\gamma_t(G) \ge \frac{2}{3}R(G)$라는 경계를 생성했습니다. 이는 $\Delta(G)$를 포함하는 정리로 빠르게 일반화되었으며 표준 추정을 사용하여 증명되었습니다.
• 촉진된 출판물: 본 논문은 TxGraffiti 추측으로 시작하여 이후 증명된 여러 그래프 이론 결과를 목록화합니다:
  • 독립수 vs 매칭수: $r$-정규 그래프에 대한 $\alpha(G) \le \mu(G)$라는 추측이 [51] 에서 증명되었습니다.
  • 제로 포싱 경계: 제로 포싱 수 ($Z, Z_t, Z_+$) 와 지배 및 독립 매개변수와 관련된 여러 부등식이 추측되고 증명되었습니다. 여기에는 claw-free 그래프에 대한 $Z(G) \le \beta(G)$와 입방 그래프에 대한 경계가 포함됩니다.
  • 미해결 문제: 시스템은 $\Delta \le 3$인 연결 그래프에 대한 $Z(G) \le \alpha(G) + 1$이라는 추측을 식별했는데, 이는 부분적 결과가 존재하지만 여전히 핵심적인 미해결 문제로 남아 있습니다.

의의 및 주장
본 논문은 TxGraffiti 를 자율적으로 심오한 정리를 발견하는 도구가 아니라, 인간의 수학적 탐구를 촉진하는 구조화된 증거 생성기로 위치시킵니다.

• 경험적 타당성: 시스템은 큐레이션된 스냅샷의 모든 인스턴스에 대해 성립하는 "테이블-참" 진술을 생성합니다. 저자들은 명시적으로 "정리"라는 용어를 공식적 증명으로 확립된 진술에 reserved 하며, 시스템의 출력은 추측으로 구분합니다.
• 철학적 입장: Graffiti 를 설계한 Fajtlowicz 의 경험적 관점을 반영하여, 본 논문은 기계가 그럴듯하고 심오한 추측을 생성할 수 있다는 능력이 경험적 사실이며, 기계가 열린 수학적 발견에서 의미 있는 참여자라는 관점을 지지한다고 주장합니다.
• 확장성과 재현성: 스냅샷 테이블을 버전 관리되고 감사 가능한 산물로 취급함으로써, TxGraffiti 는 데이터 손상 관련 견고성 문제를 해결하고 증거 기반이 성장함에 따라 추측을 재현하고 정제할 수 있도록 보장합니다.

저자들은 현재의 구현이 그래프 불변량에 초점을 맞추고 있지만, "스냅샷-테이블 패러다임"과 최적화 및 필터링 파이프라인은 계산 가능한 특징과 술어를 허용하는 대상이 있는 모든 도메인에 광범위하게 적용 가능하다고 결론지었습니다.