When Verification Hurts: Asymmetric Effects of Multi-Agent Feedback in Logic Proof Tutoring

• URL: http://arxiv.org/abs/2603.27076v1
• Date: Sat, 28 Mar 2026 01:35:59 GMT
• Title: When Verification Hurts: Asymmetric Effects of Multi-Agent Feedback in Logic Proof Tutoring
• Abstract summary: Large language models (LLMs) are increasingly used for automated tutoring, but their reliability in structured symbolic domains remains unclear.<n>We study step-level feedback for propositional logic derivation proofs, which require precise symbolic reasoning aligned with a learner's current proof state.<n>We introduce a knowledge-graph-grounded benchmark of 516 unique proof states with step-level annotations and difficulty metrics.
• Score: 3.1967732711000525
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Large language models (LLMs) are increasingly used for automated tutoring, but their reliability in structured symbolic domains remains unclear. We study step-level feedback for propositional logic proofs, which require precise symbolic reasoning aligned with a learner's current proof state. We introduce a knowledge-graph-grounded benchmark of 516 unique proof states with step-level annotations and difficulty metrics. Unlike prior tutoring evaluations that rely on model self-assessment or binary correctness, our framework enables fine-grained analysis of feedback quality against verified solution paths. We evaluate three role-specialized pipelines with varying solution access: Tutor (partial solution access), Teacher (full derivation access), and Judge (verification of Tutor feedback). Our results reveal a striking asymmetry: verification improves outcomes when upstream feedback is error-prone (<70% accuracy), but degrades performance by 4-6 percentage points through over-specification when feedback is already reliable (>85%). Critically, we identify a shared complexity ceiling; no model or pipeline reliably succeeds on proof states exceeding complexity 4-5. These findings challenge the assumption that adding verifiers or richer context universally improves tutoring, motivating adaptive, difficulty-aware architectures that route problems by estimated complexity and upstream reliability.

Related papers

• Omanic: Towards Step-wise Evaluation of Multi-hop Reasoning in Large Language Models [60.418191092851636]
  Omanic is an open-domain multi-hop QA resource that provides decomposed sub-questions and intermediate answers as structural annotations for analyzing reasoning processes.<n>It contains 10,296 machine-generated training examples (Omanic Synth) and 967 expert-reviewed human-annotated evaluation examples (OmanicBench)
  arXiv  Detail & Related papers  (2026-03-17T15:23:37Z)
• GATES: Self-Distillation under Privileged Context with Consensus Gating [89.62339954332248]
  We study self-distillation in settings where supervision is unreliable.<n>We focus on document-grounded question answering with asymmetric context.<n>We derive supervision online from tutor consensus by sampling multiple document-grounded reasoning traces.
  arXiv  Detail & Related papers  (2026-02-24T05:56:20Z)
• Learning to Repair Lean Proofs from Compiler Feedback [4.55626337217127]
  We study Lean proof repair as a supervised learning problem.<n>We introduce APRIL (Automated Proof Repair in Lean), a dataset of 260,000 supervised theorems.<n>We view diagnostic-conditioned supervision as a complementary training signal for feedback-using provers.
  arXiv  Detail & Related papers  (2026-02-03T01:53:56Z)
• Benchmarking Uncertainty Calibration in Large Language Model Long-Form Question Answering [7.1559850008795385]
  Large Language Models (LLMs) are commonly used in Question Answering (QA) settings.<n>Existing UQ approaches remain weakly validated in scientific QA.<n>We introduce the first large-scale benchmark for evaluating UQ metrics in reasoning-demanding QA.
  arXiv  Detail & Related papers  (2026-01-30T20:02:34Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• Eigen-1: Adaptive Multi-Agent Refinement with Monitor-Based RAG for Scientific Reasoning [53.45095336430027]
  We develop a unified framework that combines implicit retrieval and structured collaboration.<n>On Humanity's Last Exam (HLE) Bio/Chem Gold, our framework achieves 48.3% accuracy.<n>Results on SuperGPQA and TRQA confirm robustness across domains.
  arXiv  Detail & Related papers  (2025-09-25T14:05:55Z)
• RationAnomaly: Log Anomaly Detection with Rationality via Chain-of-Thought and Reinforcement Learning [27.235259453535537]
  RationAnomaly is a novel framework that enhances log anomaly detection by synergizing Chain-of-Thought fine-tuning with reinforcement learning.<n>We have released the corresponding resources, including code and datasets.
  arXiv  Detail & Related papers  (2025-09-18T07:35:58Z)
• 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)
• VerifyBench: A Systematic Benchmark for Evaluating Reasoning Verifiers Across Domains [19.579511315215424]
  Large language models rely on reinforcement learning to enhance their reasoning capabilities through feedback.<n>Existing research focuses on building better verifiers, yet a systematic evaluation of different types of verifiers' performance remains lacking.<n>We construct 4,000 expert-level questions covering mathematics, physics, chemistry, and biology.<n>Each question is equipped with reference answers and diverse responses.
  arXiv  Detail & Related papers  (2025-07-14T03:45:24Z)
• A Chain-of-Thought Is as Strong as Its Weakest Link: A Benchmark for Verifiers of Reasoning Chains [33.46649770312231]
  Prompting language models to provide step-by-step answers is a prominent approach for complex reasoning tasks. No fine-grained step-level datasets are available to enable thorough evaluation of such verification methods. We introduce REVEAL: Reasoning Verification Evaluation, a dataset to benchmark automatic verifiers of complex Chain-of-Thought reasoning.
  arXiv  Detail & Related papers  (2024-02-01T12:46:45Z)
• ROSCOE: A Suite of Metrics for Scoring Step-by-Step Reasoning [63.77667876176978]
  Large language models show improved downstream task interpretability when prompted to generate step-by-step reasoning to justify their final answers. These reasoning steps greatly improve model interpretability and verification, but objectively studying their correctness is difficult. We present ROS, a suite of interpretable, unsupervised automatic scores that improve and extend previous text generation evaluation metrics.
  arXiv  Detail & Related papers  (2022-12-15T15:52:39Z)

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.