Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.35269

MechAlign: Evaluating Semantic Alignment at the Project Level in Mathematical Formalization

Hao Shen·Ruichen Qiu·Lihong Zhi·Xiao-Shan Gao
View original source ↗Read source document ↗Export metadata ↓

Abstract

Lean verifies that a formal proof establishes its stated proposition under declared assumptions, but does not check whether that proposition faithfully expresses the mathematical claim in a manuscript. Assessing this correspondence requires interpreting the main theorem through its project dependencies, which may be scattered throughout a large development. We introduce MechAlign, a framework for project-level semantic alignment review that combines formal dependency extraction with LLM-based assessment. Its extraction tool, LeanTrace, constructs a statement dependency graph from elaborated declarations, retaining definition bodies and structure constraints while excluding proof bodies and stopping at an explicit library boundary. The reviewer uses this context to investigate alignment and report discrepancies with localized evidence. We conduct a preliminary review of 201 main results from 173 OpenAI Math projects, using supplied informal descriptions and available paper context. A hyperbolic-group case illustrates how dependency inspection localizes a missing dimensional constraint relative to the manuscript, consistent with the upstream declaration of formalization scope. We also construct LeanReviewBench, comprising 501 fixed claim-statement-context triples from OpenAI Math, Fermat's Last Theorem, and Kakeya, with description provenance recorded. The resource supports controlled comparisons of more project-level semantic alignment evaluations.

Explore related subjects

cs.CL

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Hao Shen, Ruichen Qiu, Lihong Zhi, Xiao-Shan Gao. 2026-10-26. MechAlign: Evaluating Semantic Alignment at the Project Level in Mathematical Formalization. https://arxiv.org/abs/2610.35269

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Auto-AdvER: Disentangling Condition, History, and Commercial Offers in Automotive Advertisements

This paper presents a case study on the development of Auto-AdvER, a specialised span-labelling schema, along with its corresponding dataset for the textual car advertisement domain. Developed with industry needs in mind, Auto-AdvER is designed to enhance text mining analytics in this domain and contributes a linguistically unique sequence-labelling dataset. We introduce a schema consisting of three labels: 'Condition', 'Historic', and 'Sales Options'. We outline the guiding principles for annotation, describe the methodology for schema development, and present the results of an annotation study demonstrating an inter-annotator agreement of 78%. Furthermore, we compare the performance of various models, including transformer encoder models (BERT, DeBERTaV3) and transformer decoder-based open- and closed-source large language models: Llama, Qwen, GPT, and Gemini, as well as conditional random fields. Our results show that a fine-tuned DeBERTaV3 encoder achieves the highest F1-score, followed closely by conditional random fields, while the large language models reach the highest precision but lower recall. We present this work as a stepping stone towards more fine-grained analysis and discuss Auto-AdvER's potential impact on advertisement analytics, pricing, and customer insights. Potential applications include the analysis of market dynamics and data-driven predictive maintenance.

cs.CL↗
arXiv2026

Large Language Model probabilities cannot reliably distinguish between possible and impossible language

A controversial test for Large Language Models concerns the ability to discern possible from impossible language. While some evidence attests to the models sensitivity to what crosses the limits of grammatically impossible language, this evidence has been contested on the grounds of the soundness of the testing material. We use model-internal representations as a direct means of investigating the way Large Language Models represent the grammatical-ungrammatical distinction. In a novel benchmark, we elicit sum log probabilities from 8 models and compute minimal-pair surprisal differences, juxtaposing probabilities assigned to grammatical sentences to probabilities assigned to (i) lower frequency grammatical sentences, (ii) ungrammatical sentences, (iii) semantically odd sentences, and (iv) pragmatically odd sentences. The prediction is that if string-probabilities can function as proxies for the limits of grammar, the ungrammatical condition will stand out among the conditions that involve linguistic violations, showing a spike in the surprisal rates. Our results do not reveal a unique surprisal signature for ungrammatical prompts: across models, we observe comparable surprisal for the pragmatically odd condition, and the semantically odd condition consistently shows even higher surprisal. We thus demonstrate that probabilities do not constitute reliable proxies for grammaticality, showing that probability differences alone cannot be used to infer model-internal representations of syntactic knowledge. Consequently, claims about models being able to distinguish possible from impossible language need verification through a different methodology.

cs.CL↗
arXiv2026

KnowMT-Bench: Benchmarking Knowledge-Intensive Long-Form Question Answering in Multi-Turn Dialogues

Multi-Turn Long-Form Question Answering (MT-LFQA) is a key application paradigm of Large Language Models (LLMs) in knowledge-intensive domains. However, existing benchmarks are limited to single-turn dialogue, while multi-turn dialogue benchmarks typically assess other orthogonal capabilities rather than knowledge-intensive factuality. To bridge this critical gap, we introduce \textbf{KnowMT-Bench}, a new benchmark designed to systematically evaluate MT-LFQA for LLMs across knowledge-intensive fields, including medicine, finance, and law. To faithfully assess the model's real-world performance, KnowMT-Bench employs a dynamic evaluation setting where models generate their own multi-turn dialogue histories given logically progressive question sequences. Our experiments on a diverse suite of LLMs show a clear degradation in both factual capability and information delivery efficiency in multi-turn dialogue. We further probe the underlying causes and investigate mitigation strategies spanning domain-specific finetuning, active context denoising, and RAG. The results show domain-dependent gains from finetuning, while active context denoising and RAG more consistently mitigate these issues, with RAG notably reversing this performance degradation. These findings underscore the importance of our benchmark for evaluating LLMs' conversational factual capabilities in real-world applications. Code and data are publicly available.\footnote{\href{https://github.com/Sven-LI-sankyuu/KnowMT-Bench}{\texttt{https://github.com/Sven-LI-sankyuu/KnowMT-Bench}}}

cs.CL↗