Humanize Olympiad Agents: A Multi-Session Workflow for Olympiad Problem Solving with Solve, Review, Wiki, Verify
cs.AI
Submitted: 2026-10-09
Updated: 2026-10-09
Code: https://github.com/humanfia/hoa
License: http://creativecommons.org/licenses/by/4.0/
The gist: Large language model (LLM) agents are rapidly improving on long-horizon scientific and olympiad tasks.
Abstract
Large language model (LLM) agents are rapidly improving on long-horizon scientific and olympiad tasks. Recent systems have produced a Lean-formalized resolution of the Navier--Stokes problem and autonomous solutions to four open questions in the Erdős Conjectures database. Yet neither system releases both its underlying model and complete inference stack. More broadly, a single agent session remains brittle on difficult problems: early errors can propagate, missing domain knowledge can stall progress, and apparent success can mask a misinterpretation or weakening of the original task. We introduce HOA (Humanize Olympiads Agent), an open, flow-level framework that coordinates multiple agent sessions through three complementary feedback channels. First, an independent reviewer evaluates each candidate and provides actionable feedback. Second, a structured wiki supplies task-specific knowledge that may be missing or unreliable in model pretraining. Third, a verifier checks generated Lean proofs against trusted challenge statements. With GPT-5.6 Sol, HOA achieves perfect scores on the IMO, IPhO, and IOI 2026, near-full marks on the IChO 2026 problem set, and solves all 672 problems (100%) on PutnamBench. On the Lean-Eval leaderboard, HOA ranks first, solving 251 of 304 problems (82.6%). We further evaluate HOA with open models. Using Kimi-K3, HOA achieves full scores on the IMO, IPhO, and IOI, and a gold-level score of 97.1% on the IChO. These results closely match the closed-source GPT-5.6 Sol + /Goal baseline on the IMO and IPhO, while exceeding it on the IChO and IOI, demonstrating that systematic feedback can help bridge substantial differences in base-model capability.
Sources
- LeanExplore: A search engine for Lean 4 declarations
- MLE-bench: Evaluating Machine Learning Agents on Machine Learning Engineering
- Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
- Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
- Towards Autonomous Mathematics Research
- CRITIC: Large Language Models Can Self-Correct with Tool-Interactive Critiquing
- Large Language Models Cannot Self-Correct Reasoning Yet
- Winning Gold at IMO 2025 with a Model-Agnostic Verification-and-Refinement Pipeline
- Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
- LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
- Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks
- HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving
- Lean-STaR: Learning to Interleave Thinking and Proving
- Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
- Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
- Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
- OProver: A Unified Framework for Agentic Formal Theorem Proving
- Self-Refine: Iterative Refinement with Self-Feedback
- AlphaEvolve: A coding agent for scientific and algorithmic discovery
- Reflexion: Language Agents with Verbal Reinforcement Learning
Related papers
- MAVEN-T: Reinforced Heterogeneous Distillation for Real-Time Multi-Agent Trajectory Prediction
- Model Discovery Agent: LLM-assisted Bayesian experiment design for data-efficient discovery of mechanistic world models
- Agents' Last Exam
- The Clinician's Veto: Navigating Trust, Liability, and Uncertainty in Autonomous AI Prescribing
- MindHelper: Closed-Loop Embodied Mental-State Reasoning for Precision Intervention
- Incumbent Advantage: Brand Bias and Cognitive Manipulation Dynamics in LLM Recommendation Systems