From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates
تقدم هذه الورقة البحثية NSPI، وهو إطار عمل عصبي-رمزي يستفيد من النماذج اللغوية الكبيرة لاقتراح حدسيات تقريبية لمجموع المربعات (Sum-of-Squares) والحوسبة الرمزية لتنقيحها إلى براهين دقيقة ومحققة آلياً باستخدام لغة Lean، مما يحقق إثباتاً آلياً قابلاً للتوسع لعدم تساوٍ متعدد الحدود يصل إلى 10 متغيرات.