Can LLM Aid in Solving Constraints with Inductive Definitions?

Created by

Haebom

저자

Weizhi Feng, Shidong Shen, Jiaxiang Liu, Taolue Chen, Fu Song, Zhilin Wu

💡 개요

귀납적(재귀적) 정의를 포함하는 제약 조건을 푸는 것은 어려운 문제입니다. 본 연구에서는 대규모 언어 모델(LLM)을 활용하여 이러한 귀납적 정의를 추론하는 데 필요한 보조 보조정리를 생성하도록 유도합니다. 또한, LLM이 반복적으로 추측을 생성하고 제약 조건 해결사가 그 유효성과 유용성을 검증하는 신경-기호적 접근 방식을 제안합니다.

🔑 시사점 및 한계

•

LLM을 활용하여 귀납적 정의를 포함하는 제약 조건 해결에 필요한 보조 보조정리를 생성할 수 있습니다.

•

LLM과 제약 조건 해결기를 결합한 신경-기호적 접근 방식이 기존의 SMT 및 CHC 해결기보다 성능을 향상시킵니다.

•

제안된 방법론은 대수적 데이터 타입 및 점화식에서 비롯된 다양한 벤치마크에서 기존 해결기보다 약 25% 더 많은 증명 과제를 해결하는 데 효과적임을 입증했습니다.

•

이 접근 방식은 특정 유형의 추론이나 복잡한 귀납적 정의에 대한 확장성 또는 일반화 가능성과 같은 한계가 있을 수 있습니다.

PDF 보기

Made with Slashpage