Engine
Scientific audit layer
SciCoQA taxonomy, FaithformBench silent-fix gate, synthetic mutations. Auditor outcomes are satisfies, violates, inconsistent, or unknown — never a forced true/false.
Claim → contract → evidence → verdict. Each stage upgrades independently. This page is the SciCoQA taxonomy plus the FaithformBench gate. It is not eight agents in one repo.
satisfies
1
violates
9
inconsistent
6
unknown
2
Paper↔code codes
- Parameter mismatch2
- Equation mismatch8
- Missing operation2
- Extra operation0
- Default-value mismatch2
- Constraint mismatch6
- Shape mismatch0
- Algorithm mismatch3
- Training mismatch2
- Evaluation mismatch5
- Omitted implementation detail3
- Dependency/version mismatch0
Faithfulness gate
A formalizer that changes σ ∈ (−1, 1) to {±1} will prove Lorentz membership of a theorem the paper did not state. F and P are separate.
| Formalization | F | P | Accept? |
|---|---|---|---|
σ ∈ (−1, 1) → σ ∈ (−1, 1) Keeps the paper. Isometry is false on the whole domain. | true | false | fails |
σ ∈ (−1, 1) → σ ∈ {−1, +1} Sycophantic repair. Lean would prove O-membership of a theorem the paper did not state. | false | true | fails |
Synthetic mutations
Start from a correct Lorentz operator, mutate as SciCoQA does, require an oracle to fire. 6/6 caught.
- equation⟨·,·⟩_L → Euclidean dotholds
- parameterσᵣ per relation → one flip_sign per moduleholds
- constraintσ ∈ {±1} → σ ∈ (−1, 1)holds
- missingR B → R onlyholds
- constraintσ ∈ (−1, 1) as printed → σ ∈ {±1} after ‘helpfulness’holds
- algorithmLorentz projection → v = d + (c·d)cholds
Upgrade order
- 1. Claim graph [Atlas]
- 2. Paper↔code taxonomy [SciCoQA]
- 3. Faithfulness gate [FaithformBench]
- 4. Contracts (not silent-fixed) [FormalScience]
- 5. Proof DAG [LeanMarathon]
- 6. Repository verification [Vero]
- 7. Scientific execution [SWE-bench Science]
- 8. Experiment reproduction [PaperBench]
Lean is not in this build. The gate exists so a future autoformalizer cannot silently repair FlorE. Invariants.