원본 영상을 바탕으로 AI의 도움을 받아 작성했습니다. 원본 영상이 기준입니다.
Log in to leave a comment
아직 작성된 글이 없습니다
Когда вы развертываете крупномасштабную систему решения математических задач на лабораторном настольном компьютере, общий обзор архитектуры ничем не поможет. В этой статье описаны практические шаги по прямой настройке конвейера 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
`
После выполнения этой задачи вы мгновенно получите кэш предварительной компиляции, и в течение 20 минут будет готова полностью готовая к работе локальная среда REPL, способная одновременно проверять до 50 блоков доказательств в секунду.
Попытка доказать сложную теорему с помощью одного вызова промпта большой языковой модели приводит к потере подцелей по мере удлинения контекста или попаданию в бесконечный цикл. Необходимо применить иерархическую архитектуру ориентированного ациклического графа, разделяющую роли на корневого агента, отвечающего за декомпозицию задач, и субагентов, выполняющих изолированные подугрозы.
Использование формата JSON в качестве спецификации связи между агентами и изоляция областей видимости при передаче промптов позволяют сократить потребление токенов 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"]
}
`
Последовательность пошагового контроля для предотвращения бесконечных циклов из-за галлюцинаций агента и запуска стабильной иерархической структуры следующая:
При поиске доказательств, длящемся часами, отправка всей истории диалога в бэкенд API при каждом запросе приводит к взрывному росту использования токенов. Необходимо создать кэширующий слой на базе 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, должны напрямую подключаться в качестве входных данных обратной связи для агента.
Принцип работы цикла управления автоисправлением, заменяющего ручную проверку и повышающего скорость исследований более чем в 2 раза, заключается в следующем:
`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 K"].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
`