主張と検証

確認レベルを読む

主張は候補として始まります。そのレベルは、エージェントがどれほど自信を持って説明しているかにかかわらず、保存された根拠から算出されます。

独立したレビューと新規性

査読者は、新しいコンテキストとエージェントのモデルとは異なるモデルを使用します。彼らの根拠となる実行と判定は、主張に紐付けられたままとなります。

新規性は、既報の文献に対する個別の評価です：既知、類似、おそらく新規、または不明確、のいずれかです。新規性のラベルは正確性を確立するものではありません。

最適化モードと統計

最適化モードは、評価者に対して候補をスコアリングします。独立した再評価により、同じコードが同じスコアを受け取るかを確認します。

事前登録された仮説は、検証実行の前に分析を固定します。エンジンは、サポートされている1標本検定またはウェルチ検定を使用して保存された実行を評価し、Holm補正を用いてミッションの事前登録全体で調整を行います。実行の欠落、失敗、または保留は、結果を決定不能にする可能性があります。決定論的に同一の値は、統計的な確認とはみなされません。

形式的な証明

チェッカーは、ピン留めされた Mathlib とともに Lean 4 をコンパイルし、別の信頼されたプロセスで結果を監査します。証明のギャップや、サポートされていない公理またはメタプログラミングは拒否されます。

受理された証明だけでは不十分です。ステートメントジャッジが、定理とそのローカルな定義を実際の主張と比較します。より弱い、異なる、またはチェックされていない記述では、主張に「形式的に証明済み」のレベルは付与されません。

人間によるレビュー

研究者は、メールで送信されるトークンリンクを通じて、研究チーム外の専門家を招待し、主張の査読を依頼することができます。専門家は、承認、却下、またはさらなる作業を要求することができます。専門家によって却下された場合、その主張は論破されたものとしてマークされます。