형식화된 표현을 기반으로 증명을 탐색 가능하게 만들기

Making Written Theorems Explorable by Grounding Them in Formal Representations

LLM이 생성한 설명은 기술적인 내용을 더 쉽게 이해하도록 만들 수 있지만, 상호 작용 측면에서 지원할 수 있는 한계가 있습니다. LLM의 출력은 정적인 텍스트이기 때문에 실행하거나 단계별로 분석할 수 없습니다. 본 연구에서는 설명에 형식화된 표현을 적용하면 정적인 텍스트만으로는 제공할 수 없는 상호 작용 기능을 구현할 수 있다고 주장합니다. 우리는 이 아이디어를 수학적 증명 이해를 위해 '탐색 가능한 정리(explorable theorems)'라는 시스템에 적용했습니다. 이 시스템은 LLM을 사용하여 정리와 그에 대한 서면 증명을 Lean이라는, 기계 검증 증명을 위한 프로그래밍 언어로 변환하고, 서면 증명과 Lean 코드를 연결합니다. 사용자는 증명을 단계별로 검토하고, 사용자 정의 예제 또는 반례를 테스트하고, 각 단계를 연결하는 논리적 의존성을 추적할 수 있습니다. 각 단계는 Lean 증명을 해당 예제에 대해 실행하고 중간 상태를 추출하여 생성됩니다. 사용자 연구($n=16$) 결과, 제안된 접근 방식의 잠재적인 장점이 확인되었습니다. 증명 검토 작업에서, 제공된 탐색 기능에 접근할 수 있었던 참가자들은 이해도 질문에 대해 더 정확하고 자세한 답변을 제공했으며, 이는 수학적 내용을 더 깊이 이해하고 있음을 보여줍니다.

LLM-generated explanations can make technical content more accessible, but there is a ceiling on what they can support interactively. Because LLM outputs are static text, they cannot be executed or stepped through. We argue that grounding explanations in a formalized representation enables interactive affordances beyond what static text supports. We instantiate this idea for mathematical proof comprehension with explorable theorems, a system that uses LLMs to translate a theorem and its written proof into Lean, a programming language for machine-checked proofs, and links the written proof with the Lean code. Readers can work through the proof at a step-level granularity, test custom examples or counterexamples, and trace the logical dependencies bridging each step. Each worked-out step is produced by executing the Lean proof on that example and extracting its intermediate state. A user study ($n = 16$) shows potential advantages of this approach: in a proof-reading task, participants who had access to the provided explorability features gave better, more correct, and more detailed answers to comprehension questions, demonstrating a stronger overall understanding of the underlying mathematics.