원본 영상을 바탕으로 AI의 도움을 받아 작성했습니다. 원본 영상이 기준입니다.
Log in to leave a comment
아직 작성된 글이 없습니다
Wenn man ein großskaliges System zum Lösen mathematischer Probleme auf dem Desktop im Forschungslabor einrichtet, hilft eine grobe Architekturübersicht absolut nicht weiter. Hier werden die Praxisphasen zusammengefasst, um eine Lean 4-Pipeline direkt in der lokalen Umgebung einzurichten und langlebige Multi-Agenten anzubinden, um mathematische Suchaufgaben vollständig zu automatisieren.
Wenn man Lean 4 in einer Entwicklungsumgebung manuell installiert und sich auf das VS Code Language Server Protocol verlässt, führt das bei großskaliger KI-Verifizierung zu schweren Engpässen. Wenn vorkompilierte Mathlib4-Binärdateien nicht gecacht werden, kompiliert die lokale CPU Hunderttausende von Sätzen direkt neu, wodurch allein der Aufbau der Umgebung über 180 Minuten dauert. Um Code-Verifizierungsanfragen von Dutzenden Malen oder mehr pro Sekunde zu verarbeiten, muss auf eine Kimina Lean Server-Pipeline auf Basis von FastAPI umgestellt werden.
Die konkreten Aufbauprozeduren, um die Einrichtungszeit für langlebige Verifizierungsaufgaben mathematischer Probleme von 180 Minuten auf unter 20 Minuten zu verkürzen, sind wie folgt:
`lean
import Lake
open Lake DSL
package «proof_automation» {
}
equire 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
`
Wenn dieser Vorgang abgeschlossen ist, wird der Vorkompilierungscache sofort empfangen und innerhalb von 20 Minuten ist eine vollständige lokale REPL-Ausführungsumgebung bereit, mit der bis zu 50 Beweisabschnitte pro Sekunde gleichzeitig verifiziert werden können.
Wenn man versucht, komplexe Satzbeweise mit einem einzigen Prompt-Aufruf eines großen Sprachmodells durchzuführen, gehen mit länger werdendem Kontext Unterziele verloren oder es wird eine Endlosschleife betreten. Es sollte eine hierarchische Directed Acyclic Graph-Architektur angewendet werden, bei der die Rollen in einen Root-Agenten, der für die Problemaufteilung zuständig ist, und Sub-Agenten, die isolierte Untertaktiken ausführen, aufgeteilt sind.
Durch die Annahme des JSON-Formats als Agenten-Kommunikationsspezifikation und die Übergabe von Prompts bei isoliertem Scope kann der Verbrauch von API-Tokens um mehr als 40 Prozent gesenkt werden. Das JSON-Schema, das beim Aufruf von Sub-Agenten verwendet wird, sieht wie folgt aus:
`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"]
}
`
Die schrittweise Steuerungsreihenfolge, um Endlosschleifen aufgrund von Halluzinationen des Agenten zu blockieren und eine stabile Hierarchiestruktur zu betreiben, ist wie folgt:
Wenn bei über stundenlang andauernden Beweissuchaufgaben bei jeder Anfrage der gesamte Gesprächsverlauf an die Backend-API übertragen wird, explodiert die Token-Nutzung. Es muss eine Caching-Schicht auf Basis von LeanExplore und einer Vector DB aufgebaut werden, und die Eingabe-Token-Overheads müssen kontrolliert werden, indem bereits verifizierte Zwischenergebnisse von Taktiken in Form von Hilfssätzen zusammenfassend im Speichergraph widergespiegelt werden.
Registrieren Sie auf dem Backend-Server den Umgebungsbezeichner der REPL-Session, um wiederkehrende import Mathlib-Anweisungen am Anfang des Prompts zu entfernen. Allein dadurch können die Eingabe-Token sofort um 50 bis 70 Prozent reduziert werden. Die Implementierungsprozedur der Steuerungspipeline zur Vermeidung einer Explosion der API-Kosten durch Budgetüberschreitung ist wie folgt:
`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)
`
Die Vorgehensweise, bei der ein KI-Agent Code generiert und Fehler dann manuell überprüft werden, stellt einen kritischen Engpass für die gesamte Forschung dar. JSON-Parsing-Daten wie Syntaxfehler, Typeninkonsistenzen und ungelöste Ziele, die der Lean REPL-Kom
}