Image de couverture de livre

MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Xie, Zixuan, Liu, Xinyu, Zhang, Shangtong
Format:	Preprint
Publié:	2026
Sujets:	Logic in Computer Science Artificial Intelligence Machine Learning
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics
par: Liu, Xinyu, et autres
Publié: (2026)

Formal Mathematical Reasoning: A New Frontier in AI
par: Yang, Kaiyu, et autres
Publié: (2024)

Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs
par: Yousefzadeh, Roozbeh, et autres
Publié: (2025)

Solving Formal Math Problems by Decomposition and Iterative Reflection
par: Zhou, Yichi, et autres
Publié: (2025)

Formal Explanations for Neuro-Symbolic AI
par: Paul, Sushmita, et autres
Publié: (2024)

What are the Right Symmetries for Formal Theorem Proving?
par: Olejniczak, Krzysztof, et autres
Publié: (2026)

LeanAgent: Lifelong Learning for Formal Theorem Proving
par: Kumarappan, Adarsh, et autres
Publié: (2024)

Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
par: Wu, Haoze, et autres
Publié: (2024)

Proving the Coding Interview: A Benchmark for Formally Verified Code Generation
par: Dougherty, Quinn, et autres
Publié: (2025)

MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classification
par: Li, Sirui, et autres
Publié: (2025)

A Semantic Search Engine for Mathlib4
par: Gao, Guoxiong, et autres
Publié: (2024)

Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces
par: Chevallier, Mark, et autres
Publié: (2025)

Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs
par: Zhang, Terry Jingchen, et autres
Publié: (2025)

Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning
par: Sälzer, Marco, et autres
Publié: (2024)

A Neurosymbolic Approach to Natural Language Formalization and Verification
par: Bayless, Sam, et autres
Publié: (2025)

BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving
par: Lamont, Sean, et autres
Publié: (2024)

Mathematics with large language models as provers and verifiers
par: Duc, Hieu Le, et autres
Publié: (2025)

Geometry of Reason: Spectral Signatures of Valid Mathematical Reasoning
par: Noël, Valentin
Publié: (2026)

Bolzano: Case Studies in LLM-Assisted Mathematical Research
par: Balko, Martin, et autres
Publié: (2026)

CLEVER: A Curated Benchmark for Formally Verified Code Generation
par: Thakur, Amitayush, et autres
Publié: (2025)

REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
par: Shen, Ziju, et autres
Publié: (2025)

Formal Methods Meet LLMs: Auditing, Monitoring, and Intervention for Compliance of Advanced AI Systems
par: Alamdari, Parand A., et autres
Publié: (2026)

Learning Formal Mathematics From Intrinsic Motivation
par: Poesia, Gabriel, et autres
Publié: (2024)

An In-Context Learning Agent for Formal Theorem-Proving
par: Thakur, Amitayush, et autres
Publié: (2023)

FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels
par: Jiang, Jiedong, et autres
Publié: (2025)

Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs
par: Li, Guchan, et autres
Publié: (2026)

Linear $Q$-Learning Does Not Diverge in $L^2$: Convergence Rates to a Bounded Set
par: Liu, Xinyu, et autres
Publié: (2025)

JustLogic: A Comprehensive Benchmark for Evaluating Deductive Reasoning in Large Language Models
par: Chen, Michael K., et autres
Publié: (2025)

PREMAP: A Unifying PREiMage APproximation Framework for Neural Networks
par: Zhang, Xiyue, et autres
Publié: (2024)

Scaling the Explanation of Multi-Class Bayesian Network Classifiers
par: Zhang, Yaofang, et autres
Publié: (2026)

Extracting Formulae in Many-Valued Logic from Deep Neural Networks
par: Zhang, Yani, et autres
Publié: (2024)

SFT-GRPO Data Overlap as a Post-Training Hyperparameter for Autoformalization
par: Su, Xiaole, et autres
Publié: (2026)

SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas
par: Wei, Anjiang, et autres
Publié: (2025)

Conditional Logical Message Passing Transformer for Complex Query Answering
par: Zhang, Chongzhi, et autres
Publié: (2024)

A Reinforcement Learning based Reset Policy for CDCL SAT Solvers
par: Li, Chunxiao, et autres
Publié: (2024)

Automated Design of Linear Bounding Functions for Sigmoidal Nonlinearities in Neural Networks
par: König, Matthias, et autres
Publié: (2024)

SATformer: Transformer-Based UNSAT Core Learning
par: Shi, Zhengyuan, et autres
Publié: (2022)

TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?
par: Taylor, Alexander K, et autres
Publié: (2026)

PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
par: Tsoukalas, George, et autres
Publié: (2024)

MathConstraint: Automated Generation of Verified Combinatorial Reasoning Instances for LLMs
par: Pati, Viresh, et autres
Publié: (2026)