PhysProver: Advancing Automatic Theorem Proving for Physics

Resumen Técnico: PhysProver

Planteamiento del Problema

Si bien la integración de Modelos de Lenguaje de Gran Escala (LLMs) con lenguajes formales verificables ha avanzado significativamente en la demostración automática de teoremas en matemáticas (por ejemplo, Lean4), el dominio del razonamiento físico formal permanece en gran medida inexplorado. Los demostradores de teoremas de vanguardia (SOTA) actuales, entrenados principalmente en conjuntos de datos matemáticos, demuestran un bajo rendimiento en tareas relacionadas con la física. Esta brecha existe porque la física depende de fundamentos matemáticos rigurosos y derivaciones formales específicas de teorías físicas (por ejemplo, Teoría de Campos Cuánticos, Teoría de Cuerdas) que no están adecuadamente representadas en los conjuntos de datos actuales de demostración de teoremas matemáticos. Trabajos previos han identificado esta deficiencia, pero no han propuesto métodos efectivos para cerrarla.

Metodología

Los autores proponen PhysProver, el primer enfoque sistemático para mejorar la demostración de teoremas formal específicamente para el dominio de la física. La metodología consta de tres componentes principales:

1. Construcción de Datos (PhysLeanData)

Para abordar la escasez de datos de física formal de alta calidad, los autores construyeron PhysLeanData, un conjunto de datos especializado que comprende aproximadamente 5,541 muestras de entrenamiento. El flujo de generación de datos involucra:

• Recolección de Semillas: Extracción de lemas demostrables y sus correspondientes demostraciones del repositorio de código abierto PhysLean, cubriendo dominios como mecánica clásica, electromagnetismo, mecánica cuántica, relatividad y teoría de campos cuánticos.
• Aumentación Sintética: Utilización de Claude-4.5-Sonnet para generar nuevas conjeturas basadas en pares de cabeceras de lemas semilla.
• Pipeline de Verificación: Un proceso de filtrado de dos etapas:
  1. Verificación Sintáctica: Uso del verificador de Lean para asegurar que las conjeturas generadas estén bien formadas y que todas las definiciones referenciadas existan.
  2. Verificación de Demostrabilidad: Empleo de múltiples demostradores fuertes (DeepSeek-Prover-V2-7B, Kimina-Prover-Distill-8B, Goedel-Prover-V2-8B) para intentar realizar las demostraciones. Las conjeturas se retienen solo si al menos un demostrador verifica la sentencia con éxito.
• Resultado: El conjunto de datos final contiene ~5,000 muestras de entrenamiento y ~250 muestras de prueba, filtradas a una longitud máxima de 4,096 tokens.

2. Marco de Entrenamiento

Los autores aprovechan DeepSeek-Prover-V2-7B, un fuerte demostrador de teoremas matemático de código abierto, como el modelo base. En lugar de un Ajuste Fino Supervisado (SFT), que los autores encontraron que degrada el rendimiento en esta tarea, emplean Aprendizaje por Refuerzo con Recompensas Verificables (RLVR) utilizando el algoritmo Optimización de Política Relativa de Grupo (GRPO).

• Señal de Recompensa: El verificador de Lean proporciona una recompensa binaria (1 para una demostración correcta, 0 de lo contrario). Las demostraciones que contienen marcadores de posición como sorry o admit son penalizadas con una recompensa de 0 para evitar el "hackeo de recompensa" (reward hacking).
• Aprendizaje Curricular: Para facilitar el aprendizaje, los datos de entrenamiento se ordenan por la longitud de sus demostraciones de verdad fundamental (ground-truth), permitiendo una progresión de entrenamiento de "fácil a difícil".

3. Estrategia de Evaluación

El modelo se evalúa en:

• Dentro de la Distribución (In-Distribution): El conjunto de prueba de PhysLeanData, categorizado en Clásica, Partículas y Cuerdas, Relatividad y Teoría de Campos Cuánticos.
• Fuera de la Distribución (OOD): El benchmark MiniF2F-Test (matemáticas) para evaluar las capacidades de generalización más allá del dominio de la física.

Resultados Clave

• Rendimiento en Benchmarks de Física: PhysProver logra una mejora general del 2.4% sobre el modelo base DeepSeek-Prover-V2-7B en todos los subdominios de la física. Notablemente, mejora el rendimiento en la desafiante categoría de "Partículas y Cuerdas" en un 3.0%.
• Comparación con Modelos Propietarios: El PhysProver de 7 mil millones de parámetros supera tanto a GPT-5 como a Claude-4.5-Sonnet en precisión general en el conjunto de prueba de física, demostrando la eficacia de los modelos expertos pequeños y especializados en el dominio.
• Generalización a las Matemáticas: El entrenamiento en datos de física produce una mejora del 1.3% en el benchmark MiniF2F-Test (pass@16), lo que indica que el entrenamiento formal en física mejora las capacidades de razonamiento matemático formal general.
• Ablación sobre SFT: Los experimentos muestran que el Ajuste Fino Supervisado (SFT) estándar en el conjunto de datos de física provoca una caída del 6.4% en el rendimiento. En contraste, el Ajuste Fino de Muestreo de Rechazo (RAFT) y el enfoque de RLVR propuesto producen mejoras, lo que sugiere que alinear la distribución de salida del modelo con los datos de entrenamiento (vía RL o RAFT) es más efectivo que el SFT directo para este dominio.

Significado y Contribuciones

El artículo reclama tres contribuciones primarias:

1. Primer Demostrador de Dominio Específico: Introduce los primeros métodos diseñados específicamente para entrenar demostradores de teoremas formales para la física, abordando una brecha crítica en la literatura donde los modelos SOTA fallan en tareas de física.
2. Dataset y Pipeline: Desarrolla y libera PhysLeanData, un conjunto de datos compacto pero exhaustivo, junto con un pipeline de síntesis de conjeturas adaptado para teoremas físicos, destinado a beneficiar a la comunidad de investigación.
3. Rendimiento y Generalización: Demuestra que un modelo entrenado con un pequeño conjunto de datos (~5K) de física puede superar a los demostradores matemáticos SOTA en tareas de física y, simultáneamente, mejorar el rendimiento en benchmarks matemáticos generales.

Los autores concluyen que su trabajo proporciona un paradigma para extender los demostradores formales más allá de los dominios matemáticos. Enfatizan que, si bien los resultados actuales son prometedores, el enfoque resalta el potencial de utilizar RLVR y datos de alta calidad y específicos del dominio para superar las limitaciones de los modelos de propósito general en campos científicos especializados. El conjunto de datos y el modelo se liberan a la comunidad para fomentar la investigación adicional.