BEAVER is the first practical deterministic verifier that maintains sound probability bounds on LLM safety properties using token tries and frontier data structures, finding 2-3x more violations than sampling at 1/10 the compute.
hub
Gold-medalist performance in solving olympiad geometry with alphageometry2
14 Pith papers cite this work, alongside 2 external citations. Polarity classification is still indexing.
14
Pith papers citing it
2
external citations · external index
hub tools
citation-role summary
background 2
citation-polarity summary
roles
background 2polarities
background 2representative citing papers
LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.
VERITAS improves zero-shot formal theorem proving to 40.6% on miniF2F and 7.3% on a new combinatorics benchmark by routing verifier signals into a two-phase Best-of-N then critic-guided MCTS protocol.
Synthetic data improves models only in information-open generation-training loops with external signals, and coarser signals like binary correctness enable better generalization by converging to the most information-efficient component.
Frontier AI models score below 10% on Riemann-Bench, a private expert-authored benchmark of research-level mathematics with closed-form, programmatically verified solutions.
A hybrid pipeline lets an LLM write high-level proof sketches in a compact DSL that a lightweight kernel then expands into explicit, checkable obligations for reliable math and logic reasoning.
Ax-Prover is a tool-using multi-agent LLM system that matches state-of-the-art provers on public math benchmarks and outperforms them on new abstract-algebra and quantum-theory benchmarks while also assisting an expert with a cryptography proof.
Aristotle reaches gold-medal-equivalent performance on 2025 IMO problems via integrated Lean proof search, informal lemma formalization, and a dedicated geometry solver.
KG-R1 trains a single RL agent to retrieve from and reason over knowledge graphs in one loop, achieving higher accuracy with fewer tokens than multi-module baselines and transferring to unseen graphs.
AI for mathematics is best described as a supervision ladder — final answers, programs, process rewards, proof-assistant kernels — culminating in verified-discovery workflows.
The paper introduces the 'topological dual of a dataset' — translating observable-logic sequents into covering-sieve statements on Grothendieck sites — as a new input representation for neuro-symbolic AI systems like AlphaGeometry.
AI4EOSC combines federated cloud scheduling, serverless inference, FAIR metadata, and provenance into one open platform for European research AI.
Pass-rate rewards in critic-free RL for code generation fail to outperform binary rewards because partial-pass solutions induce conflicting gradient directions that do not consistently favor full correctness.
AI for math combines task-specific architectures and general foundation models to support research and advance AI reasoning capabilities.
citing papers explorer
-
BEAVER: An Efficient Deterministic LLM Verifier
BEAVER is the first practical deterministic verifier that maintains sound probability bounds on LLM safety properties using token tries and frontier data structures, finding 2-3x more violations than sampling at 1/10 the compute.
-
From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.
-
VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving
VERITAS improves zero-shot formal theorem proving to 40.6% on miniF2F and 7.3% on a new combinatorics benchmark by routing verifier signals into a two-phase Best-of-N then critic-guided MCTS protocol.
-
An Information-Theoretic Criterion for Efficient Data Synthesis
Synthetic data improves models only in information-open generation-training loops with external signals, and coarser signals like binary correctness enable better generalization by converging to the most information-efficient component.
-
Riemann-Bench: A Benchmark for Moonshot Mathematics
Frontier AI models score below 10% on Riemann-Bench, a private expert-authored benchmark of research-level mathematics with closed-form, programmatically verified solutions.
-
ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning
A hybrid pipeline lets an LLM write high-level proof sketches in a compact DSL that a lightweight kernel then expands into explicit, checkable obligations for reliable math and logic reasoning.
-
Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics
Ax-Prover is a tool-using multi-agent LLM system that matches state-of-the-art provers on public math benchmarks and outperforms them on new abstract-algebra and quantum-theory benchmarks while also assisting an expert with a cryptography proof.
-
Aristotle: IMO-level Automated Theorem Proving
Aristotle reaches gold-medal-equivalent performance on 2025 IMO problems via integrated Lean proof search, informal lemma formalization, and a dedicated geometry solver.
-
Efficient and Transferable Agentic Knowledge Graph RAG via Reinforcement Learning
KG-R1 trains a single RL agent to retrieve from and reason over knowledge graphs in one loop, achieving higher accuracy with fewer tokens than multi-module baselines and transferring to unseen graphs.
-
Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery
AI for mathematics is best described as a supervision ladder — final answers, programs, process rewards, proof-assistant kernels — culminating in verified-discovery workflows.
-
The Topological Dual of a Dataset: A Logic-to-Topology Encoding for AlphaGeometry-Style Data
The paper introduces the 'topological dual of a dataset' — translating observable-logic sequents into covering-sieve statements on Grothendieck sites — as a new input representation for neuro-symbolic AI systems like AlphaGeometry.
-
AI4EOSC: a Federated Cloud Platform for Artificial Intelligence in Scientific Research
AI4EOSC combines federated cloud scheduling, serverless inference, FAIR metadata, and provenance into one open platform for European research AI.
-
Exploring Pass-Rate Reward in Reinforcement Learning for Code Generation
Pass-rate rewards in critic-free RL for code generation fail to outperform binary rewards because partial-pass solutions induce conflicting gradient directions that do not consistently favor full correctness.
-
AI for Mathematics: Progress, Challenges, and Prospects
AI for math combines task-specific architectures and general foundation models to support research and advance AI reasoning capabilities.