# mathura-snth/math-llm-verifier architecture

> Architecture diagram of the GitHub repository mathura-snth/math-llm-verifier, generated by GitDiagram from its file tree, README and a sample of source files (last updated 2026-09-30). It is an AI-made overview: check details against the source.

- Interactive diagram: https://gitdiagram.com/mathura-snth/math-llm-verifier
- Repository: https://github.com/mathura-snth/math-llm-verifier

## Overview

The active product is a reproducible benchmark generator for evaluating whether language models detect logical errors in theorem hypotheses. A user runs the benchmark, which selects theorems and error types, generates and formally validates synthetic copies, and writes labeled cases to JSON. The formal model comprises theorem requirements, hypothesis text, and implication rules. The repository also preserves an earlier French-language implementation and a Tableau exporter. The main workflow is evidenced by sampled active source; the archive is shown as a separate historical branch, not part of the active pipeline.

Main entry points: [`eng_ver/run.py`](https://github.com/mathura-snth/math-llm-verifier/blob/main/eng_ver/run.py) (Dataset runner), [`eng_ver/generate_copy.py`](https://github.com/mathura-snth/math-llm-verifier/blob/main/eng_ver/generate_copy.py) (Copy generator), [`archives/generer_copie.py`](https://github.com/mathura-snth/math-llm-verifier/blob/main/archives/generer_copie.py) (Historical generator), [`archives/run_benchmark.py`](https://github.com/mathura-snth/math-llm-verifier/blob/main/archives/run_benchmark.py) (Historical runner)

## Diagram (Mermaid)

```mermaid
flowchart TD

subgraph group_active["Active benchmark"]
  node_runner["Dataset runner<br/>[run.py]"]
  node_copygen["Copy generator<br/>[generate_copy.py]"]
end

subgraph group_logic["Formal logic"]
  node_theorems["Theorem catalog<br/>[theorems.py]"]
  node_hypotheses["Hypothesis dictionary<br/>[hypotheses.py]"]
  node_implications["Implication engine<br/>[implications.py]"]
end

subgraph group_archive["Archived version"]
  node_archive_runner["Historical runner<br/>[run_benchmark.py]"]
  node_archive_generator["Historical generator<br/>[generer_copie.py]"]
  node_archive_theorems["French theorem catalog<br/>[theoremes.py]"]
  node_archive_hypotheses["French hypothesis dictionary<br/>[hypotheses.py]"]
  node_archive_implications["Historical implication engine<br/>[implications.py]"]
  node_exporter["Table exporter"]
end

subgraph group_results["Benchmark data"]
  node_dataset["Generated cases"]
  node_archive_data["Historical dataset"]
end

node_user(("Benchmark user"))

node_user -->|"runs"| node_runner
node_runner -->|"selects from"| node_theorems
node_runner -->|"generates with"| node_copygen
node_copygen -->|"reads requirements"| node_theorems
node_copygen -->|"uses text"| node_hypotheses
node_copygen -->|"checks implications"| node_implications
node_theorems -->|"resolves identifiers"| node_hypotheses
node_implications -->|"uses identifiers"| node_hypotheses
node_runner -->|"writes cases"| node_dataset
node_archive_runner -->|"selects from"| node_archive_theorems
node_archive_runner -->|"generates with"| node_archive_generator
node_archive_generator -->|"reads requirements"| node_archive_theorems
node_archive_generator -->|"uses text"| node_archive_hypotheses
node_archive_generator -->|"checks implications"| node_archive_implications
node_archive_theorems -->|"resolves identifiers"| node_archive_hypotheses
node_archive_implications -->|"uses identifiers"| node_archive_hypotheses
node_archive_runner -->|"writes cases"| node_archive_data
node_exporter -->|"loads cases"| node_archive_data
node_user -->|"exports tables"| node_exporter

click node_runner "https://github.com/mathura-snth/math-llm-verifier/blob/main/eng_ver/run.py"
click node_copygen "https://github.com/mathura-snth/math-llm-verifier/blob/main/eng_ver/generate_copy.py"
click node_theorems "https://github.com/mathura-snth/math-llm-verifier/blob/main/eng_ver/theorems.py"
click node_hypotheses "https://github.com/mathura-snth/math-llm-verifier/blob/main/eng_ver/hypotheses.py"
click node_implications "https://github.com/mathura-snth/math-llm-verifier/blob/main/eng_ver/implications.py"
click node_dataset "https://github.com/mathura-snth/math-llm-verifier/blob/main/eng_ver/benchmark_data.json"
click node_archive_runner "https://github.com/mathura-snth/math-llm-verifier/blob/main/archives/run_benchmark.py"
click node_archive_generator "https://github.com/mathura-snth/math-llm-verifier/blob/main/archives/generer_copie.py"
click node_archive_theorems "https://github.com/mathura-snth/math-llm-verifier/blob/main/archives/theoremes.py"
click node_archive_hypotheses "https://github.com/mathura-snth/math-llm-verifier/blob/main/archives/hypotheses.py"
click node_archive_implications "https://github.com/mathura-snth/math-llm-verifier/blob/main/archives/implications.py"
click node_archive_data "https://github.com/mathura-snth/math-llm-verifier/blob/main/archives/benchmark_data.json"
click node_exporter "https://github.com/mathura-snth/math-llm-verifier/blob/main/archives/exporter_tableau.py"

classDef toneNeutral fill:#f8fafc,stroke:#334155,stroke-width:1.5px,color:#0f172a
classDef toneBlue fill:#dbeafe,stroke:#2563eb,stroke-width:1.5px,color:#172554
classDef toneAmber fill:#fef3c7,stroke:#d97706,stroke-width:1.5px,color:#78350f
classDef toneMint fill:#dcfce7,stroke:#16a34a,stroke-width:1.5px,color:#14532d
classDef toneRose fill:#ffe4e6,stroke:#e11d48,stroke-width:1.5px,color:#881337
classDef toneIndigo fill:#e0e7ff,stroke:#4f46e5,stroke-width:1.5px,color:#312e81
classDef toneTeal fill:#ccfbf1,stroke:#0f766e,stroke-width:1.5px,color:#134e4a
class node_runner,node_copygen,node_user toneBlue
class node_theorems,node_hypotheses,node_implications toneAmber
class node_archive_runner,node_archive_generator,node_archive_theorems,node_archive_hypotheses,node_archive_implications,node_exporter toneMint
class node_dataset,node_archive_data toneRose
```

## Components

### Active benchmark

- [Dataset runner](https://github.com/mathura-snth/math-llm-verifier/blob/main/eng_ver/run.py): `eng_ver/run.py`
- [Copy generator](https://github.com/mathura-snth/math-llm-verifier/blob/main/eng_ver/generate_copy.py): `eng_ver/generate_copy.py`

### Formal logic

- [Theorem catalog](https://github.com/mathura-snth/math-llm-verifier/blob/main/eng_ver/theorems.py): `eng_ver/theorems.py`
- [Hypothesis dictionary](https://github.com/mathura-snth/math-llm-verifier/blob/main/eng_ver/hypotheses.py): `eng_ver/hypotheses.py`
- [Implication engine](https://github.com/mathura-snth/math-llm-verifier/blob/main/eng_ver/implications.py): `eng_ver/implications.py`

### Archived version

- [Historical runner](https://github.com/mathura-snth/math-llm-verifier/blob/main/archives/run_benchmark.py): `archives/run_benchmark.py`
- [Historical generator](https://github.com/mathura-snth/math-llm-verifier/blob/main/archives/generer_copie.py): `archives/generer_copie.py`
- [French theorem catalog](https://github.com/mathura-snth/math-llm-verifier/blob/main/archives/theoremes.py): `archives/theoremes.py`
- [French hypothesis dictionary](https://github.com/mathura-snth/math-llm-verifier/blob/main/archives/hypotheses.py): `archives/hypotheses.py`
- [Historical implication engine](https://github.com/mathura-snth/math-llm-verifier/blob/main/archives/implications.py): `archives/implications.py`
- [Table exporter](https://github.com/mathura-snth/math-llm-verifier/blob/main/archives/exporter_tableau.py): `archives/exporter_tableau.py`

### Benchmark data

- [Generated cases](https://github.com/mathura-snth/math-llm-verifier/blob/main/eng_ver/benchmark_data.json): `eng_ver/benchmark_data.json`
- [Historical dataset](https://github.com/mathura-snth/math-llm-verifier/blob/main/archives/benchmark_data.json): `archives/benchmark_data.json`

### Other components

- **Benchmark user**

## Connections

- Benchmark user → Dataset runner: runs (evidence: `README.md`)
- Dataset runner → Theorem catalog: selects from (evidence: `eng_ver/run.py`)
- Dataset runner → Copy generator: generates with (evidence: `eng_ver/run.py`)
- Copy generator → Theorem catalog: reads requirements (evidence: `eng_ver/generate_copy.py`)
- Copy generator → Hypothesis dictionary: uses text (evidence: `eng_ver/generate_copy.py`)
- Copy generator → Implication engine: checks implications (evidence: `eng_ver/generate_copy.py`)
- Theorem catalog → Hypothesis dictionary: resolves identifiers (evidence: `eng_ver/theorems.py`)
- Implication engine → Hypothesis dictionary: uses identifiers (evidence: `eng_ver/implications.py`)
- Dataset runner → Generated cases: writes cases (evidence: `eng_ver/run.py`)
- Historical runner → French theorem catalog: selects from (evidence: `archives/run_benchmark.py`)
- Historical runner → Historical generator: generates with (evidence: `archives/run_benchmark.py`)
- Historical generator → French theorem catalog: reads requirements (evidence: `archives/generer_copie.py`)
- Historical generator → French hypothesis dictionary: uses text (evidence: `archives/generer_copie.py`)
- Historical generator → Historical implication engine: checks implications (evidence: `archives/generer_copie.py`)
- French theorem catalog → French hypothesis dictionary: resolves identifiers (evidence: `archives/theoremes.py`)
- Historical implication engine → French hypothesis dictionary: uses identifiers (evidence: `archives/implications.py`)
- Historical runner → Historical dataset: writes cases (evidence: `archives/run_benchmark.py`)
- Table exporter → Historical dataset: loads cases (evidence: `archives/exporter_tableau.py`)
- Benchmark user → Table exporter: exports tables (evidence: `README.md`)