컨텐츠 시작
학술대회/행사
초록검색
| 제출번호(No.) | 0115 |
|---|---|
| 분류(Section) | Contributed Talk |
| 분과(Session) | (AM) Applied Mathematics(including AI, Data Science) (AM) |
| 발표시간(Time) | 20th-C-10:50 -- 11:10 |
| 영문제목 (Title(Eng.)) |
Formal proof generation models: Initial stages of applying large language models and search techniques |
| 저자(Author(s)) |
Sangjun Han1, Taeil Hur2, Youngmi Hur3, Kathy Sangkyung Lee1, Myungyoon Lee1, Hyojae Lim1 Yonsei University1, JENTI Inc.2, Yonsei University / KIAS3 |
| 초록본문(Abstract) | In recent years, research for Large Language Models (LLMs) and their utilization has drawn considerable interest, showing remarkable results in various tasks. The automatic generation of mathematical proofs using formal language has emerged naturally and gained increasing attention as the foundation for artificial intelligence capable of logical reasoning. In our research on the formal proof generation, our aim is to develop a simple model using ChatGPT, the formal language Lean, and two proof search algorithms. Through various experiments, we explore how connecting ChatGPT with proof search methods can enhance the proof generation performance. As a result, our highest-performing model, despite its simplicity, outperforms state-of-the-art models on the miniF2F benchmark dataset. We subsequently conduct experiments using the combination of natural language and Python instead of Lean, revealing limitations of existing models and suggesting new directions for further improvements. |
| 분류기호 (MSC number(s)) |
68T01, 68T50, 68V15 |
| 키워드(Keyword(s)) | Large language model, theorem proving |
| 강연 형태 (Language of Session (Talk)) |
Korean |