Inference Assistant Prototype

Evidence-aware inference playground with a tiny trusted kernel, a perceptron-based rule selector, and proof object export/visualization.

• Typed propositions (atoms, implications, conjunctions) and evidence/proof nodes.
• Rules: axioms, assumptions, modus ponens, ∧-introduction, and coercion to proofs.
• Certification pass that audits allowed rules and confidence thresholds.
• Lean4-inspired C fork (c/leanfork.c) that exposes a tiny type theory (Prop, Type u, Π, →, ∧) and emits a compiler-style certificate for its proof object.
• Learning component that recommends the next rule from handcrafted examples.
• Export proof graphs to JSON or Graphviz DOT for rendering.

LeanFork (Lean4-inspired C core)

The c/leanfork.c program mirrors Lean4’s trusted kernel style (explicit universes, dependent Π, evidence vs. proof status) in a compact C11 file suitable for auditing or further verification.

Build and run the demo/certificate emitter:

cc -std=c11 -Wall -Wextra -pedantic -O2 -o c/leanfork c/leanfork.c
./c/leanfork
cat compiler_certificate.json

The demo rebuilds the “Rainy → Wet → CarryUmbrella” inference, computes confidence-weighted evidence, coerces to a proof when the threshold is met, and writes a JSON compiler certificate.

Quick start

cd inferenceAssistant
python3 -m venv .venv
source .venv/bin/activate
pip install -e .
PYTHONPATH=src python -m inference_assistant.cli \
  --export-json examples/demo_proof.json \
  --export-dot examples/demo_proof.dot \
  --print-certificate

Open the DOT file with Graphviz (dot -Tpng examples/demo_proof.dot -o proof.png) to view the proof graph.

Interactive 3D training data view

Install the optional viz extra to enable 3D scatterplots of the training manifold:

pip install -e .[viz]
PYTHONPATH=src python -m inference_assistant.cli \
  --export-training-3d examples/training_viz.html

Open the resulting HTML in your browser to traverse the labeled 3D point cloud (axes: goal complexity, avg confidence, structural mass). The Plotly runtime is embedded, so no network is required once the file is written.

Tests

PYTHONPATH=src pytest
# or, using the built-in runner with no dependencies:
PYTHONPATH=src python inferenceAssistant/tests/run.py

Layout

• src/inference_assistant/engine.py: kernel for composing evidence and certifying proof graphs.
• src/inference_assistant/learning.py: lightweight perceptron recommending inference rules.
• src/inference_assistant/visualize.py: JSON and DOT exporters for proof objects.
• src/inference_assistant/cli.py: runnable demo that builds a proof, exports artifacts, and prints a certificate.
• tests/: smoke tests for inference and learning.
• whitepaper.md: architecture narrative.
• proposal.md: short plan and milestones.
• c/leanfork.c: Lean4-inspired C kernel + certificate emitter.
• phd-proposal/: LaTeX proposal targeting a Max Tegmark collaboration on machine-supported inference.