agent-scientific

The agent-scientific worked example.

Run it from sema/:

sema check examples/agent-scientific
SEMA_STRICT=1 sema run examples/agent-scientific
sema assure examples/agent-scientific --grade silver

Source

src/main.sema

"""A failed experiment triggers a bounded dynamically admitted proof auditor."""

from std.agents import AgentSpec, AgentEnvelope

assure silver

struct ExperimentState:
    theorem: str
    observation: str

struct ScientificIssue:
    failed: bool
    detail: str

struct ProofFinding:
    correction: str
    sound: bool

struct Paper:
    title: str
    body: str

struct Verification:
    passed: bool

agent monitor(state: ExperimentState) -> ScientificIssue by monitor_model:
    sem "Detect theorem/experiment mismatch and request intervention only on failure"
    budget model_calls=1, tokens=512
    ensure result.failed == true

agent writer(finding: ProofFinding) -> Paper by writer_model:
    sem "Revise the paper from the proof finding and preserve the correction provenance"
    budget model_calls=2, tokens=1024
    ensure len(result.body) >= 1

agent verifier(paper: Paper) -> Verification by verifier_model:
    sem "Apply deterministic verification first; never overrule a failed hard gate"
    budget model_calls=1, tokens=512
    ensure result.passed == true

def proof_auditor(issue: ScientificIssue) -> AgentSpec[ScientificIssue, ProofFinding] !{}:
    return AgentSpec(name="proof_auditor", input_type="ScientificIssue", output_type="ProofFinding",
                     sem="Redo the derivation, isolate the failed premise, and return a sound correction",
                     model="proof_model", tools=[], completion="contract", model_calls=2, tokens=1024)

circuit publish(state: ExperimentState) -> Paper !{agent.spawn, model.invoke}:
    budget agents=8, spawn_depth=2, model_calls=16, tokens=12000
    issue = monitor(state)
    envelope = AgentEnvelope(input_type="ScientificIssue", output_type="ProofFinding",
                             allowed_models=["proof_model"], tools=[], max_model_calls=2,
                             max_tokens=1024, max_children=0, max_spawn_depth=0)
    if issue.failed:
        spec = proof_auditor(issue)
        specialist = Agent.build(spec, under=envelope)?
        finding = (spawn specialist(issue)).join()?
        draft = writer(finding)
        verification = verifier(draft)
        ensure verification.passed
        return draft
    return Paper(title="No correction required", body=state.observation)

def main() -> Paper !{agent.spawn, model.invoke}:
    result = publish(ExperimentState(theorem="H", observation="counterexample"))
    print(result.title)
    return result

Reflected API

main

A failed experiment triggers a bounded dynamically admitted proof auditor.

struct ExperimentState

Fields

field	type	descriptor
theorem	str
observation	str

struct ScientificIssue

Fields

field	type	descriptor
failed	bool
detail	str

struct ProofFinding

Fields

field	type	descriptor
correction	str
sound	bool

struct Paper

Fields

field	type	descriptor
title	str
body	str

struct Verification

Fields

field	type	descriptor
passed	bool

agent monitor

agent monitor(state: ExperimentState) -> ScientificIssue

Parameters

name	type
state	ExperimentState

Returns ScientificIssue

agent writer

agent writer(finding: ProofFinding) -> Paper

Parameters

name	type
finding	ProofFinding

Returns Paper

agent verifier

agent verifier(paper: Paper) -> Verification

Parameters

name	type
paper	Paper

Returns Verification

def proof_auditor

def proof_auditor(issue: ScientificIssue) -> AgentSpec[ScientificIssue, ProofFinding] !{}

Parameters

name	type
issue	ScientificIssue

Returns AgentSpec[ScientificIssue, ProofFinding]

Effects !{}

circuit publish

circuit publish(state: ExperimentState) -> Paper !{agent.spawn, model.invoke}

Parameters

name	type
state	ExperimentState

Returns Paper

Effects !{agent.spawn, model.invoke}

def main

def main() -> Paper !{agent.spawn, model.invoke}

Returns Paper

Effects !{agent.spawn, model.invoke}