Reasoning without Gold Standards: A Proxy-Judge Theory of Autoformalization

• URL: http://arxiv.org/abs/2606.09449v1
• Date: Mon, 08 Jun 2026 12:57:09 GMT
• Title: Reasoning without Gold Standards: A Proxy-Judge Theory of Autoformalization
• Abstract summary: Autoformalization (AF) asks a model to translate informal mathematical or logical reasoning into a formally checkable object.<n>We introduce a reference-free proxy-judge framework for AF that replaces gold-standard matching with a vector of per-axis property checks.<n>Across seven formalization backbones on miniF2F, ProofNet, e-SNLI, and ProntoQA, refinement consistently lifts Pass Rate over the single-shot ICL baseline.
• Score: 25.540859911959885
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Complex reasoning tasks increasingly require systems to produce outputs whose correctness cannot be judged by exact match against a single reference. Autoformalization (AF) is a representative example; it asks a model to translate informal mathematical or logical reasoning into a formally checkable object, yet expert-validated formalizations do not scale beyond toy cases and a single informal argument can admit many valid formal renderings. Progress therefore depends on whether partial, structured proxies can substitute for exact references. We introduce a reference-free proxy-judge framework for AF that replaces gold-standard matching with a vector of per-axis property checks. The framework organizes the proxy along three structural scopes that cover global properties of the elicited object, per-module properties internal to its sub-components, and cross-domain properties that re-align it to the informal source, and aggregates each axis into a verdict vector. The vector drives a reflective refinement loop in which a violated coordinate routes the controller to a matching repair target, so each iteration changes only what is judged wrong. Under bounded judge noise, the expected intrinsic gap contracts geometrically to a noise-dependent plateau. Across seven formalization backbones on miniF2F, ProofNet, e-SNLI, and ProntoQA, refinement consistently lifts Pass Rate over the single-shot ICL baseline, and the per-axis proxy outperforms a matched scalar proxy on benchmarks where the baseline has room to improve. Structured proxy judgments therefore provide both a practical refinement signal and a theoretical handle on convergence when exact references are unavailable.

Related papers

• Structuring Semantic Embeddings for Principle Evaluation: A Prototype-Guided Contrastive Learning Approach [58.15427952222424]
  General-purpose text embeddings are widely deployed for such tasks, but broad semantic similarity can place semantically similar yet task-distinct examples.<n>We introduce Prototype-Guided Contrastive Learning (PGCL), a prototype-guided geometric regularization module built on top of frozen text embeddings.
  arXiv  Detail & Related papers  (2026-08-15T13:19:25Z)
• More Data, Worse Decisions? Preference Reversals in Neural Networks under Gram Incompatibility [9.196757973061198]
  Case-Based Decision Theory (CBDT) formalizes the requirement through its composition axiom.<n>We study when this property holds for fixed-representation neural networks with ordinary least squares (OLS) output heads.<n>We develop a three-stage audit that traces strict pairwise reversals through decision changes to task-defined utility loss.
  arXiv  Detail & Related papers  (2026-07-28T18:52:47Z)
• NormWorlds-CF: Solver-Verified Counterfactual Normative Reasoning with Metamorphic-Relation GRPO [1.5483078145498086]
  NormWorlds-CF is a solver-verified environment for counterfactual normative reasoning in rule worlds.<n>Its deterministic solver produces final answers, proof and falsification certificates, argument statuses, support sets, and paired-world change labels.
  arXiv  Detail & Related papers  (2026-07-04T17:11:21Z)
• Citation-Closure Retrieval and Per-Rule Attribution for Real-World Regulatory Compliance Question Answering [54.97384993676565]
  We formalize Regulatory Compliance QA with RegOps-Bench, a novel benchmark featuring an Operational Knowledge Graph derived from complex national R&D regulations.<n>RefWalk traverses cross-document citations, fuses multi-view candidates via max-based aggregation, and enforces per-rule attribution to explicitly map claims to sources.
  arXiv  Detail & Related papers  (2026-05-28T10:38:38Z)
• A Controlled Counterexample to Strong Proxy-Based Explanations of OOD Performance: in a Fixed Pretraining-and-Probing Setup [0.9805949492148788]
  Task-agnostic structure proxies are often used to interpret why one pretraining corpus transfers better than another.<n>We test this requirement in a fixed pretraining-and-probing setup motivated by computationally bounded notions of learned structure.<n>A proxy for total learned structure can fail to track the task-relevant structure that drives OOD performance, even in a controlled setting.
  arXiv  Detail & Related papers  (2026-05-12T05:36:46Z)
• CellScientist: Dual-Space Hierarchical Orchestration for Closed-Loop Refinement of Virtual Cell Models [62.281480231694]
  Virtual Cell Modeling (VCM) requires models that not only predict perturbation responses, but also support targeted revision when predictions fail.<n>Current LLM-assisted modeling face a refinement-routing problem: prediction discrepancies are observed through executable implementations.<n>We propose CellScientist, a dual-space hierarchical framework that couples a high-level hypothesis space with a low-level executable implementation space.
  arXiv  Detail & Related papers  (2026-05-08T06:40:24Z)
• IMPACT-CYCLE: A Contract-Based Multi-Agent System for Claim-Level Supervisory Correction of Long-Video Semantic Memory [73.22944697933603]
  Existing pipelines produce opaque, end-to-end outputs that expose no intermediate state for inspection.<n>We present IMPACT-Cycle, a supervisory multi-agent system that reformulates long-video understanding as a multimodal iterative claim-level maintenance.
  arXiv  Detail & Related papers  (2026-04-22T03:03:33Z)
• From Perception to Autonomous Computational Modeling: A Multi-Agent Approach [0.0]
  We present a solver-agnostic framework in which coordinated large language model (LLM) agents autonomously execute the complete computational mechanics workflow.<n>Agents are formalised as conditioned operators on a shared context space with quality gates that introduce conditional iteration between pipeline layers.
  arXiv  Detail & Related papers  (2026-04-08T07:56:34Z)
• Reasoning Provenance for Autonomous AI Agents: Structured Behavioral Analytics Beyond State Checkpoints and Execution Traces [0.0]
  Agent Execution Record (AER) is a structured reasoning primitive that captures intent, observation, and inference as first-class queryable fields on every step.<n>We show how AERs enable population-level behavioral analytics: reasoning pattern mining, confidence calibration, cross-agent comparison, counterfactual regression testing via mock replay.
  arXiv  Detail & Related papers  (2026-03-23T08:27:54Z)
• VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning [4.3414302048068745]
  We present a neurosymbolic framework that combines Large Language Models with SMT solvers to produce verification-guided answers.<n>We introduce three key innovations: (1) multi-model consensus via formal semantic equivalence checking, (2) semantic routing that directs different claim types to appropriate verification strategies, and (3) precise logical error localization via Minimal Correction Subsets.<n>With the GPT-OSS-120B model, VERGE demonstrates an average performance uplift of 18.7% at convergence across a set of reasoning benchmarks compared to single-pass approaches.
  arXiv  Detail & Related papers  (2026-01-27T20:59:11Z)
• Refinement Provenance Inference: Detecting LLM-Refined Training Prompts from Model Behavior [58.751981587234916]
  This paper formalizes the Refinement Provenance Inference (RPI) audit task as Refinement Provenance Inference (RPI)<n>We propose RePro, a logit-based framework that fuses teacher-forced likelihood features with logit-ranking signals.<n>During training, RePro learns a transferable representation via shadow fine-tuning, and uses a lightweight linear head to infer provenance on unseen victims without training-data access.
  arXiv  Detail & Related papers  (2026-01-05T10:16:41Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  We develop CompassVerifier, an accurate and robust lightweight verifier model for evaluation and outcome reward.<n>It demonstrates multi-domain competency spanning math, knowledge, and diverse reasoning tasks, with the capability to process various answer types.<n>We introduce VerifierBench benchmark comprising model outputs collected from multiple data sources, augmented through manual analysis of metaerror patterns to enhance CompassVerifier.
  arXiv  Detail & Related papers  (2025-08-05T17:55:24Z)
• Retrieval is Not Enough: Enhancing RAG Reasoning through Test-Time Critique and Optimization [58.390885294401066]
  Retrieval-augmented generation (RAG) has become a widely adopted paradigm for enabling knowledge-grounded large language models (LLMs)<n>RAG pipelines often fail to ensure that model reasoning remains consistent with the evidence retrieved, leading to factual inconsistencies or unsupported conclusions.<n>We propose AlignRAG, a novel iterative framework grounded in Critique-Driven Alignment (CDA)<n>We introduce AlignRAG-auto, an autonomous variant that dynamically terminates refinement, removing the need to pre-specify the number of critique iterations.
  arXiv  Detail & Related papers  (2025-04-21T04:56:47Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.