Fateme Mazdarani

Proof-generating systems return many candidates for the same theorem. Lean's kernel determines whether each candidate is correct, but not whether the candidates contain different mathematical reasoning. We study one measurable component of mathematical creativity: whether repeated successful generations explore distinct proof ideas rather than new formal expressions of the same idea. We analyze LeanRoute-216, which began with 36 kernel-verified and human-reviewed Lean proofs for 36 fixed propositions. Five additional proofs were then generated for each proposition with the goal of obtaining diverse proofs, producing 216 kernel-verified proofs in total. A graph-derived route-level review identified 61 diverse routes among the 216 distinct proof strings. This observation motivated a closer study of the distinction between formal variation and mathematical route diversity. Across the benchmark's 180 parent-candidate pairs, 25 were labeled as route changes and 155 as same-route comparisons. All pairs of candidate proofs were human-evaluated in a blinded second pass, with 95.6% agreement with the original route-change labels (κ = 0.793). Five theorem panels were used to refine the rubric and judging prompts, while the remaining 31 panels were held out for evaluation. On these 31 panels, LLM judges recognize route changes more reliably than lexical baselines, but remain substantially weaker at identifying the kind of change. These results support route diversity as an evaluation target separate from correctness and show how route-level auditing can inform proof search and the curation of synthetic reasoning data.

Mathematical reasoning systems should be consistent when the same concept is expressed in equivalent forms. This requires not only recognizing shared mathematical meaning but also identifying the representation changes and reconstructing a traceable route between forms. We study this problem through mathematical theorems, whose equivalent formulations preserve the same underlying result while differing substantially in representation. In this setting, theorem recognition is only the first step: a robust system must also identify the intervening transformations and recover their order. We introduce an evaluation of robust procedural mathematical reasoning with three components: theorem identification, transformation identification, and ordered reconstruction. Using validated theorem-representation pairs from an existing corpus, we build a procedural-robustness dataset with typed operations, reference procedures, and matched contrasts that distinguish valid reformulations from invalid ones. We first measure closed-book performance of four open-weight models to establish a baseline, then evaluate retrieval-augmented generation (RAG) as support mechanism for the same task. Models identify theorem identity more reliably than they recover the transformations and ordered routes connecting equivalent representations. RAG improves every stage, but procedural reconstruction remains the main bottleneck. The framework supports more consistent and traceable mathematical systems, with potential applications in mathematical search, tutoring, autoformalization, and scientific discovery.

Large language models (LLMs) are increasingly integrated into complex workflows as automated evaluators, yet their reliability in assessing unconventional reasoning processes remains under-explored. Current evaluation frameworks often overlook models' robustness to procedural equivalence, the ability to recognize valid but non-canonical paths to a correct result. In this work, we introduce a benchmark specifically designed to test LLMs in an evaluative capacity, using linear-equation problems with diverse solution variants as a controlled proxy for correctness-critical, multi-step verification tasks in science and engineering. We further define a process-centric evaluation framework across three dimensions: (i) final-answer correctness, (ii) step-level correctness, and (iii) localization of the initial logical error. Our evaluation of state-of-the-art open LLMs reveals a significant robustness gap: models that accurately evaluate canonical solutions often fail when presented with perturbed but logically equivalent variants. Models exhibit high false-negative rates by rejecting valid alternative solutions and show signs of bias. Our results suggest that while adaptation strategies can narrow this gap, achieving reliable process-level verification remains a critical challenge for deploying LLM evaluators in correctness-critical domains.

AI systems increasingly operate between flexible input representations and formal objects used by downstream tools. A key challenge is recognizing when an unfamiliar formulation denotes a known formal object. We study this challenge through theorem recognition: given an equivalence-preserving transformation of a theorem condition, a model must recover the theorem identity associated with the standard statement. We introduce TREAT, a benchmark designed to isolate this representation-dependent access problem. Rather than paraphrasing theorem text, TREAT changes the mathematical form of theorem conditions themselves, expressing known results through residual equations, witness statements, optimization identities, set relations, operator forms, and proof-intermediate characterizations. Starting from scraped theorem pages, we filter for entries with usable mathematical expression forms, extract canonical theorem conditions, and generate transformed variants with recorded assumptions and inverse mappings. The final corpus contains 737 theorem identities and 29,900 transformed rows. On a test panel, the best model retrieves the correct theorem identity in only 60.73% of cases. Other systems reveal different failure modes, including abstention, wrong-theorem commitments, and malformed structured outputs. These results suggest that theorem knowledge can be fragile under equivalent changes in representation. TREAT therefore provides a controlled testbed for evaluating representation-robust access to formal knowledge, with broader relevance to domains that require stable target objects, explicit equivalence relations, validation procedures, and auditable scoring.

Spectral co-clustering is a useful tool for discovering latent structure in word-document matrices, but its reliance on singular value decomposition (SVD) can make standard formulations expensive on high-dimensional data. This paper presents two randomized approximations for normalized spectral co-clustering of bipartite text data when the numbers of document and word clusters may differ. The first method uses randomized SVD through random projection, while the second combines partial SVD with element-wise random sampling. Across real-world and synthetic datasets, both methods reduce runtime relative to the full-SVD baseline, but their behavior depends on matrix sparsity. The random projection method is the more reliable approximation across the tested settings, whereas the sampling-based method is most useful on denser matrices and provides limited benefit on already sparse text data. These results show that randomized approximations for spectral co-clustering should be selected according to the underlying structure of the data.

Task recommendation algorithms in crowd work platforms can erode worker autonomy through strategies such as amplifying the visibility of undesirable or low-paying jobs to meet client demand. We explore whether transparency can shift these systems toward worker-centered values. We built a simulated crowd work platform comparing an opaque Baseline interface against a Transparent variant with explained recommendations and navigation cues. In a within-subjects lab study capturing an initial thirty-minute interaction (n=40), participants rated the transparent system substantially higher on fairness, trust, empowerment, and usability. Behaviorally, transparency supported more strategic task evaluation and increased recommendation alignment. Our results suggest that transparency, even in the form of lightweight disclosure, can improve trust and experience without altering the underlying algorithm. Therefore, we discuss design implications for worker-centered systems, including explanation scope and deployment trade-offs, while acknowledging that durable empowerment requires pairing transparency with meaningful agency and field validation under real economic constraints.