Logic, programming, and type systems

Últimos artículos

• FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification

  Naing Oo Lwin · 2 de octubre de 2026

  Coding agents increasingly automate Lean proof development, but successful compilation alone does not establish that a candidate proves the intended statement under acceptable assumptions. We present FORALL-LEAN-AGENT, a frontend-agnostic framework for auditable reasoning in formal mathematics and s…

• Can AI Oversight Be Zero Knowledge?

  Alessandro Chiesa, Ziyi Guan, Burcu Yildiz · 2 de octubre de 2026

  AI systems increasingly produce outputs from confidential data, such as a fitness-for-duty assessment from medical records or the predicted properties of a drug candidate from its secret structure. It is important to verify that such outputs are correct without revealing the underlying data. A recen…

• From Verification Failures to Reusable Guidance for Coding Agents

  Yuqing Zhai, Xiaohong Chen, Lingming Zhang, Sriram Vishwanath, Grigore Rosu · 1 de octubre de 2026

  Coding agents need to establish that a program satisfies a specification and that the specification captures the requested behavior. We study how expert diagnosis of verification failures can become reusable guidance for this work. Our approach combines executable language definitions in the K frame…

• Cogentic: Multi-Agent Orchestration for Automated Proof Discovery

  Yang Cai, Vineet Gupta, Yanchen Jiang, Christopher Liaw, Aranyak Mehta, Grigoris Velegkas, Di Wang · 1 de octubre de 2026

  We present Cogentic, a multi-agent harness for automated proof discovery on open research problems. While frontier language models can generate strong mathematical ideas in a single shot, single-shot generation is often insufficient for open problems that require exploring multiple competing conject…

• Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean

  Jules Viennot, Guillaume Baudart, Marc Lelarge · 1 de octubre de 2026

  Recent achievements in AI-assisted mathematics require intensive interaction of agents with proof assistants to generate machine-checked proof certificates. Agents interact with proof assistants such as Rocq or Lean through an interface that controls what the agent receives from the prover and the c…

• Semantic Prefix Oracles for LLM Decoding: Contracts and Differential Validation

  Paul Kronlund-Drouault · 30 de septiembre de 2026

  Constrained decoding can enforce regular or context-free output formats, but many program-generation failures are semantic: scope, typing, and declaration effects depend on context. We present semantic grammar specifications, a declarative formalism that attaches such constraints to a context-free s…

• Verification of PETSc with CIVL using LLM-generated ACSL contracts and deterministic driver generation

  Hansol Suh, Jan H\"uckelheim, Stephen Siegel · 30 de septiembre de 2026

  Parallel numerical libraries such as PETSc are widely used in science and engineering applications where wrong results can have costly consequences. Despite this, numerical libraries are rarely formally verified. One of the challenges is the need for an expert to hand-write a specification and manua…

• Sage: Formalization with Semantic Correction

  Thomas Hirtz, Farzad Jafarrahmani, Abdelmouksit Sagueni, Xiang Zhou, Wengping Deng, Liang Zhang · 30 de septiembre de 2026

  While neural theorem provers have achieved impressive milestones in formal mathematics, they largely operate on the assumption that faithful Lean 4 formal statements are already provided. Translating informal natural language into a formal language is a critical data bottleneck plagued by an "illusi…

• Learning to Prove, Not Just to Answer: Reinforcement Learning from Formal Verification for Natural-Language Logical Reasoning

  Qili Zhang, Qianren Mao, Hanze Cai, Kaiming Zhao, Yuening He, Xihan Lei, Yashuo Luo, Hanwen Hao, Yutong Gu, Likang Xiao, Zhijun Chen, Weifeng Jiang, Haoyi Zhou, Jianxin Li · 30 de septiembre de 2026

  Large language models (LLMs) are increasingly deployed for natural-language logical reasoning, where the final answer is easy to check but the proof behind it is not. In natural-language logical reasoning, an intermediate conclusion should follow from its premises, and the resulting derivation shoul…

• TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science

  Chutong Yang, Xiyuan Zhang, Yu Huang, Boran Han, Soonho Kong, Shuai Zhang, Vihang Prakash Patil, Zhen Han, Michael Bohlke-Schneider, Bernie Wang · 29 de septiembre de 2026

  Large language models perform strongly on competition mathematics, but their research-level reasoning remains difficult to evaluate systematically. Theoretical computer science (TCS) connects algorithm design to explicit guarantees and fundamental limits, providing a setting for evaluating whether m…

• ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization

  Feiming Wang, Daibo Li, Kun Yuan · 29 de septiembre de 2026

  Formalizing research-level stochastic optimization in Lean requires both an algorithm model and domain theory connecting foundational libraries to convergence proofs. Revising a model to restore provability can change the mathematical claim. We introduce ProofLoom, a fully automated LLM-agent system…

• Fewer Assumptions by Design: A Reusable Skill for LLM-Assisted Verus Verification

  Andrada-Livia Antoneac (Alexandru Ioan Cuza University of Ia\c{s}i, Bitdefender), Dorel Lucanu (Alexandru Ioan Cuza University of Ia\c{s}i), Drago\c{s} Teodor Gavrilu\c{t} (Alexandru Ioan Cuza University of Ia\c{s}i, Bitdefender) · 29 de septiembre de 2026

  LLM-assisted Verus verification is a less tedious method to verify Rust implementations, but paired with self-referential structures, e.g., Doubly Linked Lists (DLLs)—notoriously difficult to formalise for verification—it becomes a substantially more demanding verification task. Moreover, a s…

• Learning Strategies to Break Judges

  Guruprerana Shabadi, Aaditya Naik, Rajeev Alur, Mayur Naik · 29 de septiembre de 2026

  As AI agents surpass human performance, it becomes exceedingly hard for system designers to evaluate them directly and understand their failure modes. Consequently, agents themselves are being deployed extensively to evaluate, judge, and provide feedback on model traces. But this raises an important…

• Choir: An Open Protocol for Distributed Multi-Agent Autoformalization

  Yidi Qi, Melanie Weber · 29 de septiembre de 2026

  AI agents can now formalize entire textbooks and major theorems in proof assistants such as Lean, but current efforts are typically centralized: a single team runs all agents and bears the full computational cost. We introduce Choir, an open protocol for distributed formalization. Choir decomposes a…

• PROOF: Profiling Reliability of Object-Level Facts in Large Language Models

  Andrei Chetvergov, Mikhail Solovev, Timofei Sivoraksha, Stepan Ukolov, Valeriia Kuschenko, Alexander Evseev, Sergey Bolovtsov · 25 de septiembre de 2026

  Aggregate factuality scores hide where a language model succeeds, which relations it confuses, and whether an answer survives innocuous changes to the question or decoder. We introduce PROOF, a profile-oriented benchmark for factual coverage in instruction-tuned language models. PROOF converts a fro…

• Direct Optimization of Generators for Search in Automated Theorem Proving

  Adam Ousherovitch, Ambuj Tewari · 23 de septiembre de 2026

  Fine-tuned Large Language Models (LLMs) significantly advance Automated Theorem Proving (ATP), but are often deployed as guiding policies within tree search rather than for single-attempt generation. Recent work shows cross entropy is suboptimal for an LLM used in flat search strategies such as aggr…

• Lean Pool: An AI-Maintained Archive of Formalized Mathematics

  Vasily Ilin · 23 de septiembre de 2026

  Lean Pool is a repository of formalized mathematics. It is grown, maintained and optimized by AI agents.…

• Human-LLM Deliberation as Interactive Proof: Conditions for Verifiability Without Transparency

  Baotong Zhang, Dean Foster, Jo\~ao Sedoc · 22 de septiembre de 2026

  When an LLM supplies an argument that a user could not readily construct, how can the user decide whether to accept its claim? Inspired by interactive proofs, we model human-LLM deliberation as an interaction between a prover with unrestricted internal search and a resource-bounded human verifier. T…

• SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?

  George Ma, Benjamin Mikek, Haoyu Li, Ferhat Erata, Yuhao Zhang, Zeren Shui, Behrooz Omidvar Tehrani, Jun Huan, Murali Krishna Ramanathan, Somayeh Sojoudi, Hao Zhou, Anoop Deoras · 21 de septiembre de 2026

  Ensuring the correctness of LLM-generated code is a core challenge for modern software engineering. Benchmarks for agentic code generation check correctness with held-out test suites, which are inherently incomplete and increasingly susceptible to memorization. Formal verification avoids both proble…

• Long-horizon autoformalization of a core theorem underlying MIP* = RE

  Sirui Lu, Ruixuan Deng, Yanqiao Zhu, Zhengfeng Ji · 18 de septiembre de 2026

  Landmark mathematical formalizations have taken specialist teams years to complete. We present FormalFlow, a system that coordinates AI proving agents under human supervision to address statement drift and proof composition in long-horizon formalization. Drawing on software engineering principles an…

• Autoformalizing Argumentative Material Inferences

  Xin Quan, Reto Gubelmann, Andr\'e Freitas · 16 de septiembre de 2026

  Natural language arguments are compelling before they are formally explicit. A premise supports a claim through defeasible warrants, background commitments, and exception conditions that the text leaves implicit. However, formal verification requires the opposite. Making such arguments machine-check…

• Proving olympiad geometry theorems on a superconducting quantum processor

  Ning Wang, Zheng-Zhi Sun, Zhengyi Cui, Yiren Zou, Aosai Zhang, Fanhao Shen, Jiarun Zhong, Zehang Bao, Zitian Zhu, Han Wang, Jia-Nan Yang, Jiayuan Shen, Gongyu Liu, Yanzhe Wang, Yihang Han, Yiyang He, Jiahua Huang, Sailang Zhou, Xinrong Zhang, Yaozu Wu, Zixuan Song, Jinfeng Deng, Hang Dong, Qi Ye, Weikang Li, Si Jiang, Yixuan Ma, Shuangyue Geng, Zhide Lu, Chao Song, Hekang Li, Pengfei Zhang, Qiujiang Guo, H. Wang, Dong-Ling Deng · 15 de septiembre de 2026

  Automated theorem proving seeks to use computational systems to prove or disprove mathematical and logical statements [1, 2]. It underpins a wide range of applications, and enhancing theorem-proving capabilities remains a central objective in artificial intelligence [3]. Although recent neuro-symbol…

• Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science

  Honghao Lin, David P. Woodruff, Yuan Deng, Jieming Mao, Song Zuo, Vahab Mirrokni · 15 de septiembre de 2026

  Language models can produce plausible short proofs, but may still be unreliable on long-horizon research problems, where progress depends on a sequence of uncertain and interdependent decisions. We introduce Stellar Colosseum, a model-agnostic harness for allocating inference across research in math…

• Toward a First-Principles Update Geometry for the Language-Model Head

  Aditya Somasundaram, Charles Guille-Escuret, Alexander Moreno, Zhengzhong Liu, Eric Xing · 11 de septiembre de 2026

  Muon motivates designing optimizer geometry around the function of each parameter block and uses the spectral norm for hidden linear layers. For the language-model head, the spectral norm is not a faithful measure of functional change. Softmax removes shared logit shifts, whereas the spectral norm c…

• Beyond Solver Verdicts: Generative Reward Models for Autoformalization

  Vikash Singh, Debargha Ganguly, Aman Goel, Ali Torkamani, Xiaoxue Han, Joseph Lilien, Ferhat Erata, Vipin Chaudhary · 11 de septiembre de 2026

  Neurosymbolic systems rely on mathematical solvers to guarantee reasoning correctness, yet solvers are fundamentally blind to whether a formal translation maintains strict reference-equivalence to a designated formalization. We formalize this vulnerability as Verdict-Preserving-Unfaithfulness (VPU):…