Written with AI assistance from the source video. The video is the authority.
Log in to leave a comment
No posts yet
عند إعداد نظام واسع النطاق لحل المسائل الرياضية على جهاز سطح المكتب الخاص بمختبرك، فإن النظرة العامة للبنية الكبيرة لن تكون مفيدة بشكله الأمثل. سنلخص هنا الخطوات العملية للإعداد المباشر لخط أنابيب Lean 4 في البيئة المحلية وربط الوكلاء المتعددين طويلي الأمد لأتمتة مهام الاستكشاف الرياضي بالكامل.
إن تثبيت Lean 4 يدوياً في بيئة التطوير والاعتماد على بروتوكول خادم لغة VS Code يسبب اختناقات خطيرة أثناء التحقق بواسطة الذكاء الاصطناعي واسع النطاق. إذا لم يتم تخزين الملفات الثنائية المعالجة مسبقاً لـ Mathlib4 مؤقتاً، فإن وحدة المعالجة المركزية المحلية ستقوم بإعادة تجميع مئات الآلاف من النظريات يدوياً، مما يستغرق أكثر من 180 دقيقة لمجرد إنشاء البيئة. لمعالجة عشرات أو أكثر من طلبات التحقق من الكود في الثانية، يجب الانتقال إلى خط أنابيب Kimina Lean Server القائم على FastAPI.
فيما يلي خطوات الإعداد المحددة لتقليل وقت إعداد مهمة التحقق من المسائل الرياضية طويلة الأمد من 180 دقيقة إلى أقل من 20 دقيقة:
`lean
import Lake
open Lake DSL
package «proof_automation» {
}
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git" @ "v4.15.0"
require repl from git
"https://github.com/leanprover-community/repl.git" @ "main"
@[default_target]
lean_lib «ProofAutomation» {
}
`
`bash
lake update
lake exe cache get
lake build
`
عند الانتهاء من هذه العملية، ستتلقى ذاكرة التخزين المؤقت المعالجة مسبقاً على الفور لتصبح بيئة تنفيذ REPL المحلية الكاملة جاهزة في غضون 20 دقيقة، مع القدرة على التحقق من ما يصل إلى 50 مقطع برهان في وقت واحد في الثانية.
تؤدي محاولة إثبات نظريات معقدة من خلال استدعاء نموذج لغة كبير واحد إلى فقدان الأهداف الفرعية أو الدخول في حلقات لا نهائية كلما طال السياق. يجب تطبيق بنية رسم بياني موجه بلا دورات (DAG) تفصل الأدوار إلى وكيل رئيسي مسؤول عن تقسيم المشكلات ووكلاء فرعيين ينفذون تكتيكات فرعية معزولة.
من خلال اعتماد تنسيق JSON كمعيار لاتصالات الوكلاء وعزل النطاق لتمرير مطالبات (Prompts)، يمكنك تقليل استهلاك رموز API بنسبة تزيد عن 40 بالمائة. مخطط JSON المستخدم عند استدعاء الوكيل الفرعي هو كالتالي:
`json
{
"$schema": "https://json-schema.org/draft/2020-12/schema",
"title": "SubAgentProofTask",
"type": "object",
"properties": {
"task_id": { "type": "string" },
"target_hypothesis": { "type": "string" },
"current_goal_state": { "type": "string" },
"previous_failure_logs": {
"type": "array",
"items": {
"type": "object",
"properties": {
"attempted_tactic": { "type": "string" },
"error_message": { "type": "string" }
}
}
},
"sub_goal_target": { "type": "string" }
},
"required": ["task_id", "target_hypothesis", "current_goal_state", "sub_goal_target"]
}
`
ترتيب التحكم خطوة بخطوة لمنع الحلقات اللانهائية الناتجة عن هلوسة الوكيل وتشغيل بنية هرمية مستقرة هو كما يلي:
في مهام البحث عن البراهين التي تستغرق عدة ساعات، يؤدي إرسال سجل المحادثة بالكامل إلى واجهة برمجة التطبيقات للخلفية مع كل طلب إلى زيادة هائلة في استخدام الرموز (Tokens). يجب بناء طبقة التخزين المؤقت المستندة إلى LeanExplore وVector DB، والتحكم في النفقات العامة لرموز الإدخال عن طريق تلخيص نتائج التكتيكات الوسيطة التي تم التحقق منها مسبقاً وعكسها في الرسم البياني للذاكرة في شكل نظريات مساعدة.
قم بتسجيل معرف البيئة لجلسة REPL في خادم الخلفية لإزالة عبارات import Mathlib المتكررة في أعلى المطالبات. وحدها هذه الخطوة يمكنها تقليل رموز الإدخال بنسبة 50 إلى 70 بالمائة على الفور. إجراءات تنفيذ خط أنابيب التحكم لمنع انفجار تكاليف API بسبب تجاوز الحد الأقصى للميزانية هي كالتالي:
`python
import sys
import json
import logging
class CostMonitor:
def init(self, max_budget_usd: float, token_cost_per_1k: float):
self.max_budget = max_budget_usd
self.cost_per_1k = token_cost_per_1k
self.total_tokens_used = 0
self.current_cost = 0.0
def track_usage(self, prompt_tokens: int, completion_tokens: int):
tokens_in_call = prompt_tokens + completion_tokens
self.total_tokens_used += tokens_in_call
self.current_cost += (tokens_in_call / 1000.0) * self.cost_per_1k
logging.info(f"[TELEMETRY] Used Tokens: {tokens_in_call} | Total Cost: ${self.current_cost:.4f}")
if self.current_cost >= self.max_budget:
self.trigger_safe_pause()
def trigger_safe_pause(self):
logging.warning("[WARNING] Target budget threshold reached. Pausing workflow...")
with open(".leanflow/workflow-state/checkpoint.json", "w") as f:
json.dump({"status": "PAUSED_BUDGET_EXCEEDED", "tokens": self.total_tokens_used}, f)
sys.exit(0)
`
إن الطريقة التي يقوم فيها وكيل الذكاء الاصطناعي بتوليد الكود ثم مراجعة الأخطاء يدوياً تشكل عنق زجاجة قاتلاً للبحث بأكمله. يجب ربط بيانات تحليل JSON التي يصدرها مترجم Lean REPL (مثل أخطاء بناء الجملة، وعدم تطابق الأنواع، والأهداف التي لم تُحل) مباشرة كمدخلات تغذية مرجعية للوكيل.
طريقة عمل حلقة تحكم التصحيح التلقائي التي تحل محل المراجعة اليدوية وتضاعف سرعة البحث بأكثر من الضعف هي كالتالي:
`python
def parse_lean_repl_output(repl_response_json: str):
data = json.loads(repl_response_json)
parsed_diagnostics = {
"has_error": False,
"errors": [],
"open_sorries": []
}
if "messages" in data:
for msg in data["messages"]:
if msg.get("severity") == "error":
parsed_diagnostics["has_error"] = True
parsed_diagnostics["errors"].append({
"line": msg["pos"]["line"],
"column": msg["pos"]["column"],
"data": msg["data"]
})
if "sorries" in data:
for sorry in data["sorries"]:
parsed_diagnostics["open_sorries"].append({
"goal": sorry["goal"],
"proof_state": sorry["proofState"],
"line": sorry["pos"]["line"]
})
return parsed_diagnostics
`
يتم تمرير الكود النظيف الذي تم التحقق منه بالكامل عبر أدوات التحويل doc-gen4 و paperproof ليتم إنشاؤه تلقائياً في صورة تصور للرسم البياني المنطقي وسياق LaTeX يمكن إدراجهما فوراً في ورقة البحث.
`bash
lake build LeanAutomation:docs
lean-graph extract --input Main.lean --output proof_dependency.json
`