arxiv arXiv cs.AI · hace 55 d · research

Lean como Oráculo de Recompensa Verificado por Proceso en RL para Demostración de Teoremas

Traducido del English → Español

Este trabajo muestra que Lean puede servir como un oráculo simbólico de proceso, proporcionando retroalimentación fina y verificada durante el aprendizaje por refuerzo. Al analizar los intentos de demostración en secuencias de tácticas y usar la elaboración de Lean para marcar pasos válidos y primeros fallos, el sistema genera señales de recompensa densas basadas en teoría de tipos. Los experimentos demuestran que la supervisión a nivel de táctica supera a los métodos solo de resultado en benchmarks como MiniF2F y ProofNet, destacando el papel de Lean tanto como evaluador como fuente de recompensa de entrenamiento.

Importancia 3/3 Nueva función frente a los líderes Nuevo entorno de evaluación con diferenciadores arXiv cs.AI DeepSeek Google DeepMind OpenAI Evaluation & benchmarks Reasoning models Training methods

Leer original

VIMPO: Optimización de política sin crítico para LLMs

VIMPO introduce un método de optimización de política sin crítico que deriva una función de valor implícita por la política a partir del aprendizaje por refuerzo con regularización KL. Permite la incorporación de recompensas verificables sin entrenar un crítico y supera a GRPO en benchmarks matemáticos, especialmente bajo recompensas ruidosas.

arxiv arXiv cs.CL · hace 55 d · 4 vistas

Aprendizaje de currículo bayesiano en variedades latentes de LLM

Manifold Bandits introduce el Currículo de Variedad Bayesiana (BMC), un marco que modela el muestreo de problemas como un problema estructurado de bandits en el espacio latente de los LLM. BMC organiza las tareas en un árbol jerárquico y utiliza aprendizaje bayesiano para guiar el muestreo, revelando compensaciones entre la señal de aprendizaje, la diversidad de tareas y la relevancia de la evaluación. Priorizar únicamente la dificultad no logra un buen rendimiento en tareas posteriores, subrayando la necesidad de estructura y muestreo consciente del tipo.

arxiv arXiv cs.LG · hace 56 d · 2 vistas

El RL guiado por discriminador corrige el emparejamiento de flujos con recompensas alineadas a los datos

El RL guiado por discriminador (DRL) utiliza un espacio de representaciones preentrenado para entrenar un discriminador que separa los datos reales de las muestras generadas por el modelo. Su logit se usa como recompensa en el RL con regularización KL, alineando las salidas del modelo con la realismo visual y semántico sin preferencias humanas. DRL mejora FID y FD semántico en modelos como SiT y JiT, y mejora la frontera de Pareto entre preferencia y fidelidad.

arxiv arXiv cs.LG · hace 56 d

TAPO: Auto-distilación con trayectorias micro-reflectivas

TAPO avanza la auto-distilación mediante la construcción de trayectorias micro-reflectivas explícitas que retienen el razonamiento erróneo e insertan diagnósticos en lenguaje natural. Estas trayectorias, derivadas de rollouts del modelo correctos e incorrectos, proporcionan correcciones de error finas ancladas en el propio razonamiento del modelo, mejorando tanto el razonamiento del primer intento como la corrección de errores en comparación con GRPO.

arxiv arXiv cs.AI · hace 56 d · 1 vista

Asignación de crédito autocondicionada para RL con recompensas verificables

SC-GRPO utiliza la divergencia KL por token desde trayectorias autocondicionadas para ponderar gradientes en el aprendizaje por refuerzo. Supera a GRPO en un 8.1% y a DAPO en un 5.9% en tareas de matemáticas, código y agentes, con un rendimiento superior fuera de la distribución y mejores resultados que OPD.