(Auto)formalization is supposed to be easy: Trellis process semantics for spelling out rigorous proofs

Paper 1 addresses a critical and timely gap in evaluating deep research agents—multi-turn improvement under feedback—revealing fundamental limitations (regression during revision) that have broad implications for AI agent design. Its systematic methodology, quantitative findings, and publicly available code make it highly actionable for the rapidly growing field of AI agents. Paper 2, while innovative in combining LLMs with formal verification via a novel workflow, targets a narrower audience (autoformalization/theorem proving) and its impact depends on scalability beyond the demonstrated case study. Paper 1's findings are more broadly applicable across AI research.

Paper 2 likely has higher impact: it proposes a broadly applicable, timely methodology for reliable LLM-driven autoformalization with deterministic process semantics, demonstrated by an end-to-end Lean formalization of a recent major Ramsey theory result—strong evidence of rigor and real-world utility. Its approach can influence multiple fields (formal methods, theorem proving, ML/LLMs, mathematics) and addresses a central bottleneck in scalable verification. Paper 1 is innovative for long-horizon latent planning, but is more specialized, has preliminary results on a limited benchmark, and impact depends on further validation.

Paper 1 is more novel: it proposes a deterministically constrained, process-semantics workflow for LLM-based autoformalization grounded in a principled notion of proof rigor, and demonstrates an end-to-end Lean formalization of a recent research-level result—high potential to shift how formalization is done and to impact mathematics, PL, and AI verification. Paper 2 is timely and useful for evaluation practice, but its core contribution is an empirical validation of pairwise/Elo rankings and an identified bias factor; impact is likely narrower and more incremental.

Paper 2 tackles the highly impactful challenge of autoformalization in mathematics, demonstrating significant real-world utility by formalizing a recent Ramsey theory breakthrough. Its process-driven approach offers a reliable method for rigorous proof generation without requiring specialized training, potentially accelerating AI-assisted mathematics and formal verification. While Paper 1 introduces a valuable benchmark for physical assembly, its current success rates remain relatively low, making its immediate impact more exploratory compared to Paper 2's concrete achievement.

Paper 2 is likely higher impact: it tackles a timely, broadly relevant problem (off-policy evaluation under strategic covariate manipulation) with clear applications in high-stakes decision systems (lending, hiring, healthcare) and connections to causal inference, econometrics, and mechanism design. It proposes a concrete methodological contribution (local disclosure + doubly robust estimator) with stated consistency under explicit assumptions and empirical validation, suggesting rigor and adoptability. Paper 1 is novel and exciting for formal methods, but its impact may be narrower and more dependent on engineering maturity and generalization beyond showcased examples.

Paper 1 addresses the fundamental and widely-studied problem of LLM self-correction with a concrete, well-motivated framework (Thought-ICS) that demonstrates measurable improvements (20-40% self-correction lift). It has broad applicability across all LLM reasoning tasks, strong methodological rigor with quantitative results, and connects to neuroscience insights about error monitoring. Paper 2 presents a niche autoformalization system with an interesting workflow but targets a narrower community (formal verification/theorem proving). Paper 1's broader relevance to the rapidly growing LLM reasoning and self-improvement research area gives it higher potential impact.

Paper 1 demonstrates a breakthrough in autoformalization, a highly sought-after goal in AI for mathematics. By successfully formalizing a recent Ramsey theory breakthrough using generalist agents in a constrained workflow, it offers a highly novel approach that could revolutionize how mathematical proofs are verified. While Paper 2 presents a valuable contribution to AI safety and agent guardrails, Paper 1's impact on advancing AI-driven mathematical reasoning represents a more fundamental and transformative scientific milestone.

Paper 1 introduces a foundational theoretical framework for causal learning in AI agents, addressing the critical issue of persistent errors. Its rigorous mathematical bounds and general applicability across reinforcement learning and LLM systems offer broader, longer-term foundational impact compared to Paper 2's practical, though valuable, workflow for autoformalization.

Paper 1 presents a novel autoformalization system (Trellis) that bridges natural language mathematics and formal proofs in Lean, demonstrated on a recent Ramsey theory breakthrough. It combines LLM agents with deterministic process semantics in a practical, end-to-end system with concrete results. This addresses a fundamental bottleneck in mathematical formalization with broad implications for AI-assisted mathematics. Paper 2, while intellectually rigorous, is primarily a theoretical/diagnostic framework for legal RAG limitations without implementation or empirical validation, limiting its immediate scientific impact.

TRL-Bench addresses a significant gap in tabular representation learning by providing a standardized cross-paradigm evaluation framework with extensive benchmarks (20 models, 16 tasks, multiple granularities). Its breadth of impact is high given the ubiquity of tabular data in ML/AI. It provides reusable infrastructure, curated datasets, and actionable findings about encoder selection. Paper 2, while creative in combining LLMs with formal verification, presents a more niche contribution to autoformalization with limited demonstrated generality beyond a single case study. TRL-Bench's systematic methodology and broad applicability give it higher potential impact.