כתבה
arXiv cs.AI ·
Magenta: סגירת המעגל בין התפיסה המתמטית לבין האימות המוצק
Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification
במאמר זה, נציגים פילוסופיה חדשה לתפיסה המתמטית, המשלבת חיפוש טבעי ואימות מוצק. המאמר כולל שימוש במודלי GPT-5 ו-Gemini.
תקציר מקורי באנגליתarXiv:2609.11319v1 Announce Type: new Abstract: Most of mathematical knowledge has been communicated through so-called informal use of mathematics and natural language. With large language models (LLMs) being highly adept in using natural language, they achieve strong performance, yet not perfect, in informal mathematical reasoning. Restraining LLMs to informal reasoning misses out on the opportunity to use the discrete verification abilities that machines offer through machine-checkable proofs. In this paper, we bridge the gap between informal and formal reasoning by integrating Lean signals into the informal reasoning process. We introduce Magenta, a training-free agentic pipeline that, given only a natural-language problem, produces an answer, expresses it as a Lean 4 statement, and con
קרא במקור המקורי
arxiv.org
פתח כתבה מקורית