연구진은 그래프 이론에서 추측 생성-반박-형식화-증명을 자동화하는 계산 파이프라인 'AutoGraphForge'를 개발 중이라고 보고했다. 추측 생성은 반례 유도 방식으로 진행되며, Graffiti3 생성기가 수백 개 그래프와 그 불변량으로 이뤄진 작은 스냅샷 테이블에서 추측을 제안하고, 이 테이블은 자신의 추측에 대한 반례로만 커진다. 559개의 고전·통설 관계로 구성된 참신성 필터가 선형계획법으로 후보가 이미 알려진 결과에 포함되는지 판별하며, 살아남은 후보는 약 34만8000개 그래프 데이터셋으로 검증된다. HPC 클러스터에서 여러 라운드를 실행한 결과 반박 데이터셋, 참신성 필터, 능동 탐색을 모두 통과한 추측 6522개를 얻었고, 이 중 이분·정규 그래프의 소멸수와 간선피복수 사이의 비자명한 관계 등은 직접 증명했다. 이후 단계에서는 각 추측을 Lean 4 명제로 자동 변환하고 두 신경망 증명기를 커널 검증과 결합해 검증한다.

• •그래프 이론 추측의 생성-반박-형식화-증명을 자동화하는 파이프라인 AutoGraphForge 개발
• •Graffiti3 생성기가 반례로만 성장하는 스낵샷 테이블에서 추측 제안
• •559개 관계로 구성된 참신성 필터와 약 34만8000개 그래프 데이터셋으로 후보 검증
• •여러 라운드 실행 끝에 6522개 추측이 모든 검증을 통과, 일부는 직접 증명
• •최종 단계에서 Lean 4 명제로 자동 변환 후 신경망 증명기와 커널 검증으로 확인