Sequent-Prover: Training Agents for Formal, Checkable SMT-based Reasoning
cs.CL, cs.AI, cs.LG, cs.LO
Submitted: 2026-10-11
Updated: 2026-10-11
Code: https://github.com/DebarghaG/proofofthought
Sources
- Evaluating Large Language Models Trained on Code
- Think you have Solved Question Answering? Try ARC, the AI2 Reasoning Challenge
- Transformers as Soft Reasoners over Language
- Training Verifiers to Solve Math Word Problems
- VeriCoT: Neuro-symbolic Chain-of-Thought Validation via Logical Consistency Checks
- Measuring Massive Multitask Language Understanding
- CASP: An evaluation dataset for formal verification of C code
- BIG-Bench Extra Hard
- Measuring Faithfulness in Chain-of-Thought Reasoning
- ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoning
- Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
- Understanding R1-Zero-Like Training: A Critical Perspective
- DafnyBench: A Benchmark for Formal Software Verification
- LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers
- DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
- Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought
- DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models
- VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning
- Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
- DAPO: An Open-Source LLM Reinforcement Learning System at Scale
Related papers
- Exploring Solution Divergence and Its Effect on Large Language Model Problem Solving
- Ishigaki-IDS-Bench: A Benchmark for Generating Information Delivery Specification from BIM Information Requirements
- Subliminal Steering: Stronger Encoding of Hidden Signals
- MedStruct-S: A Benchmark for Key Discovery, Key-Conditioned QA and Semi-Structured Extraction from OCR Clinical Reports
- The End of Transformers? On Challenging Attention and the Rise of Sub-Quadratic Architectures
- Untangling the Mechanisms of Misleading Context in Medical Question Answering