Learning Conjecturing from Scratch
Created by
- Haebom
Category
Empty
저자
Thibault Gauthier, Josef Urban
개요
본 논문은 OEIS에서 추출한 16197개의 문제 데이터셋을 기반으로 귀납적 예측을 추측하는 자기 학습 접근 방식을 제시합니다. 기존의 SMT 및 ATP 시스템으로는 귀납적 및 산술적 추론이 동시에 필요하여 해결하기 어려운 문제들입니다. 제안하는 접근 방식은 (i) 기존에 해결된 문제와 유용한 귀납적 예측 간의 대응 관계를 학습하는 신경망 번역기를 훈련하고, (ii) 훈련된 신경망 시스템을 사용하여 새로운 귀납적 예측을 생성하고, (iii) z3 증명기를 사용하여 생성된 예측을 통해 문제를 증명하고, (iv) 예측 크기 및 증명된 문제에 대한 해결 속도와 같은 휴리스틱을 사용하여 다음 반복 훈련을 위한 최적의 예측을 선택하는 피드백 루프로 구성됩니다. 결과적으로, CVC5, Vampire 또는 Z3가 60초 안에 2265개의 문제를 해결한 것과 비교하여 5565개의 문제를 해결했습니다.
시사점, 한계점
•
시사점:
◦
자기 학습 기반의 귀납적 예측 추측 방식을 통해 기존 시스템보다 많은 수의 어려운 수학 문제를 해결 가능함을 보여줌.
◦
신경망 번역기와 자동 증명 시스템의 결합을 통한 새로운 문제 해결 접근법 제시.
◦
복잡한 수학적 추론 문제 해결에 대한 새로운 가능성 제시.
•
한계점:
◦
현재 접근 방식은 OEIS 데이터셋에 국한되어 있으며, 다른 유형의 문제에 대한 일반화 가능성은 추가 연구가 필요함.
◦
사용된 휴리스틱의 성능에 대한 추가적인 분석과 개선이 필요할 수 있음.
◦
신경망 모델의 해석성 및 설명 가능성에 대한 추가 연구 필요.
