File size: 1,963 Bytes
cf5fd96 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 | cff-version: 1.2.0
title: "RagSolver: a multi-agent system for olympiad-style problem solving with embeddings-based retrieval and Lean 4 verification"
message: "If you use this software, please cite it as below."
type: software
authors:
- given-names: "Camilo Andres"
family-names: "Niño Amaya"
affiliation: "Universidad Pedagógica y Tecnológica de Colombia (UPTC), Sogamoso"
- given-names: "Jose L."
family-names: "Salamanca"
affiliation: "Universidad Pedagógica y Tecnológica de Colombia (UPTC), Sogamoso"
version: 0.2.0
date-released: "2026-10-21"
license: Apache-2.0
repository-code: "https://github.com/camiloAndres11/RagSolver"
abstract: >-
Multi-agent pipeline (planner, retriever, generator, autoformalizer, verifier, critic)
orchestrated with LangGraph that solves competition mathematics problems and certifies
solutions with the Lean 4 kernel and Mathlib (v4.28.0-rc1). Retrieval-augmented generation
over the LeanSearch v2 informalized Mathlib corpus (LanceDB, hybrid dense + BM25) and over
a corpus of solved olympiad problems parsed from PDF (MinerU + VLM figure descriptions). A locally served
Lean prover (Goedel-Prover-V2-8B) is the first stage; the agents and retrieval act on what it leaves
unsolved (draft-sketch-prove, step-wise repair, Lean skeletons, retrieval of verified proofs of similar problems).
keywords: [Lean 4, Mathlib, retrieval-augmented generation, multi-agent systems, theorem proving, miniF2F, Goedel-Prover-V2]
references:
- type: dataset
title: "lsv2-mathlib-v4.28.0-rc1-jsonl (LeanSearch v2 corpus)"
authors: [{name: "FrenzyMath"}]
license: Apache-2.0
- type: dataset
title: "miniF2F-v2"
authors: [{name: "roozbeh-yz"}]
license: Apache-2.0
- type: software
title: "Goedel-Prover-V2-8B"
authors: [{name: "Goedel-LM"}]
license: Apache-2.0
- type: dataset
title: "Lean-workbook-proofs"
authors: [{name: "Goedel-LM"}]
license: MIT
|