Imagen de Portada

Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Baudart, Guillaume, Lelarge, Marc, Stérin, Tristan, Viennot, Jules
Formato:	Preprint
Publicado:	2026
Materias:	Machine Learning Computation and Language Logic in Computer Science
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
por: Viennot, Jules, et al.
Publicado: (2025)

TensorRocq: Enabling diagrammatic reasoning in Rocq
por: Caldwell, Benjamin, et al.
Publicado: (2026)

RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation
por: Kozyrev, Andrei, et al.
Publicado: (2025)

TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq
por: Rosain, Johann, et al.
Publicado: (2026)

String Diagrams for Monoidal Categories, in Rocq
por: Pous, Damien
Publicado: (2026)

Revisiting the Fast Fourier Transform in Rocq
por: Théry, Laurent
Publicado: (2022)

RocqSmith: Can Automatic Optimization Forge Better Proof Agents?
por: Kozyrev, Andrei, et al.
Publicado: (2026)

Nominal Sets in Rocq
por: Paranhos, Fabrício Sanches, et al.
Publicado: (2025)

A Rocq Formalization of Monomial and Graded Orders
por: Boldo, Sylvie, et al.
Publicado: (2025)

Adhesive category theory for graph rewriting in Rocq
por: Arsac, Samuel, et al.
Publicado: (2025)

A Rocq Formalization of Simplicial Lagrange Finite Elements
por: Boldo, Sylvie, et al.
Publicado: (2026)

PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
por: Tsoukalas, George, et al.
Publicado: (2024)

Verified Purely Functional Catenable Real-Time Deques
por: Viennot, Jules, et al.
Publicado: (2025)

Process-Driven Autoformalization in Lean 4
por: Lu, Jianqiao, et al.
Publicado: (2024)

Learning to Estimate System Specifications in Linear Temporal Logic using Transformers and Mamba
por: Işık, İlker, et al.
Publicado: (2024)

MANTRA: Synthesizing SMT-Validated Compliance Benchmarks for Tool-Using LLM Agents
por: Anand, Ashwani, et al.
Publicado: (2026)

Hybrid Models for Natural Language Reasoning: The Case of Syllogistic Logic
por: Guzmán, Manuel Vargas, et al.
Publicado: (2025)

Process discovery on deviant traces and other stranger things
por: Chesani, Federico, et al.
Publicado: (2021)

Interchangeable Token Embeddings for Extendable Vocabulary and Alpha-Equivalence
por: Işık, İlker, et al.
Publicado: (2024)

Herald: A Natural Language Annotated Lean 4 Dataset
por: Gao, Guoxiong, et al.
Publicado: (2024)

Guiding Word Equation Solving using Graph Neural Networks (Extended Technical Report)
por: Abdulla, Parosh Aziz, et al.
Publicado: (2024)

Formal P-Category Theory and Normalization by Evaluation in Rocq
por: Berry, David G., et al.
Publicado: (2025)

The Expressive Power of Transformers with Chain of Thought
por: Merrill, William, et al.
Publicado: (2023)

Loop Invariant Generation: A Hybrid Framework of Reasoning optimised LLMs and SMT Solvers
por: Bharti, Varun, et al.
Publicado: (2025)

Boosting Few-Pixel Robustness Verification via Covering Verification Designs
por: Shapira, Yuval, et al.
Publicado: (2024)

Smart Choices and the Selection Monad
por: Abadi, Martin, et al.
Publicado: (2020)

Mini-Batch Robustness Verification of Deep Neural Networks
por: Tzour-Shaday, Saar, et al.
Publicado: (2025)

Towards a Certified Proof Checker for Deep Neural Network Verification
por: Desmartin, Remi, et al.
Publicado: (2023)

Programmatic Reinforcement Learning: Navigating Gridworlds
por: Shabadi, Guruprerana, et al.
Publicado: (2024)

Floating-Point Neural Networks Are Provably Robust Universal Approximators
por: Hwang, Geonho, et al.
Publicado: (2025)

Neural Network Verification is a Programming Language Challenge
por: Cordeiro, Lucas C., et al.
Publicado: (2025)

Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
por: Ye, Kangfeng, et al.
Publicado: (2023)

A Neurosymbolic Approach to Natural Language Formalization and Verification
por: Bayless, Sam, et al.
Publicado: (2025)

Canonical bidirectional typechecking
por: Mihejevs, Zanzi, et al.
Publicado: (2025)

Controlling Logical Collapse in LLMs via Algebraic Ontology Projection over F2
por: Miyashita, Hisashi, et al.
Publicado: (2026)

Geometry of Reason: Spectral Signatures of Valid Mathematical Reasoning
por: Noël, Valentin
Publicado: (2026)

ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization
por: Ahuja, Riyaz, et al.
Publicado: (2026)

Bolzano: Case Studies in LLM-Assisted Mathematical Research
por: Balko, Martin, et al.
Publicado: (2026)

JustLogic: A Comprehensive Benchmark for Evaluating Deductive Reasoning in Large Language Models
por: Chen, Michael K., et al.
Publicado: (2025)

SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas
por: Wei, Anjiang, et al.
Publicado: (2025)