Theory-Scale Auto-Formalization of Logics for Computer Science

• URL: http://arxiv.org/abs/2606.26525v1
• Date: Thu, 25 Jun 2026 01:59:53 GMT
• Title: Theory-Scale Auto-Formalization of Logics for Computer Science
• Abstract summary: LCS-Bench is a theory-scale benchmark based on Logics for Computer Science.<n>The artifact covers 327 textbook items, over 4,076 Lean declarations, and more than 85K lines of Lean code.<n>We demonstrate that LCS-Bench is of high quality, consistent, and faithful.
• Score: 36.45195518081978
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Auto-formalization is critical for scalable formal verification, but existing progress largely focuses on isolated statements, while theory-scale auto-formalization, which coherently translates hundreds of interdependent definitions, lemmas, and theorems, remains open due to challenges in consistency, faithfulness, scalability, and correctness. In this paper, we introduce LCS-Bench, a stand-alone, theory-scale benchmark based on Logics for Computer Science. LCS-Bench is built through a novel semi-automated agentic pipeline that leverages concept graphs, formal signature planning, issue tracking, sorry-filling with counter-example search, complemented by faithfulness review from human experts. The resulting artifact covers 327 textbook items, over 4,076 Lean declarations, and more than 85K lines of Lean code. The dataset supports broad evaluation through a data engine that automatically derives five tracks of evaluation benchmarks, measuring different aspects of auto-formalization and theorem-proving capabilities. We also introduce a novel evaluation protocol featuring definitional equivalence checkers, enabling more fine-grained and faithful assessment. Through extensive evaluation on 14 models, we demonstrate that (1) LCS-Bench is of high quality, consistent, and faithful; (2) the benchmark is challenging, with state-of-the-art models achieving only 20.1% on auto-formalization tasks; and (3) our analysis reveals key findings regarding theory-scale auto-formalization and suggests promising directions for future work.

Related papers

• FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models [53.68149869349268]
  Large language models (LLMs) have shown growing potential for automated theoretical computer science (TCS) research.<n>We introduce ourbenchmark, an expert-validated benchmark for evaluating LLMs on frontier, end-to-end TCS research.
  arXiv  Detail & Related papers  (2026-08-20T15:13:41Z)
• From Reasoning to Agentic: Credit Assignment in Reinforcement Learning for Large Language Models [3.651838585096184]
  Reinforcement learning (RL) for large language models increasingly relies on sparse, outcome-level rewards.<n>We survey 47 CA methods published between 2024 and early 2026, organizing them in a two-dimensional taxonomy by assignment.<n>We contribute three reusable resources: (1) a structured, machine-readable paper inventory with taxonomy labels, baseline families, and evidence levels; (2) a reporting checklist for future CA papers to identify systematic methodological gaps; and (3) a benchmark protocol specification with task families, metadata requirements, and controlled bifurcation tasks.
  arXiv  Detail & Related papers  (2026-04-10T16:17:44Z)
• SciMDR: Benchmarking and Advancing Scientific Multimodal Document Reasoning [59.93568326270048]
  We introduce the synthesize synthesize framework, which generates faithful, isolated QA pairs on focused segments.<n>We construct SciMDR, a large-scale training dataset for crossmodal comprehension.<n>Experiments demonstrate that SciMDR models achieve significant improvements across multiple scientific QA benchmarks.
  arXiv  Detail & Related papers  (2026-03-12T17:57:52Z)
• Beyond Holistic Scores: Automatic Trait-Based Quality Scoring of Argumentative Essays [15.895792302323883]
  In educational contexts, teachers and learners require interpretable, trait-level feedback.<n>We study trait-based Automatic Argumentative Essay Scoring using two complementary modeling paradigms.<n>We show that explicitly modeling score ordinality substantially improves agreement with human raters.
  arXiv  Detail & Related papers  (2026-02-04T14:30:52Z)
• RPC-Bench: A Fine-grained Benchmark for Research Paper Comprehension [65.81339691942757]
  RPC-Bench is a large-scale question-answering benchmark built from review-rebuttal exchanges of high-quality computer science papers.<n>We design a fine-grained taxonomy aligned with the scientific research flow to assess models' ability to understand and answer why, what, and how questions in scholarly contexts.
  arXiv  Detail & Related papers  (2026-01-14T11:37:00Z)
• 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)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  We propose a Reflective Autoformalization method that integrates semantic consistency evaluation into the autoformalization process.<n>This enables the model to iteratively generate formal statements, assess its semantic fidelity, and self-correct identified errors.<n>Experiments show that ReForm achieves an average improvement of 22.6 percentage points over the strongest baselines.
  arXiv  Detail & Related papers  (2025-10-28T16:22:54Z)
• Conjecturing: An Overlooked Step in Formal Mathematical Reasoning [10.398167568549924]
  Many mathematical problems cannot be formalised directly without first conjecturing a conclusion.<n>We develop ConjectureBench to measure the conjecturing capabilities of Large Language Models.<n>We show that our method achieves the first successful end-to-end autoformalisation of 13 PutnamBench problems with GPT-4.1 and 7 with DeepSeek-V3.1.
  arXiv  Detail & Related papers  (2025-10-13T22:29:49Z)
• Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency [22.86318578119266]
  We introduce a novel framework that scores and selects the best result from k autoformalization candidates based on symbolic equivalence and semantic consistency.<n>Our experiments on the MATH and miniF2F datasets demonstrate that our approach significantly enhances autoformalization accuracy.
  arXiv  Detail & Related papers  (2024-10-28T11:37: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.